Inhale, Exhale, Verify

Can you introduce yourselves and your research area(s)?

Peter: I am Peter Müller. I work at ETH Zurich, mostly on modular program verification.

Rustan: And I am Rustan Leino. I’m based in Seattle and work on programming languages and program verification tools.

In 2025, you won the ETAPS Test of Time Award for your paper “A Basis for Verifying Multi-threaded Programs”. First things first: was it fun to do this work? Was it a piece of cake or really hard work?

Peter: Working on this paper was great fun. In the summer of 2008, we both worked at Microsoft Research. I recall spending our afternoons outside on the terrace and developing the verification technique on paper. We had the whole technique, including its encoding into Boogie sketched out before Rustan implemented it as a Boogie frontend that we later called Chalice.

Can you explain permission-based reasoning and what it is useful for to a first-year PhD student?

Peter: Permission-based reasoning is quite intuitive: Conceptually, we associate an access permission with each heap location. This permission gets created when the memory is allocated. It can be held by a method execution and transferred between methods, but never duplicated or forged. A method may access the memory location only if it holds the corresponding permission, otherwise a verification error occurs. Permissions have many applications in verification. Most prominently, they enable framing (other methods cannot modify a location while one method holds its permission) and data race freedom (as there is only one permission per location, no two methods can hold permission and access simultaneously). Permission reasoning is the foundation of separation logic. It is also used in the Implicit Dynamic Frames technique, which is similar to separation logic, but specifies permissions and value properties separately.

And can you tell us a bit about what motivated you to do this work? What was the main question you wanted to solve at that time?

Peter: I believe the starting point was that we had seen the paper on Implicit Dynamic Frames by Jan Smans, Bart Jacobs and Frank Piessens at the FTfJP workshop at ECOOP 2008. We wanted to understand that work better and explore its potential for the verification of concurrent programs; our main projects back then—Spec# and Dafny—focused on sequential code. So in our paper, we generalized Implicit Dynamic Frames to concurrency, incorporated a variation of Boyland’s fractional permissions to enable concurrent reads while ensuing exclusive writes, and proposed a technique to prove deadlock freedom using a locking order that may change dynamically, for instance, when a data structure gets reorganized.

Rustan: We also had an idea to go beyond the inspiring paper by Smans et al. The original Implicit Dynamic Frames were described by a set of memory locations that Smans et al. showed can be obtained by a simple transformation of user-defined formulas. Instead, we extended every memory location with an extra variable that kept track of the permissions available for that memory location. The extra variable is updated (through operations we called “inhale” and “exhale”) whenever there is a change in permissions, like on procedure boundaries. Furthermore, we made the type of that extra variable a real number, which allowed us to keep track of fractional permissions by adding and subtracting.

Did you have a gut feeling that this paper will become big already before it took off?

Peter: No, not really. This was our first result on permission-based reasoning and, like separation logic at the time, still had lots of limitations.

Rustan: I had thought the encoding in an automated tool (Chalice) would perform better than it did. Alas, the many disjunctions that appear in specifications caused there to be too many different ways to update the real-numbered access permissions, which put too much strain on SMT solvers at the time. That made the technique seem less than perfect, but Peter’s group has worked hard to make this better in Viper since then.

So what follow-up work made you realize that this paper is actually taking off?

Peter: I believe the turning point was when we realized that the inhale and exhale operations we used as a part of this encoding would make an excellent basis for an intermediate verification language. Typical separation logic proof rules can be expressed as exhaling an assertion, framing all properties that were not exhaled, and then inhaling an assertion. This insight allows one to encode and automate diverse separation logic proof rules, just like assume and assert had been used to encode the rules of Hoare logic.

Do you have any guess on what made this work so impactful rather than just being “just another” research result?

Rustan: We believe that two developments contributed to the impact of this work. One was the development of the Viper infrastructure, which uses inhale and exhale as its main primitives and the Boogie encoding in one of its backends. Viper demonstrated that the ideas from our paper work in practice and can handle a diverse class of languages, programs, properties, and logics.

Peter: The other important development was to realize that Implicit Dynamic Frames have various advantages over standard separation logic because they separate permission reasoning from reasoning about values, for instance, because they reduce redundancy between specifications and code and facilitate incremental verification. We did not invent Implicit Dynamic Frames, but for many years Chalice and later Viper were the main projects developing this approach further.

Did different aspects about your paper become influential than the ones you would have expected? Any surprises? Anything that aged particularly well or not so well?

Peter: Yes, absolutely. When I prepared the talk for our Test-of-Time award, I re-read the paper and was quite astonished how different my perception is now than it was 16 years ago. Back then, I saw the inhale and exhale primitives mostly as shorthands for defining the Boogie encoding. I had not realized their potential as primitives of an intermediate language. Conversely, much of the paper is about proving deadlock freedom with dynamic locking orders, an aspect that seemed very important to us, but did not trigger much follow-up work.

In your award lecture, Peter, you mentioned that you were criticized for the terminology inhale / exhale as keywords of your intermediate verification language. Can you give us some intuition on what inhale and exhale means and what is different to assume / assert?

Peter: You can think of inhale and exhale as the permission-aware analogs of assume and assert statements. For a given assertion, inhale adds all permissions denoted by the assertion and assumes its value constraints. Exhale asserts the value constraints and removes the permissions. Interestingly, most encodings of operations into guarded commands generalize to separation logic simply by replacing asserts and assumes with exhales and inhales, respectively. For instance, the standard encoding for a method call is to assert its precondition and then assume its postcondition. In permission reasoning, the encoding exhales the precondition and inhales the postcondition, which performs the same reasoning about value constraints, but also transfers permissions to the callee method and back. Exhale and inhale are also known as consume and produce in symbolic execution engines for separation logic, e.g., VeriFast, but their use is not limited to symbolic execution.

Rustan: The fact that permissions are transferred when a formula is exhaled or inhaled can be viewed as if the evaluation of the formula had side effects. No one would accept a paper that celebrated side effects in expressions, but if you think about it through this lens, you realize that this is what any kind of linear logic does.

In hindsight, would you have made any significantly different design choices?

Rustan: Our paper extends Boyland’s fractional permissions with a notion of infinitesimal fractions, which allow unboundedly many reads. There are more elegant solutions that can be encoded efficiently into SMT, such as the abstract read permissions we proposed later.

Moving forward, what are the most exciting current advances in the field?

Peter: It is exciting to see that formal verification is finally catching on. There is a renewed interest in developing verification tools, such as Caesar, COMA, Gillian, Loom, Raven, Verus, and many others. It is also interesting that the combination of interactive theorem provers with AI might offer a third way to automate proofs, beyond SMT and tactics in interactive theorem provers.

Rustan: Yes, it’s great to see that formal verification for programs is catching on. The idea of designing programming languages that incorporate specifications goes back many decades (for example, the Euclid language around 1980). These days, it has been shown that AI performs particularly well on such languages. Moreover, if an AI is going to generate code for us, it is only fair that it also supplies us with a proof of correctness.

What do you expect is the next big thing / next big challenge in verification, formal methods, and programming language theory? Where do you see the biggest conceptual gaps?

Peter: A huge challenge is obviously to get AI to a point where it can generate code with verified correctness and security properties. Ideally, an AI would generate code along with proofs and check them before even showing them to the user. Automated, modular verification has a major role to play in such a scenario.

Rustan: I’ve always liked the idea of providing all programmers with the ability to use verification. AI will help with this. But I think there’s still room to improve our interface to writing verified programs and the ergonomics of using a verifier.

Finally, who would you like to see interviewed for our blog in the future?

Peter: I am excited about Ilya Sergey’s work on Loom, Velvet, and Veil. They explore new directions in verification, combining automatic, AI-based, and interactive proofs.

Rustan: I suggest Daan Leijen. He writes beautiful papers, he works on theoretical programming-language constructs, and he writes impressive implementations that are used in industry. Asking him how he blends theory and practice would be interesting for the blog.

…and which paper would you recommend everyone to read?

Rustan: The verification work done using an auto-active verifier in “Atmosphere: Practical Verified Kernels with Rust and Verus” by Xiangdong Chen et al. is impressive. It also gives some idea of what is possible today with formal verification. Another recent paper that impressed me was “A benchmark for vericoding: formally verified program synthesis” by Sergiu Bursuc et al. It collects vericoding benchmarks created in different settings and applies LLMs to these using several tools.

Peter: I would recommend reading Aleks Chakarov et al.’s “Formally Verified Cloud-Scale Authorization” from ICSE 2025. It is a great showcase of what auto-active verification can do today; I find it especially impressive that the verified Dafny implementation developed in this project outperforms the prior Java code. I’d also suggest the work on COMA by Andrei Paskevich et al. from ESOP 2025. Letting programmers choose where to place the abstraction boundaries for modular verification is a simple, yet powerful idea.

Peter, Rustan, many thanks for taking the time! And once again: congratulations on the Test of Time Award!