Sound Gradual Verification with Symbolic Execution
This version contains supplementary material for the paper of the same name accepted for publication by Principles of Programming Languages (2024).

Conrad Zimmerman

Brown University

Jenna DiVincenzo

Purdue University

Jonathan Aldrich

Carnegie Mellon University

Gradual verification, which supports explicitly partial specifications
and verifies them with a combination of static and dynamic checks, makes
verification more incremental and provides earlier feedback to developers.
While an abstract, weakest precondition-based approach to gradual verification
was previously proven sound, the approach did not provide sufficient guidance
for implementation and optimization of the required run-time checks.  More
recently, gradual verification was implemented using symbolic execution
techniques, but the soundness of the approach (as with related static
checkers based on implicit dynamic frames) was an open question.  This paper
puts practical gradual verification on a sound footing with a formalization
of symbolic execution, optimized run-time check generation, and run time
execution.  We prove our approach is sound; our proof also covers a core
subset of the Viper tool, for which we are aware of no previous soundness result.
Our formalization enabled us to find a soundness bug in an implemented gradual
verification tool and describe the fix necessary to make it sound.

20 February 2007
[revised]12 March 2009
[accepted]5 June 2009

§ INTRODUCTION

Static verification technology based on Hoare-logic-styled pre- and postconditions <cit.> has come a long way in the last few decades. Such tools can now support the modular verification of data structures that manipulate the heap <cit.> and are recursive <cit.>. However, verification is expensive, requiring many auxiliary specifications such as loop invariants and lemmas, and often costing an order of magnitude more human effort than development alone. In response, <cit.> introduced the idea of gradual verification, which supports the incremental specification and verification of code by seamlessly combining static and dynamic verification. A developer can now write partial, imprecise specifications—formulas such as $\simprecise{x.f \keq 2}$—backed by run-time checking. During static verification, imprecise specifications are strengthened in support of proof goals when it is necessary and non-contradictory to do so. Then, corresponding dynamic checks are inserted to ensure soundness. As a result, gradual verification allows users to specify and verify only the properties and components of their system that they care about, and incrementally increase the scope of verification as necessary.

Based on this early idea, <cit.> and <cit.> extended gradual verification to support recursive heap data structures.
<cit.> presented the first theory of gradual verification for implicit dynamic frames (IDF) <cit.>, a variant of separation logic <cit.>, and abstract predicates <cit.>. Their design, corresponding theory, and proofs rely heavily on the backward-reasoning technique called weakest liberal preconditions (WLP), and on infinite sets that are not easy to approximate in finite form. Additionally, <cit.>'s design checks all proof obligations at run-time, even when some obligations have been discharged statically. Therefore, it remained unclear how to implement gradual verification and whether gradually-verified programs could achieve good performance. Fortunately, in follow-up work, <cit.> implemented and empirically evaluated , the first gradual verifier that can be used on real programs. is based on symbolic execution, a forward-reasoning technique which is routinely used in static verifiers such as Viper <cit.>, and optimizes run-time checks with statically available information to improve run-time performance. <cit.> showed that this improvement over prior work yields significant performance boosts.

Technically, is built on top of Viper <cit.>, which is a static verification infrastructure and tool that facilitates the development of program verifiers supporting IDF and recursive abstract predicates. Viper also uses symbolic execution at its core. Besides , an array of widely-used verifiers have been built on top of Viper, including Prusti <cit.> for Rust, Nagini <cit.> for Python, and VerCors <cit.> for Java.
However, despite its prominence, Viper has not been proven sound; nor have, to our knowledge, other symbolic execution-based methods for verifying IDF logics. Thanks to the complexities of symbolic execution and Viper's support for practical but advanced verification features, <cit.>'s specification of Viper is full of implementation details that make it difficult to formally state and prove soundness. Since is built on Viper, this problem carries over to 's specification in <cit.> and is made worse by the combination of static and dynamic checking. Thus <cit.> does not contain a proof of soundness for . Furthermore, since uses symbolic execution instead of WLP and optimizes run-time checks, <cit.>'s proof is also not applicable. This is problematic, because the intricate interactions of static and dynamic checking in gradual verification can easily lead to subtle soundness bugs in gradual verifiers like , as we will show in <ref>.

Therefore, this paper presents a formal statement and proof of soundness for and its underlying core subset of Viper. We formalize 's symbolic execution algorithm in sets of inference rules, rather than the CPS-style specification in <cit.> and <cit.>, to enable abstractions that improve the readability of the design and make it easier to state and prove soundness. The level of abstraction we use is far closer to the implementation of than <cit.>'s formal system, but slightly more abstract than <cit.>'s CPS-style specification, which is littered with implementation details. Reaching the right level of abstraction for our goals took some trial and error. We reflect on this process, including our missteps, in this paper as well. Our approach is inspired by the formal system for a basic type checker combined with symbolic execution in <cit.>. However, we separate the rules into several types of judgements to reflect the architecture of <cit.> and <cit.> and deal with the complexities of IDF and gradual verification. Given an initial symbolic state, the rules compute a next possible state (of which many may exist), and a set of run-time checks required for this transition when optimism is relied upon. That is, our rules are non-deterministic, but only in regards to the multiple execution paths explored by symbolic execution at program points like if statements, while loops, and logical conditionals.

Furthermore, we clearly separate the cases required to support imprecise specifications from those dealing with the underlying verification algorithm supporting only complete static specifications. Therefore, our formal system is a conservative extension of a core calculus of Viper; and so, by formalizing and proving it sound, we have also formalized the core of Viper and proved it sound. To make it easier for readers of this paper to take advantage of our formal statement and proof of soundness for Viper for their own uses, we present first a core language, which we call , along with verification rules modeling 's underlying static verification algorithm. We then define , which extends to include gradual specifications and corresponds to the full language used by . We also formally define static verification for , modeling the verification algorithm of . We hope this separation provides a solid foundation for future proof endeavors of other static verifiers based on symbolic execution.

In order to fully define the behavior of and its subset , we specify its dynamic semantics, which combines the semantics of <cit.> with the dynamic semantics of , the language used to define the theory of gradual verification with recursive predicates in <cit.>.
The programming language is a core, safe variant of the C language introduced for education <cit.> and is also supported by . allows specification of the pre- and post-conditions of methods, but does not include constructs necessary for static verification using IDF.
Thus we add the dynamic semantics from <cit.> for IDF specifications, recursive predicates, and imprecise specifications. These semantics assert the validity of every specification at run-time, ensuring both memory safety and functional correctness of programs.
Thus these semantics provide a foundation against which we can establish the soundness of 's symbolic execution algorithm. That is, we prove that when all run-time checks produced by the symbolic execution algorithm are satisfied, then the program is guaranteed to dynamically execute successfully. A tricky part of this proof is defining a valuation function <cit.>, which is a partial function mapping symbolic values from symbolic execution to their concrete values for a specific execution trace from program execution. This function is used to state the correspondence between symbolic and concrete execution states. While we start with <cit.>'s simplistic valuation function, we end up with one that is far more complex as it additionally connects isorecursive symbolic predicates from static verification with their equirecursive counterparts in dynamic verification and handles global invariants such as separation and access permissions from IDF.
This proof technique allows our formal system and reasoning to match the implementation more closely than other techniques such as the evidence calculus used in <cit.>. This enables us to explore future developments using either the implementation or formalization, and easily update the other to ensure we remain both implementable and sound.

Finally, we present and discuss a soundness bug we found in during our proof work and have since communicated to <cit.>. The bug is a specific interaction caused by reducing run-time checks using statically available information in isorecursive predicates, and then checking the remaining run-time checks using equirecursive predicates. This bug could not have arisen in <cit.>'s work as their gradual verification approach checks all proof obligations at run time. We explore several options for addressing this soundness bug, explain our chosen method in detail, and discuss an implementation fix. Despite <cit.>'s thorough empirical evaluation and testing of , this bug was never discovered in their testing. This is likely due to the subtle, intricate interactions between verification technologies in gradual verification that are hard to test. This demonstrates the value of formally proving soundness in the case of gradual verification, and we hope this paper serves as a basis for similar future work.

To summarize, this paper makes the following contributions:

* Formalization and proof of soundness for , the first gradual verifier for recursive heap data structures that is based on symbolic execution <cit.>. The level of abstraction chosen for this proof work improves the readability of 's design and makes adapting this work to prove other symbolic execution-based gradual verifiers sound much easier.

* Formalization of a core subset of the Viper static verifier, which is based on symbolic execution and supports IDF. This work provides the first solid foundation for proof work on static verifiers that use symbolic execution and IDF.

* A reflection on the trial and error of picking the right level of abstraction for our proof work in this paper.

* Demonstration of a soundness bug we found in during our work and have since communicated to <cit.>. We also provide several options for addressing this bug and advise on how to implement one of our solutions.

We first introduce and a corresponding static verification algorithm. Since it does not include imprecise specifications, can be verified by existing static verification tools such as Viper <cit.>.
The verification algorithm corresponds to the core algorithm of Viper, which is the foundation for static verification in .
We illustrate how our formalism and soundness result can be applied to Viper. In later sections we extend 's verification algorithm to support the verification of gradually-specified programs.

§.§ Definition

We define an abstract syntax for in Figure <ref>. Its form is similar to the language of Viper, which is intended for use as a generic backend for multiple frontend languages; however, we use the syntax of .

Programs consist of struct, predicate, and method[To distinguish them from pure functions (which are used in the specification language of similar verification tools) we use method to refer to any potentially impure function.] definitions, and an entry statement. Struct definitions contain a list of fields, predicate definitions contain a parameter list and a formula (the predicate body), and method definitions contain a parameter list, a return type, a pre-condition (denoted by $\krequires$), a post-condition (denoted by $\kensures$), and a statement (the method body). The entry statement represents the body of the main method in traditional C programs. Statements in follow C conventions, except for while, alloc, and return. All while statements specify a formula called a loop invariant, which states the properties preserved by the loop during execution. An alloc statement allocates new memory on the heap, initializes it with a default value, and updates the variable on the left-hand side to contain a reference to the newly allocated value. This matches semantics, except returns a pointer, not a reference, and thus the type of the variable is written differently. We omit return statements; instead, the method body must assign to a special result variable, whose value is then returned after executing the method body. This reflects the behavior of which also does not have a return statement. Additionally, we simplify several statements to make formal definitions and proofs easier. For example, assignment only occurs to a variable or a field of a variable; statements such as x.y.z = 1 are not permitted. We also omit void method calls, since these do not differ meaningfully from calls to value-returning methods.

Like <cit.>, does not support arrays. Verifying non-trivial properties of programs that use arrays would require significant extensions to existing gradual verification theory – for example, quantified formulas. These extensions are left to future work. However, we can verify recursive data structures such as linked lists with abstract predicates. Note that Viper does support quantified formulas and arrays, thus further work is necessary to formally prove soundness of these capabilities.

We make several simplifying assumptions for programs. All variables are initialized before they are used, and every execution path for a method body assigns the result variable at its end. Every program is well-typed; that is, expressions used in if conditions or as boolean operands will evaluate to bool values, all arguments passed to method parameters will match the defined parameter type, and the value assign to result has type equal to the method's return type. Finally, all specifications (predicate bodies, loop invariants, and method pre- and post-conditions) are self-framed, which is a special well-formedness condition from IDF that we define later.

x    ∈   Variable names

f    ∈   Field names

p    ∈   Predicate names

m    ∈   Method names

S    ∈   Struct names

n    ∈ℤ    Integers

Π   ::= 𝒮   𝒫   ℳ   s

𝒮    ::=  S   T f

𝒫    ::= p(T x) = ϕ

ℳ    ::= T m(T x)   Φ  s

Φ::=      ϕ  ϕ

T           ::=     S |||

s           ::=     ss ||x e |x = (S) |

x = m(e) |ϕ |p(e) |

p(e) |ess |

e           ::=     l |x |e.f |e ⊕e |e e |e e |e

l           ::=     n |||

⊕::=     + |- |/ |* |== |!= |<= |>= |< |>

ϕ::=     ϕ* ϕ|p(e) |e |(e.f) |

Abstract syntax for

§.§.§ Formulas

Formulas (specifications) in are written in the logic of IDF <cit.> and recursive predicates <cit.>. Thus formulas may contain expressions as well as abstract predicates and accessibility predicates from IDF; formulas may be joined by the separating conjunction $*$ <cit.>. An accessibility predicate $\kacc(e.f)$ requires access to the heap location $e.f$. A predicate instance $p(\overline{e})$ applies the boolean predicate $p$ to the arguments $\overline{e}$. An expression $e$ requires that $e$ evaluates to $\ktrue$. A separating conjunction, as in $\phi_1 * \phi_2$, acts like a logical AND for $\phi_1$ and $\phi_2$, but also requires the heap locations specified by predicates and accessibility predicates in $\phi_1$ to be disjoint from those specified in $\phi_2$, e.g. $\kacc(x.f) * \kacc(y.f)$ implies $x \kneq y$. A conditional formula $\sif{e}{\phi_1}{\phi_2}$ denotes the validity of $\phi_1$ when $e$ evaluates to $\ktrue$; otherwise it denotes the validity of $\phi_2$.

Formulas in IDF, and thus in , must be self-framed <cit.>, which requires permissions for all heap locations used in a formula to also be in that formula. For example, x.value == 0 is not self-framed since it references the heap location x.value, but does not assert accessibility of the field x.value. However, acc(x.value) $*$ x.value == 0 is self-framed. We specify rules for framing and self-framing in <ref>.

Static verification of predicates is done isorecursively <cit.>, thus predicate instances must be explicitly folded before they can be asserted. Similarly, predicate bodies must be explicitly unfolded before asserting the implications of a predicate. This enables static verification of recursive predicates and simplifies reasoning about the verifier's behavior.

§.§ Representation

In this section, we formally define the data structures used during static verification of programs.

* A symbolic value $\nu \in \textsc{SValue}$ is an abstract value representing an unknown value, such as an integer or object reference. We leave the concrete type of $\textsc{SValue}$ undefined, but assume that an infinite number of distinct new values can be produced by a $\ffresh$ function.

* A symbolic expression $t \in \SExpr$ is a symbolic or literal value, or is composed of other symbolic expressions and operators.

$$t \quad::=\quad \nu \quad\mid\quad l \quad\mid\quad \kneg t \quad\mid\quad t_1 \kand t_2 \quad\mid\quad t_1 \kor t_2 \quad\mid\quad t_1 \oplus t_2$$

* A path condition $\pc \in \SExpr$ is a symbolic expression composed of conjuncts identifying a particular execution path. Conjuncts are added at every conditional branch during symbolic execution.

* A field chunk $\triple{f}{t}{t'} \in \SField$ represents, in the symbolic heap, the field $f$ of an object reference $t$ containing a value $t'$. A heap chunk is roughly approximate to the points to construct in separation logic <cit.>. A predicate chunk $\pair{p}{\multiple{t}} \in \SPredicate$ represents an isorecursive instance of a predicate $p$ with arguments $\multiple{t}$. Together, field chunks and predicate chunks are called heap chunks.

* A symbolic heap $\sheap \in \powerset{\SField \cup \SPredicate}$ is a finite set of heap chunks. All heap chunks that it contains must represent distinct locations in the heap at run time.

* A symbolic state $\sstate \in \SState$ is a tuple containing a path condition (referenced by $\pc(\sstate)$), a symbolic heap (referenced by $\sheap(\sstate)$), and a symbolic environment (referenced by $\senv(\sstate)$). A symbolic state stores all values for a particular point during symbolic execution. The symbol $\ssempty$ represents an empty symbolic state, i.e. $\pc(\ssempty) = \ktrue$ and $\sheap(\ssempty) = \senv(\ssempty) = \emptyset$.

* A verification state $\vstate$ represents a particular point during static verification. It is either a special symbol or a triple $\triple{\sstate}{s}{\gform}$ consisting of a symbolic state $\sstate$, a statement $s$ that remains to be executed, and a formula $\gform$ that must be asserted after executing $s$. $\sstate(\vstate)$, $s(\vstate)$, and $\gform(\vstate)$ are used to reference a specific component of $\vstate$ when $\vstate$ is not a symbol.

$$\vstate \quad::=\quad \initsym \quad\mid\quad \finalsym \quad\mid\quad \triple{\sstate}{s}{\gform}$$

* A valuation $V : \SValue \to \Value$ is a mapping from symbolic values to concrete values (defined in <ref>). Valuations are implicitly extended to be defined for all $\SExpr$, following the structure of symbolic expressions.

A symbolic expression $t$ implies the symbolic expression $t'$ (written $t \implies t'$) if, for all valuations $V$, $V(t) = \ktrue \implies V(t') = \ktrue$. For example, $t_1 \kand t_2 \implies t_2$. A symbolic expression $t$ is satisfiable, denoted $\mathrm{sat}(t)$, if $V(t) = \ktrue$ for some valuation $V$.

§.§ Evaluating expressions

Symbolic execution evaluates an expression $e$ to a symbolic value $t$ using the symbolic state $\sstate$, and is denoted by the judgement $\sstate \vdash e \Downarrow t \dashv \sstate'$.
It also yields a new symbolic state $\sstate'$ which may contain a more specific path condition if this particular evaluation short-circuits a boolean operator.
Selected formal rules for symbolic evaluation are given in Figure <ref>. Literals are evaluated to themselves and variables are evaluated to the corresponding value in the symbolic store. Some operators, such as negation and arithmetic operators, are directly translated into a symbolic expression using the respective operator. In contrast, boolean operators are short-circuiting: when evaluating $e_1 \kand e_2$, if $e_1$ evaluates to $\kfalse$, then $e_2$ is never evaluated (in this case, $e_1 \keq \kfalse$ is added to the path condition). We define two non-deterministic rules for each binary boolean operator—SEvalAndA represents the short-circuiting case just described, while

SEvalAndB represents the non-short-circuiting case where $e_1$ is true, so $e_2$ must also be evaluated to determine the result.

Finally, field references are evaluated to the symbolic value contained in their corresponding field chunk in the symbolic heap. Note, a heap chunk for the field reference must be in the heap, otherwise evaluation fails (and ultimately static verification as well), thus the field reference must be framed by the current state.

We also define a judgment of the form $\sstate \vdash e \downarrow t$ which symbolically evaluates an expression $e$ to a symbolic expression $t$ without short-circuiting. Thus the judgment is deterministic and does not update the path condition. Instead, logical operators such as $\kand$ are encoded directly in the symbolic expression (compare SEvalPCAnd with SEvalAndA/SEvalAndB in Figure <ref>). This results in a less specific path condition, but reduces the number of execution paths during symbolic execution. This matches the evaluation method described in <cit.> for evaluation in formulas, while the former style is used for evaluation in imperative code.

⊢l ⇓l ⊣ [SEvalVar]

⊢x ⇓()(x) ⊣ [SEvalNeg]
⊢e ⇓t ⊣'
⊢e ⇓t ⊣'  [SEvalAndA]
⊢e_1 ⇓t_1 ⊣'
⊢e_1 e_2 ⇓t_1 ⊣'[= (') t_1]  [SEvalAndB]
⊢e_1 ⇓t_1 ⊣'

'[= (') t_1] ⊢e_2 ⇓t_2 ⊣”
⊢e_1 e_2 ⇓t_2 ⊣”  [SEvalField]
⊢e ⇓t_e ⊣'

(') t_e t_e'

t_e'ft ∈(')
⊢e.f ⇓t ⊣'  [SEvalPCAnd]
⊢e_1 ↓t_1

⊢e_2 ↓t_2
⊢e_1 e_2 ↓t_1 t_2 ⊣”

Selected symbolic evaluation rules

§.§ Consuming formulas

Given a symbolic state $\sstate$ and formula $\phi$, consuming a formula $\phi$ first asserts that $\phi$ is established by $\sstate$, and second removes the heap chunks in $\sstate$ corresponding to permissions (predicates and accessibility predicates) in $\phi$. The judgment $\sstate \vdash \phi \rhd \sstate'$ denotes consumption; i.e., $\phi$ is consumed from $\sstate$, resulting in the new symbolic state $\sstate'$. See Figure <ref> for selected rules.

Consuming an accessibility predicate such as $\kacc(e.f)$ first asserts the predicate has a corresponding field chunk in the heap, and second removes the chunk from the heap (SConsumeAcc).
Consuming a predicate similarly looks for and removes the corresponding predicate chunk from the heap (SConsumePredicate). If any of the chunks are missing from the heap, then verification fails.
Expressions must evaluate to $\ktrue$ in the current symbolic execution path. That is, the current path condition must imply the symbolic value of the expression (SConsumeValue). As mentioned previously and seen in the aforementioned rule, expressions in formulas are evaluated with the deterministic evaluation judgment (i.e., not the short-circuiting one), which matches the behavior described in <cit.> and reduces the number of branches generated during symbolic execution. This differs from Viper, which uses a single, short-circuiting eval algorithm everywhere, including in consume. A separating conjunction, such as $\phi_1 * \phi_2$, is consumed left-to-right, i.e. $\phi_1$ is consumed and then $\phi_2$ is consumed (SConsumeConjunction). This enforces the separation of permissions between the two conjuncts – heap chunks necessary to satisfy the permissions asserted in $\phi_1$ will be removed before consuming $\phi_2$, so, if they overlap, consumption of $\phi_2$ will fail.
Finally, we define consumption of logical conditionals, like $\sif{e}{\phi_1}{\phi_2}$, in two non-deterministic rules. In SConsumeConditionalA, $e$ is assumed to be true in the path condition and $\phi_1$ is consumed. Likewise, in SConsumeConditionalB, $e$ is assumed to be false in the path condition and $\phi_2$ is consumed.

Note, as we saw in <ref>, evaluation of a field access in an expression requires the state to contain a heap chunk for the field. But consume removes heap chunks from the state in a left-to-right manner thanks to rules SConsumeAcc and SConsumeConjunction.

For example, we may want to consume the formula $\kacc(e.f) * e.f \keq 0$. First, a heap chunk for $\kacc(e.f)$ is found and removed from the heap. Then, the resulting state is used to frame and evaluate $e.f \keq 0$ in the next consume step. However, the heap chunk for $e.f$ was removed from the state so evaluation fails when it shouldn't since the original state contained the heap chunk.
To solve this issue, we define consume using an underlying judgment, denoted $\sstate, \sstate_E \vdash \phi \rhd \sstate'$, which asserts and removes permissions from $\sstate$ while evaluating expressions with the unchanging reference state $\sstate_E$. The state $\sstate_E$ is the symbolic state before consumption. The rule SConsume defines the top-level consume judgment using this new underlying judgment.

Our consume judgment represents the core functionality of <cit.> and <cit.>'s consume algorithms.
We, of course, ignore unnecessary implementation details like snapshots, which preserve certain portions of the state that are removed during consume.

, ⊢ϕ'
⊢ϕ'  [SConsumeValue]
_E ⊢e ↓t

() t
, _E ⊢e  [SConsumeAcc]
_E ⊢e ↓t_e

() t_e t_e'

() =  ft_e't ⊎'
, _E ⊢(e.f) [= ']  [SConsumePredicate]
_E ⊢e ↓t

() t t'

() = pt'⊎'
, _E ⊢[= ']  [SConsumeConjunction]
, _E ⊢ϕ_1 '

', _E[= (')] ⊢ϕ_2 ”
, _E ⊢ϕ_1 * ϕ_2 ”  [SConsumeConditionalA]
_E ⊢e ↓t

' = () t

[= '], _E[= '] ⊢ϕ_1 '
, _E ⊢eϕ_1ϕ_2 '  [SConsumeConditionalB]
_E ⊢e ↓t

' = () t

[= '], _E[= '] ⊢ϕ_2 '
, _E ⊢eϕ_1ϕ_2 '

Selected consume rules

§.§ Producing formulas

Given an initial state $\sstate$ and formula $\phi$, producing $\phi$ adds the information in $\phi$ into the symbolic state $\sstate$, resulting in a new state $\sstate'$. The judgment for $\sstate \vdash \phi \lhd \sstate'$ denotes production; i.e., $\phi$ is produced into the state $\sstate$, resulting in $\sstate'$. In particular, produce adds heap chunks representing predicates in $\phi$ to the symbolic heap and symbolic expressions representing constraints from boolean expressions in $\phi$ to the path condition in a left-to-right manner. Note, each symbolic heap chunk represents a distinct region of memory at run-time, an invariant that we later prove. Thus overlapping heap chunks may only occur in symbolic states which represent an unreachable dynamic state and can safely be ignored.

When producing formulas, we use deterministic symbolic evaluation for expressions, but we introduce separate execution paths for conditionals (similar to <ref>).

Formal rules are given in the supplement <cit.><ref>.

These rules capture the functionality of the produce algorithm specified in <cit.> and <cit.>. As noted in the previous section, <cit.> uses short-circuiting evaluation in all places, while we use deterministic evaluation.

§.§ Executing statements

Now that we have formally defined symbolic execution of expressions and formulas, we can put the pieces together to define symbolic execution of program statements.

We represent the symbolic execution of program statements as small-step execution rules denoted by the judgment $\sstate \vdash s \to s' \dashv \sstate'$, where the initial statement $s$ is symbolically executed with the initial state $\sstate$, resulting in the state $\sstate'$, and then transitions to the next statement $s'$ with the new state $\sstate'$. Selected formal rules are shown in Figure <ref>. Executing a variable assignment updates the symbolic store (SExecAssign); while executing a field assignment first consumes $\kacc(x.f)$,
and then adds a new heap chunk for $x.f$ to the heap that contains $x.f$'s new symbolic value after the write (SExecAssignField).
An $\kalloc(S)$ statement adds a heap chunk for each field in $S$ to the symbolic heap. The new object reference is a fresh value but the new field chunks are each initialized with default values, which reflects the behavior of (SExecAlloc).
Execution rules for $\kif$ statements are non-deterministic: given a statement $\sif{e}{s_1}{s_2}$, SExecIfA adds $e$ to the path condition and continues execution with $s_1$, while SExecIfB adds $\kneg e$ to the path condition and continues execution with $s_2$.

Symbolic execution of method calls is modular; i.e., the behavior of the method call is represented by the method's pre- and post-conditions (SExecCall).
First, the method's arguments are evaluated to symbolic values. Then the pre-condition is consumed using a special environment containing the argument values. A $\ffresh$ symbolic value is added to represent the return value of the method, and then the post-condition of the method is produced.
The special environment is then replaced by the original environment, with the addition of the result's symbolic value. Loops (i.e $\kwhile$ statements) are executed similarly: the loop invariant is consumed, variables modified by the loop body are set to fresh values in the symbolic store, the loop invariant is produced, and the negated loop condition is added to the path condition (SExecWhile).
Execution of the $\kfold$ and $\kunfold$ statements is also similar to loops and method calls:

$\kfold$ consumes the predicate body and adds a representative predicate chunk to the symbolic heap, while $\kunfold$ consumes the predicate instance (thus removing the predicate chunk from the heap) and produces the predicate body.

⊢e ⇓t ⊣'

' = ()[x ↦t]
⊢x es →s ⊣'[= ']  [SExecAssignField]
⊢e ⇓t ⊣'

' ⊢(x.f) ”

' = (”) ∪ f(”)(x)t
⊢x.f es →s ⊣”[= '] [SExecAlloc]
t =

T f = (S)

' = () ∪ ft(T)
⊢x (S)s →s ⊣[= ']  [SExecCall]
⊢e ⇓t ⊣'

x = (m)

'[= [x ↦t]] ⊢(m) ”

t' =

' = (')[y ↦t']

”[= [x ↦t, ↦t']] ⊢(m) ”'
⊢y m(e)s →s ⊣”'[= ']  [SExecIfA]
⊢e ⇓t ⊣'

” = '[= (') t]
⊢es_1s_2s →s_1s ⊣”  [SExecIfB]
⊢e ⇓t ⊣'

” = '[= (') t]
⊢es_1s_2s →s_2s ⊣”  [SExecWhile]

x = (s)

'[= (')[x ↦]] ⊢ϕ”

” ⊢e ↓t
⊢eϕss' →s' ⊣”[= (”) t]

Selected symbolic execution rules

§.§ Modularly verifying programs

We now define verification of entire programs.
We start by defining what a program $\prog$ is; it is a quadruple $\quadruple{s}{M}{P}{S}$ where $s$ is the entry statement of the program, $M$ is the set of method names, $P$ is the set of predicate names, and $S$ is the set of struct names in the program.
Then, we define the judgment $\strans{\prog}{\vstate}{\vstate'}$ that specifies all possible symbolic execution steps that occur during verification of $\prog$. Selected rules are given in Figure <ref>.

A verification state $\vstate$ is reachable from program $\prog$ if $\vstate = \initsym$ or $\strans{\prog}{\vstate_0}{\vstate}$ for some reachable $\vstate_0$.  The latter judgement only holds when $\vstate_0$ is itself reachable.

This judgement includes rules for modular verification. From $\initsym$, we can begin verification of the entry statement (SVerifyInit) or of any method (SVerifyMethod). When verifying a method, the method's post-condition is used as the formula of the verification state. After completely executing the method's body, i.e. having reached $\kskip$, we consume the formula contained in the verification state (SVerifyFinal), which is the method's post-condition.

We modularly verify loop bodies following a similar pattern. As described in <ref>, symbolic execution steps over loop bodies in the same way it steps over method calls. However, we introduce a verification rule (SVerifyLoopBody) that allows symbolic execution of a loop body, beginning with a new symbolic state. We reuse the symbolic store from the initial symbolic state, except that all variables modified by the loop body are replaced by fresh values. Verification proceeds similar to method verification, except that we use the loop invariant for the formula of the new verification state—we produce the loop invariant, symbolically execute the loop body, and finally consume the loop invariant. Thus symbolic execution, which steps over the loop, ensures that the loop invariant holds for the initial iteration, while this verification rule ensures that the loop invariant is preserved after every iteration.

We also include another verification rule for loops, SVerifyLoop, in order to match the behavior of . This rule and its correspondence with is described further in <ref>.

Statements are executed by symbolic execution as described in <ref>. Given a reachable verification state $\triple{\sstate}{s}{\phi}$ and the symbolic execution $\sstate \vdash s \to s' \dashv \sstate'$, the state $\triple{\sstate'}{s'}{\phi}$ is reachable, i.e. $\prog \vdash \triple{\sstate}{s}{\phi} \to \triple{\sstate'}{s'}{\phi}$.

sMPSs  [SVerifyMethod]
m ∈M

x = (m)

[= [x ↦]](m)
sMPS(m)s(m)  [SVerifyLoopBody]

(_0)[x ↦]∅∅(_0)

x = (s)

⊢_0ess'_0 →

[= () t]s

_0'[= (_0)[x ↦]]_0”

x = (s)

⊢_0ess'_0 →

_0ess'_0  [SVerifyStep]

sϕ's'ϕ  [SVerifyFinal]

Selected verification rules

§.§ Example

struct List  int value; List next

predicate acyclic(List l) =
acc(l.value) * acc(l.next) *
(if l.next == NULL then true
else acyclic(l.next))

List singleton(int value)
requires true
ensures (acyclic(result) *
result != NULL)
(*@ $\cdots$ @*)

List append(List l, int value)
requires acyclic(l) * l != NULL(*@@*)
ensures acyclic(result) * result != NULL(*@@*)
unfold acyclic(l);(*@@*)
if (l.next == NULL)(*@@*)
n = singleton(value);(*@@*)
n = append(l.next, value);(*@@*)
l.next = n;(*@@*)
fold acyclic(l);(*@@*)
result = l;(*@@*)

Code and supporting declarations for appending to an acyclic linked list

We now illustrate verification of the append method defined in Figure <ref>, which appends a given value to the end of a list using recursion. The append method is ensured to be memory safe and preserve acyclicity of the list through verification. We begin with an empty state and initialize all parameters with fresh values:
[aboveskip=.25em, belowskip=0.5em,numbers=none]
(*@$\sstate_1 = \triple{\emptyset}{\senv}{\ktrue} \quad \senv = [\ttt{l} \mapsto \nu_1, \ttt{v} \mapsto \nu_2]$ @*)

Then the pre-condition acyclic(l) * l != NULL is produced:
[aboveskip=.25em, belowskip=0.5em,numbers=none]
(*@$\sstate_2 = \triple{\set{ \pair{\ttt{acyclic}}{\nu_1} }}{\senv}{\nu_1 \kneq \knull}$ @*)

Unfolding acyclic(l) (line <ref>) consumes the predicate from the state and produces its body. The body of acyclic(l) contains a logical conditional resulting in two possible execution paths for produce – one where $\nu_4$ is null and one where $\nu_4$ is not null, where $\nu_4$ is the symbolic value for l.next:
[aboveskip=.25em, belowskip=0.5em, firstnumber=17,stepnumber=17]
unfold acyclic(l);
(*@$\sstate_{A3} = \triple{\set{ \triple{\ttt{value}}{\nu_1}{\nu_3}, \triple{\ttt{next}}{\nu_1}{\nu_4} }}{\senv}{\nu_1 \kneq \knull \kand \nu_4 \keq \knull}$ @*)
(*@$\sstate_{B3} = \triple{\set{ \triple{\ttt{value}}{\nu_1}{\nu_3}, \triple{\ttt{next}}{\nu_1}{\nu_4} , \pair{\ttt{acyclic}}{\nu_4}} }{\senv}{\nu_1 \kneq \knull \kand \nu_4 \kneq \knull} $ @*)

We follow both execution paths, using color-coding to distinguish them. Next, when executing the if statement (line <ref>), we first evaluate the condition. Since l.next is framed by the state, evaluation of the condition succeeds and execution branches along the if. We first consider executing the then branch of the if, where $\nu_4 \keq \knull$ is added it to the path condition:
[aboveskip=.25em, belowskip=0.5em, firstnumber=18,stepnumber=18]
if (l.next == NULL)
(*@$\sstate_{A4} = \triple{\cdots}{\cdots}{\nu_1 \kneq \knull \kand \nu_4 \keq \knull \kand \nu_4 \keq \knull}$ @*)
(*@$\sstate_{B4} = \triple{\cdots}{\cdots}{\nu_1 \kneq \knull \kand \nu_4 \kneq \knull \kand \nu_4 \keq \knull}$ @*)

However, the path condition $\nu_1 \kneq \knull \kand \nu_4 \kneq \knull \kand \nu_4 \keq \knull$ is unsatisfiable, thus we can safely prune this execution path and only continue with the first. We proceed to symbolically execute the call to singleton (line <ref>) by consuming the (empty) pre-condition, and producing the post-condition. The result is represented by a fresh symbolic value $\nu_5$:
[aboveskip=.25em, belowskip=0.5em, firstnumber=19,stepnumber=19]
n = singleton(value);
(*@$\sstate_{A5} = \triple{\set{ \triple{\ttt{value}}{\nu_1}{\nu_3}, \triple{\ttt{next}}{\nu_1}{\nu_4}, \pair{\ttt{acyclic}}{\nu_5}} }{\senv[\ttt{n} \mapsto \nu_5]}{\nu_1 \kneq \knull \kand \nu_4 \keq \knull \kand \nu_5 \kneq \knull}$ @*)

Symbolic execution of this path then jumps to line <ref>, but to preserve code order we now demonstrate verification of the else branch (line <ref>). To do this, we use states $\sstate_{A3}$ and $\sstate_{B3}$, and add the negation of the condition to verify the else body:
[aboveskip=.25em, belowskip=0.5em,firstnumber=20,stepnumber=20]
(*@$\sstate_{A4}' = \triple{\cdots}{\cdots}{\nu_1 \kneq \knull \kand \nu_4 \keq \knull \kand \nu_4 \kneq \knull}$ @*)
(*@$\sstate_{B4}' = \triple{\set{ \triple{\ttt{value}}{\nu_1}{\nu_3}, \triple{\ttt{next}}{\nu_1}{\nu_4}, \triple{\ttt{acyclic}}{\nu_4} }}{\senv}{\nu_1 \kneq \knull \kand \nu_4 \kneq \knull}$ @*)

Here again this results in an unsatisfiable path condition $\nu_1 \kneq \knull \kand \nu_4 \keq \knull \kand \nu_4 \kneq \knull$, so we prune that path. We continue with the other path and execute the recursive call to append (line <ref>), which consumes the pre-condition (removing $\pair{\ttt{acyclic}}{\nu_4}$) and produces the post-condition, using the fresh value $\nu_6$ to represent the result (adding $\pair{\ttt{acyclic}}{\nu_6}$):
[aboveskip=.25em, belowskip=0.5em, firstnumber=21,stepnumber=21]
n = append(l.next, value);
(*@$\sstate_{B5}' = \triple{\set{ \triple{\ttt{value}}{\nu_1}{\nu_3}, \triple{\ttt{next}}{\nu_1}{\nu_4}, \pair{\ttt{acyclic}}{\nu_6}} }{\senv[\ttt{n} \mapsto \nu_6]}{\nu_1 \kneq \knull \kand \nu_4 \kneq \knull \kand \nu_6 \kneq \knull}$ @*)

Now we have completed verifying both branches of the if statement. Note that we do not actually join execution at this point; instead, we jump to line <ref> immediately after executing the program up to $\sstate_{A5}$ and $\sstate_{B5}'$ along both paths. We follow both of these paths for the rest of verification. The field assignment on line 22 consumes acc(l.next) and produces a new corresponding heap chunk with n's value:
[aboveskip=.25em, belowskip=0.5em, firstnumber=22,stepnumber=22]
l.next = n;
(*@$\sstate_{A6} = \triple{\set{ \triple{\ttt{value}}{\nu_1}{\nu_3}, \triple{\ttt{next}}{\nu_1}{\nu_5}, \pair{\ttt{acyclic}}{\nu_5}} }{\senv[\ttt{n} \mapsto \nu_5]}{\nu_1 \kneq \knull \kand \nu_4 \keq \knull \kand \nu_5 \kneq \knull}$ @*)
(*@$\sstate_{B6}' = \triple{\set{ \triple{\ttt{value}}{\nu_1}{\nu_3}, \triple{\ttt{next}}{\nu_1}{\nu_6}, \pair{\ttt{acyclic}}{\nu_6}} }{\senv[\ttt{n} \mapsto \nu_6]}{\nu_1 \kneq \knull \kand \nu_4 \kneq \knull \kand \nu_6 \kneq \knull}$ @*)

Folding acyclic results in twice the number of execution paths since it consumes acylic(l)'s body, which includes an logical conditional.
However, again, information from the path conditions in $\sstate_{A6}$ and $\sstate_{B6}'$ allow us to prune some of these paths.
We elide these pruned paths and only show the taken ones. After consuming acyclic(l)'s body, execution produces acyclic(l) into the state:
[aboveskip=.25em, belowskip=0pt, firstnumber=23,stepnumber=23]
fold acyclic(l);
(*@$\sstate_{A7} = \triple{\set{ \pair{\ttt{acyclic}}{\nu_1}} }{\senv[\ttt{n} \mapsto \nu_5]}{\nu_1 \kneq \knull \kand \nu_4 \keq \knull \kand \nu_5 \kneq \knull}$ @*)
(*@$\sstate_{B7}' = \triple{\set{ \pair{\ttt{acyclic}}{\nu_1}} }{\senv[\ttt{n} \mapsto \nu_6]}{\nu_1 \kneq \knull \kand \nu_4 \kneq \knull \kand \nu_6 \kneq \knull}$ @*)

[aboveskip=0pt, belowskip=0.5em, firstnumber=24,stepnumber=24]
result = l;
(*@$\sstate_{A8} = \triple{\set{ \pair{\ttt{acyclic}}{\nu_1}} }{\senv[\ttt{n} \mapsto \nu_5, \ttt{result} \mapsto \nu_1]}{\nu_1 \kneq \knull \kand \nu_4 \keq \knull \kand \nu_5 \kneq \knull}$ @*)
(*@$\sstate_{B8}' = \triple{\set{ \pair{\ttt{acyclic}}{\nu_1}} }{\senv[\ttt{n} \mapsto \nu_6, \kresult \mapsto \nu_1]}{\nu_1 \kneq \knull \kand \nu_4 \kneq \knull \kand \nu_6 \kneq \knull}$ @*)

Finally, in both $\sstate_{A8}$ and $\sstate_{B8}'$, we can consume the post-condition acyclic(result) * result != NULL. Therefore, we have verified all possible symbolic execution paths of append's body, and thus verified append.

reflects the core components of Viper—eval, consume, produce, and exec. We now formally define , an extension of which supports gradual specifications. We then define static verification for that allows optimistic assumptions to satisfy proof goals and generates checks to be verified at run time to cover these assumptions as in <cit.>.

Note, the syntax of differs slightly from that of (the frontend for ), particularly with its omission of C-style pointers. However, due to the restrictions of , all usages of pointers in can be translated to use object references. This and other translations are done by during its conversion to an intermediate language , which is used in the backend verifier. In order to simplify our model, is very similar to the language of , but incorporates elements of the language when this simplifies the definition of our verification algorithm.

§.§ Gradual formulas

We first extend the syntax of our language to include imprecise formulas—formulas of the form $\simprecise{\phi}$. An imprecise formula may represent any logically consistent strengthening of the precise portion $\phi$ <cit.>. For example, the imprecise formula $\simprecise{x\,\ttt{>}\,0}$ consistently implies $x \keq 2$, but does not consistently imply $x \keq 0$. Then, a gradual formula $\gform$ may be precise or imprecise, and gradual programs are programs that contain gradual formulas. The abstract syntax of extends 's syntax with gradual formulas:

𝒫    ::= p(T x)

Φ   ::=

s         ::= ⋯|es

::= ϕ|ϕ

Note, imprecise formulas are always considered self-framed, because they can always be strengthened to be self-framing. Therefore we require all method pre- and postconditions, loop invariants, and predicate bodies to be specifications—formulas which are either imprecise or self-framed.

Also, note that IDF is particularly well-suited for gradual specifications, in comparison to separation logic <cit.>, since IDF allows separately specifying access permission and heap values. This allows specification of heap values while leaving more complex accessibility assertions unspecified, as in the formula $\simprecise{\ttt{x.f} \kneq \knull}$.

§.§ Representation

In this section we extend the data structures from <ref> to support imprecise states—states in which it is permissible to make optimistic assumptions—and define our representation of run-time checks.

* A symbolic state $\sstate$ is now a quintuple $\quintuple{\imp}{\sheap}{\oheap}{\senv}{\pc}$ where $\imp$ is an imprecise flag, $\sheap$ is a precise heap, $\oheap$ is an optimistic heap, $\senv$ is the symbolic store, and $\pc$ is the path condition. As before, we use the notation $\imp(\sstate)$, $\sheap(\sstate)$, etc. to reference specific components of a symbolic state. $\senv$ and $\pc$ are defined in <ref> but we redefine the other components.

* An imprecise flag $\imp \in \set{\top, \bot}$ is a flag indicating whether a symbolic state is imprecise ($\top$) or precise ($\bot$). $\imp(\sstate)$ denotes that $\imp(\sstate) = \top$ (and thus $\sstate$ is an imprecise state), while $\neg \imp(\sstate)$ denotes that an $\imp(\sstate) = \bot$ (and thus $\sstate$ is precise). Imprecise states are produced by consuming or producing an imprecise specification. Once imprecise, a state always remains imprecise.

* A precise heap $\sheap$ is a symbolic heap as described in section <ref>. Thus it is a finite set of heap chunks where all heap chunks represent distinct locations in the heap at run time.

* An optimistic heap $\oheap$ is a finite set of field chunks. Field chunks contained in the optimistic heap may represent the same location in the heap at run time, i.e. the optimistic heap does not preserve the separation invariant like the precise heap. The optimistic heap of a well-formed symbolic state must be empty unless it is an imprecise state.

§.§ Run-time checks

A run-time check $r \in \SCheck$ denotes an assertion that validates assumptions made during static verification of imprecise programs. It is a symbolic expression, symbolic permission, pair of symbolic permission sets, or $\bot$:

$$r \quad::=\quad t \quad\mid\quad \sperm \quad\mid\quad \fsep(\sperms_1, \sperms_2) \quad\mid\quad \bot$$

A set of run-time checks is denoted $\scheck \in \powerset{\SCheck}$.
In a run-time check, a symbolic expression $t$ asserts that the value represented by $t$ at run time is $\ktrue$, a symbolic permission $\sperm$ asserts ownership of a field or a predicate instance, and a pair $\fsep(\sperms_1, \sperms_2)$ asserts that the sets of permissions represented by $\sperms_1$ and $\sperms_2$ are disjoint. $\bot$ represents a static verification failure. We represent static verification failure as an unsatisfiable run-time check, instead of failing verification entirely, to accommodate imprecision.

Note that our run-time checks contain symbolic values. This is unlike <cit.>, where checks produced have their symbolic values replaced by corresponding program variables. This replacement is needed to support the implementation of run-time checks and adds a significant amount of complexity to their algorithms. Fortunately, as we will see later, we can abstract away this connection of symbolic values to program variables (aka. concrete values) using valuations; and so we can produce abstracted checks here, avoiding additional complexity in our formalism.

Additionally, at each branch point <cit.> check whether all possible branches fail and, if so, halt static verification. We do not specify this behavior; however, this is possible by checking for $\bot \in \scheck$ at each step of symbolic execution.

§.§ Evaluating expressions

We now extend our previous judgement for symbolic evaluation from <ref> to allow optimistic symbolic evaluation of expressions. We specify a set $\scheck$ of run-time checks necessary for a given evaluation, thus our judgement is now $\seval{\sstate}{e}{t}{\sstate'}{\scheck}$.

Field chunks may be referenced in the optimistic heap by SEvalFieldOptimistic in Figure <ref>. These field chunks have already been validated, thus we do not need additional run-time checks. A field may also be optimistically evaluated by SEvalFieldImprecise, even if it does not exist in $\sheap$ or $\oheap$. This adds a new field chunk with a $\ffresh$ value to $\oheap$. This requires a run-time check which asserts permission to access the field. Finally, SEvalFieldFailure applies in a precise state when a field is referenced but no matching heap chunk exists. This results in a failure of static verification, represented by $\bot$, for that execution branch.

We also modify the existing set of rules described in <ref> to collect run-time checks from recursive evaluations. Likewise, we modify the deterministic evaluation judgement to add similar rules as those described above, allowing it to also generate run-time checks, thus its form is $\spceval{\sstate}{e}{t}{\scheck}$.

ft_e't ∈(')(') t_e' t_e

ft_e't ∈(')

(') t_e' t_e
e.ft'  [SEvalFieldImprecise]

ft_e't ∈(') ∪(')(') t_e' t_e

t =

' = () ∪ ft_et
e.ft'[= ']∪ t_ef   [SEvalFieldFailure]

ft_e't ∈(') ∪(')(') t_e' t_e

Selected rules for evaluation during gradual verification

§.§ Consuming formulas

We extend our previous judgment for consuming formulas from <ref> to handle imprecise formulas and imprecise states. As in <ref>, we add a parameter $\scheck$ to the consume judgments. Additionally, we collect all permissions for the given formula into a set of symbolic permissions $\sperms$ so that separation checks may be added where necessary. Thus the new judgments are of the form $\scons{\sstate}{\gform}{\sstate'}{\scheck}$ and $\sconsume{\sstate}{\sstate_E}{\gform}{\sstate'}{\scheck}{\sperms}$; these two forms are related by SConsume and correspond to the forms described in <ref>. We list selected rules in Figure <ref>.

Consuming an imprecise formula empties the precise and optimistic heaps (SConsumeImprecise). This is because the imprecision may represent access to arbitrary fields. For example, a method with an imprecise precondition could modify any field that the callee owns, thus we cannot make any assumptions about field permissions or values after the method returns. Consuming an imprecise formula results in an imprecise state, thus removed field chunks can be referenced optimistically, with the possible addition of a run-time check.

We must also consider the case of consuming an imprecise formula in a precise state. Since optimistic assumptions are not permitted in a precise state, we cannot assume any of the assertions contained in the imprecise formula. However, the imprecise formula may reference fields without a corresponding accessibility predicate. Thus, when consuming an imprecise formula, we use an imprecise state as the symbolic state for evaluation, but use the original (possibly precise) state for assertions.

In an imprecise state we may optimistically consume an expression, even if it is not implied by the current path condition. We then add the value as a run-time check to be asserted at run-time.

Consumption of accessibility predicates must be modified to handle imprecise states, where field chunks in $\oheap$ may overlap with field chunks in $\sheap$. We must remove all fields that may represent the same heap reference when removing a field chunk from $\sheap$. To do this, we use the helper functions $\fremfp$ and $\fremf$.
$\fremfp$ is used when removing heap chunks from the precise heap.
For precise states, $\fremfp$ removes the field chunk that coincides exactly with the heap location being consumed (thus computing the same result as the rules in <ref>).
For imprecise states, it also removes all field chunks that could possibly coincide with the specified heap location. $\fremf$ is used when removing chunks from the optimistic heap and behaves similarly, but also removes all predicate chunks, since predicates occurring in the precise heap could overlap with heap chunks in the imprecise heap.

Some optimizations could be made – for instance, if a predicate's unfolding will never reference a field $f$, we could preserve an instance of this predicate when consuming $\kacc(e.f)$. However, we leave such optimizations to future work.

We can also optimistically assume an accessibility predicate in an imprecise state, even if a matching field chunk does not exist in $\sheap$ or $\oheap$. Since this assumes ownership of the field, we add the corresponding symbolic permission to $\scheck$.
Finally, like accessibility predicates, we allow optimistic consumption of predicate instances. In this case the symbolic permission representing the predicate instance is added as a run-time check.

When consuming any accessibility predicate or predicate instance, the symbolic permission is always added to a set $\sperms$. This allows specification of checks for separation. When consuming $\kacc(x.f) * \kacc(y.f)$, if $\kacc(x.f)$ is optimistically assumed while $\kacc(y.f)$ is statically verified, the run-time check for $\kacc(x.f)$ does not imply that its permission is disjoint from that of $y.f$. Therefore additional checks for separation are added when consuming a separating conjunction such as $\phi_1 * \phi_2$. If no run-time check for permissions exists, all permissions must have been consumed from $\sheap$ or $\oheap$ and thus separation may be assumed. However, if a symbolic permission is contained in $\scheck$ we can no longer assume separation. Thus we add a run-time check $\fsep(\sperms_1, \sperms_2)$ where $\sperms_1$ is the set of symbolic permissions collected while consuming $\phi_1$ and likewise for $\sperms_2$ and $\phi_2$.

'  [SConsumeImprecise]
_E[= ⊤]ϕ'
_Eϕ⊤(')(')∅∅   [SConsumeValueImprecise]

() t
_Ee[= () t]∪t∅  [SConsumeValueFailure]

() t

() t_e' t_e

ft_e't ∈()

' = ((), , t_e, f)

' = ((), , t_e, f)

' = [= ', = ']
_E(e.f)'t_ef  [SConsumeAccOptimistic]

() t_e' t_e

ft_e't ∈()() t_e' t_e

ft_e't ∈()

' = ((), , t_e, f)

' = ((), , t_e, f)

' = [= ', = ']
_E(e.f)'t_ef  [SConsumeAccImprecise]

ft_e't ∈() ∪()() t_e' t_e

' = [= ((), , t_e, f), = ((), , t_e, f)]
_E(e.f)'∪ t_ef t_ef  [SConsumeAccFailure]

ft_e't ∈() ∪()() t_e' t_e

Selected rules for consuming gradual formulas

§.§ Producing formulas

Since a formula is only produced when we can assume its validity, producing a gradual formula does not require any optimistic assumptions, thus we do not need to calculate any run-time checks. When producing an imprecise formula, we produce the precise portion and set $\imp = \top$. All other rules from <ref> are left unchanged.

§.§ Executing statements

All rules from <ref> are left unchanged. While it may seem natural to calculate run-time checks while determining execution transitions (as in the exec algorithm of <cit.>), we found that this unnecessarily complicates statements of soundness since symbolic execution steps are not equivalent to dynamic execution steps. For example, a method call occurs in one step during symbolic execution but may never complete during dynamic execution, therefore it may be impossible to determine which symbolic execution step applies. However, assertion of run-time checks must occur before a dynamic execution step may proceed. Therefore we cleanly delineate between symbolic execution transitions, specified by the judgement $\sexec{\sstate}{s}{s'}{\sstate'}$, and the calculation of run-time checks.

§.§ Guarding execution

As described above, we must the assert run-time checks before the corresponding dynamic execution step occurs. Therefore we define guard judgements to calculate run-time checks which ensure that execution can safely proceed. A guard for a method call calculates the checks necessary to ensure that the method's pre-condition is satisfied, while a guard for a field assignment calculates the checks necessary to ensure permission to access the assignee and evaluate the value to be stored.

A guard judgement $\sguard{\vstate}{\sstate'}{\scheck}{\sperms}$ denotes that, at the execution state represented by $\vstate$, when the execution path matches the path condition in $\sstate'$, the run-time checks $\scheck$ must be checked. Selected guard rules are defined in Figure <ref>.

In a guard judgement, $\sperms$ determines the exclusion frame—a set of permissions which must not escape the executing method's context. Its necessity and behavior is explained in <ref>.

x es'∅  [SGuardAssignField]

x.f es”∪'∅  [SGuardCall]

x = (m)

'[= [x ↦t]](m)”'
y m(e)s ” ⊣

∪', (”, (m))

(,   ) :=
∅   if $\gform$ is completely precise

pt : pt ∈()   ∪

tf : ftt' ∈() ∪()      otherwise

Selected guard rules

§.§ Example

List append(List l, int value)
requires ? * true(*@  @*)
ensures ? * acyclic(result)(*@  @*)

if (l.next == NULL)(*@  @*)
n = singleton(value);(*@  @*)

else(*@  @*)
n = append(l.next, value);(*@  @*)
l.next = n;(*@  @*)
result = l;(*@  @*)
(*@  @*)

code for appending to an acyclic linked list

We now illustrate verification of the gradually-specified method in Figure <ref>. We assume the definition of List and acyclic from Figure <ref>. The gradual specification of append ensures that all returned lists are acyclic.

Symbolic states are tuples of the form $\quintuple{\imp}{\sheap}{\oheap}{\senv}{\pc}$. As in <ref>, we begin verification of append by assigning fresh symbolic values to all parameters and producing the pre-condition $\simprecise{\ktrue}$, which results in an imprecise state:
[aboveskip=.25em, belowskip=0.5em,numbers=none]
(*@$\sstate_1 = \quintuple{\top}{\emptyset}{\emptyset}{\senv}{\ktrue} \quad \senv = [\ttt{l} \mapsto \nu_1, \ttt{v} \mapsto \nu_2]$ @*)

At each statement we compute the guard to find the necessary run-time checks. The guard for the if statement at line <ref> evaluates l.next == NULL. A heap chunk for l.next is optimistically added to $\oheap$ with a fresh value $\nu_3$. This also results in a run-time check for the symbolic permission $\pair{\nu_1}{\ttt{next}}$.

The next state $\sstate_{A2}$ is computed by symbolic execution. This again evaluates l.next == NULL in the state $\sstate_1$, which again requires the addition of an optimistic heap chunk. Since $\nu_3$ was not previously used in $\sstate_1$ it can be used again as a fresh value for symbolic execution.
[aboveskip=.25em, belowskip=0.5em,firstnumber=4,stepnumber=5]
(*@$\scheck = \set{ \pair{\nu_1}{\ttt{next}}$} } @*)
if (l.next == NULL)
(*@\lightpurple{$\sstate_{A2} = \quintuple{\top}{\emptyset}{\set{\triple{\ttt{next}}{\nu_1}{\nu_3}}}{\senv}{\nu_3 \keq \knull}$} @*)
\end{lstlisting}}
The guard for line \ref{ln:imprecise-append-single} consumes the pre-condition of \ttt{singleton}, which requires no run-time checks. Symbolic execution consumes the same pre-condition and produces the post-condition; here we use the fresh value $\nu_4$ for the returned value:
\begin{lstlisting}[aboveskip=.25em, belowskip=0.5em,firstnumber=5,stepnumber=6]
(*@\lightpurple{$\scheck = \emptyset$} @*)
n = singleton(value);
(*@\lightpurple{$\sstate_{A3} = \quintuple{\top}{\set{\pair{\ttt{acyclic}}{\nu_4}}}{\set{\triple{\ttt{next}}{\nu_1}{\nu_3}}}{\senv[\ttt{n} \mapsto \nu_4]}{\nu_3 \keq \knull}$} @*)
\end{lstlisting}}
As in \S\ref{sec:static-example}, we follow code order, instead of following each execution path individually, and distinguish separate execution paths with color-coding. The guard at line \ref{ln:imprecise-append-if} computes the checks for both branches of \ttt{if}, thus the guard is not computed at line \ref{ln:imprecise-append-else}. We can symbolically execute the \ttt{else} branch by adding the negation of the path condition we used previously:
\begin{lstlisting}[aboveskip=.25em, belowskip=0.5em,firstnumber=7,stepnumber=7]
(*@\lightblue{$\sstate_{B2} = \quintuple{\top}{\emptyset}{\set{\triple{\ttt{next}}{\nu_1}{\nu_3}}}{\senv}{\nu_3 \kneq \knull}$} @*)
\end{lstlisting}}
The guard for line \ref{ln:imprecise-append-rec} consumes the pre-condition of \ttt{append}, which is $\simprecise{\ktrue}$. Since the body of this imprecise formula is only $\ktrue$, no run-time checks are necessary. However, since this is an imprecise formula, we clear the precise and optimistic heaps (\textsc{SConsumeImprecise} in Figure \ref{fig:gradual-consume-rules}). Symbolic execution then produces the post-condition; here we use the fresh value $\nu_5$ for the returned value:
\begin{lstlisting}[aboveskip=.25em, belowskip=0.5em,firstnumber=7,stepnumber=8]
(*@\lightyellow{$\scheck_B = \emptyset$} @*)
n = append(l.next, value);
(*@\lightblue{$\sstate_{B3} = \quintuple{\top}{\set{\pair{\ttt{acyclic}}{\nu_5}}}{\emptyset}{\senv[\ttt{n} \mapsto \nu_5]}{\nu_3 \kneq \knull \kand \nu_5 \kneq \knull}$} @*)
\end{lstlisting}}
We resume symbolic execution of both paths at line \ref{ln:imprecise-append-next}. Executing \ttt{l.next = n} in the state $\sstate_{A3}$ does not require any run-time checks since it contains the heap chunk representing \ttt{l.next}. However, executing the same statement in $\sstate_{B3}$ requires optimistic assumption of the symbolic permission $\pair{\ttt{next}}{\nu_1}$ which requires a run-time check and removes the predicate instance. \citet{divincenzo2022gradual} describe the implementation of such conditional run-time checks, but here we represent it with separate symbolic execution paths:
\begin{lstlisting}[aboveskip=.25em, belowskip=0pt,firstnumber=8,stepnumber=9]
(*@\lightpurple{$\scheck_A = \emptyset$}, \lightblue{$\scheck_B = \set{\pair{\ttt{next}}{\nu_1}}$} @*)
l.next = n;
(*@\lightpurple{$\sstate_{A4} = \quintuple{\top}{\set{\pair{\ttt{acyclic}}{\nu_4}}}{\set{\triple{\ttt{next}}{\nu_1}{\nu_4}}}{\senv[\ttt{n} \mapsto \nu_4]}{\nu_3 \keq \knull}$} @*)
(*@\lightblue{$\sstate_{B4} = \quintuple{\top}{\set{\triple{\ttt{next}}{\nu_1}{\nu_5}}}{\emptyset}{\senv[\ttt{n} \mapsto \nu_5]}{\nu_3 \kneq \knull \kand \nu_5 \kneq \knull}$} @*)
\end{lstlisting}
\begin{lstlisting}[aboveskip=0pt, belowskip=0.5em,firstnumber=9,stepnumber=10]
(*@\lightpurple{$\scheck_A = \emptyset$}, \lightblue{$\scheck_B = \emptyset$} @*)
result = l;
(*@\lightpurple{$\sstate_{A5} = \quintuple{\top}{\nu_3 \keq \knull}{\set{\pair{\ttt{acyclic}}{\nu_4}}}{\set{\triple{\ttt{next}}{\nu_1}{\nu_4}}}{\senv[\ttt{n} \mapsto \nu_4, \ttt{result} \mapsto \nu_1]}$} @*)
(*@\lightblue{$\sstate_{B4} = \quintuple{\top}{\nu_3 \kneq \knull \kand \nu_5 \kneq \knull}{\set{\triple{\ttt{next}}{\nu_1}{\nu_5}}}{\emptyset}{\senv[\ttt{n} \mapsto \nu_5, \ttt{result} \mapsto \nu_1]}$} @*)
\end{lstlisting}}
Finally, the applicable guard at line \ref{ln:imprecise-append-end} consumes the post-condition $\ttt{acyclic(result)}$. Since neither state contains a matching predicate instance, in both paths a run-time check is added for the symbolic permission $\pair{\ttt{acyclic}}{\nu_1}$:
\begin{lstlisting}[aboveskip=.25em, belowskip=0.5em,firstnumber=10,stepnumber=11]
(*@\lightpurple{$\scheck_A = \set{\pair{\ttt{acyclic}}{\nu_1}}$}, \lightblue{$\scheck_B = \set{\pair{\ttt{acyclic}}{\nu_1}}$} @*)
\end{lstlisting}}
Now we have verified the method and computed all necessary run-time checks.

\section{Executing \gvl}

% CZ: This should prob go somewhere else
% In addition, our aim is to prove the static verifier sound, given a sound implementation of run-time checks (we will specify soundness for run-time checks). We consider soundness of a particular implementation of run-time checks to be orthogonal to our soundness result, since showing soundness of run-time checks as they are implemented in \cite{divincenzo2022gradual} would require reasoning about source code transformations, or defining new execution semantics that depend on the calculated run-time checks.

Since soundness of static verification requires specification of program execution, we define execution semantics for \gvl programs (including \svl programs, which are a subset). This includes dynamic semantics for formulas, and execution semantics which dynamically assert the validity of every specification. Therefore, these semantics define valid execution for \gvl programs.

As explained in \S\ref{sec:introduction}, execution semantics are based on those of \co \citep{arnold2010c0}, while the semantics of formulas are based on those of \gvlrp \citep{wise2020gradual}.

\subsection{Representation}\label{sec:dynamic-representation}

In this section, we formally define the data structures used during execution of \gvl programs:

\begin{itemize}
\item A \textit{value} $v \in \Value$ is an integer, boolean, or object reference.

\item An \textit{object reference} $\ell \in \textsc{Ref}$ is an identifier for a particular object. As with symbolic values, we assume that an infinite number of distinct values can be generated by the $\ffresh$ function. The type of value represented by $\ffresh$ is disambiguated by its usage.

\item An \textit{environment} $\env$ is a partial function mapping variable names to values, i.e. $\env : \Var \pfunc \Value$.

\item A \textit{heap} $\heap : \textsc{Ref} \times \Field \to \Value$ is a function mapping object reference and field pairs to values. We assume that the heap function is total, i.e. all reference and field pairs have some corresponding value, but heap access is restricted during execution by a set of \textit{access permissions} $\perms \in \mathcal{P}(\textsc{Ref} \times \textsc{Field})$. This reflects the semantics of IDF \citep{smans2012implicit}. A heap location $\pair{\ell}{f}$ is \textit{owned} if it is contained in the currently-applicable set of access permissions.

\item A \textit{stack frame} is a triple $\triple{\perms}{\env}{s}$ containing of a set of owned permissions $\perms$, a local environment $\env$, and a statement $s$. A \textit{stack} $\stack$ is a list of stack frames -- either $\triple{\perms}{\env}{s} \cdot \stack$ for some other $\stack$, or the empty stack, denoted $\nilsym$. For a non-empty stack $\stack$, $\perms(\stack)$, $\env(\stack)$, and $s(\stack)$ refer to their respective components of the head element.

\item A \textit{dynamic state} $\Gamma$ may be a symbol $\initsym$ or $\finalsym$, or pair $\pair{\heap}{\stack}$ containing a heap $\heap$ and a non-empty stack $\stack$. $\heap(\Gamma)$ and $\stack(\Gamma)$ reference individual components of $\Gamma$ when $\Gamma$ is not a symbol, while $\perms(\Gamma)$, $\env(\Gamma)$, and $s(\Gamma)$ reference a component of the head element of $\stack(\Gamma)$. $\perms(\initsym)$ and $\heap(\initsym)$ are defined to be $\emptyset$.
\end{itemize}

\subsection{Evaluating expressions}

Given a heap $\heap$ and environment $\env$, the evaluation of expression $e$ to a value $v$ is represented by a judgement of the form $\eval{\heap}{\env}{e}{v}$. This follows standard evaluation rules---variables are evaluated to the corresponding value in $\env$ and field references are evaluated to the corresponding value in $\heap$. The boolean operators $\kand$ and $\kor$ are short-circuiting---when evaluating $e_1 \kand e_2$, $e_2$ is only evaluated when $e_1$ is not true.

\subsection{Asserting formulas}\label{sec:dynamic-formulas}

A judgement of the form $\assertion{\heap}{\perms}{\env}{\gform}$ denotes that a gradual formula $\gform$ is satisfied given a heap $\heap$, a set of accessible permissions $\perms$, and an environment $\env$. Selected rules are shown in Figure \ref{fig:dynamic-rules}. Boolean expressions are satisfied when they evaluate to true. An accessibility predicate $\kacc(e.f)$ is satisfied when the field referenced by $e.f$ is in the set of accessible permissions. A predicate instance $p(\overline{e})$ is satisfied when the predicate body is satisfied using an environment mapping each predicate parameter $x$ to the corresponding argument $e$. A separating conjunction $\phi_1 * \phi_2$ is satisfied when $\phi_1$ is satisfied using a permission set $\perms_1$ and $\phi_2$ is satisfied using a permission set $\perms_2$, where $\perms_1$ and $\perms_2$ are disjoint subsets of $\perms$. Finally, an imprecise formula $\simprecise{\phi}$ is satisfied exactly when $\phi$ is satisfied.

A judgement of the form $\frm{\heap}{\perms}{\env}{e}$ denotes that the expression $e$ is \textit{framed} by the given set of permission $\perms$. This denotes that all heap locations necessary to evaluate $e$ are included in $\perms$. Selected rules are shown in Figure \ref{fig:dynamic-rules}.

Note that a predicate instance $p(\overline{e})$ is satisfied iff the predicate body is satisfied. Thus dynamic execution of \gvl uses \textit{equirecursive} semantics for predicates \citep{summers2013formal}. We also define \textit{equirecursive framing} of formulas by the judgement $\efrm{\heap}{\perms}{\env}{\gform}$. A formula is equirecursively framed if its \emph{unrolling}, the recursive expansion of referenced predicate bodies, is framed.

A formula $\gform$ is \textit{self-framed} if $\universal{\heap, \perms, \env}{\assertion{\heap}{\perms}{\env}{\gform} \implies \efrm{\heap}{\perms}{\env}{\gform}}$. As specified in \S\ref{sec:gradual-formulas}, a specification is a formula which is imprecise or self-framed.

\subsection{Footprints}

The \emph{footprint} of a formula is the set of permissions necessary to assert a formula \cite{reynolds2002separation}. There are two types of footprints for gradual formulas:

The \emph{exact footprint} of a formula is the minimal set of permissions necessary to assert and frame a formula. Given a heap $\heap$ and environment $\env$, $\efoot{\heap}{\env}{\gform}$ denotes the exact footprint of a formula $\gform$.

The \emph{maximal footprint} (often abbreviated to \emph{footprint}) of a formula contains the exact footprint and all permissions that are consistently implied by the formula. The maximal footprint of a completely precise formula is its exact footprint, but the maximal footprint of an imprecise formula contains all accessible permissions. Given a heap $\heap$, set of owned permissions $\perms$, and environment $\env$, $\foot{\heap}{\perms}{\env}{\gform}$ denotes the maximal footprint of a formula $\gform$.

\subsection{Executing statements}\label{sec:dynamic-exec}

We represent the dynamic execution of program statements as small-step execution semantics denoted by the judgement $\dexec{\heap}{\stack}{\xperms}{\heap}{\stack}$, where the statement $s$ is executing with the initial state $\pair{\heap}{\stack}$, and then transitions to the next statement $s'$ with the new state $\pair{\heap}{\stack}$. $\xperms$ specifies the \emph{exclusion frame}, which is described below. Selected rules are shown in Figure \ref{fig:dynamic-rules}. Execution will be stuck (i.e., no further derivation will apply) when an error is encountered. For example, execution is stuck when a formula is not satisfied or if some expression is not framed.

A method call is executed by evaluating all arguments, asserting the pre-condition, and adding a new stack frame containing the footprint of the pre-condition and the method body. After the method body is completely executed, the post-condition is asserted and the $\kresult$ value in the callee's environment is passed to the caller's environment.

A loop is executed similarly to a method, but uses the loop invariant instead of a method contract. When the loop condition is true, an iteration is executed by asserting the invariant and adding a new stack frame for the loop body. When the body is complete, we return to the original loop statement, allowing further iterations as long as the condition remains true. When the condition is false, the invariant is still asserted but execution skips over the statement. These rules are specified in \supplement{the supplement \citep{supplement}}{\S\ref{sec:exec-rules}}.

$\xperms$ specifies the \textit{exclusion frame} -- a set of permissions which may not be passed to the callee or loop body. It is used only for executing method calls and loops. We later explain why this is necessary for soundness in \S\ref{sec:unsoundness}.

$\kfold$ and $\kunfold$ statements are ignored at run-time. Explicit folding and unfolding of predicate instances is not required because the run-time uses equirecursive semantics for predicates.

The entire set of possible execution steps for a program $\prog$ is determined by judgements of the form $\dtrans{\prog}{\xperms}{\Gamma}{\Gamma'}$, which denote that execution transitions from $\Gamma$ to $\Gamma'$, using the exclusion frame $\xperms$. From the $\initsym$ state, execution may only step to the entry statement, and then execution follows the rules described above.

\begin{figure}
\begin{mathpar}
\inferrule[AssertImprecise]
{ \assertion{\heap}{\perms}{\env}{\phi} \\
\efrm{\heap}{\perms}{\env}{\phi} }
{ \assertion{\heap}{\perms}{\env}{\simprecise{\phi}} } \and
\inferrule[AssertAcc]
{ \eval{\heap}{\env}{e}{\ell} \\
\pair{\ell}{f} \in \perms }
{ \assertion{\heap}{\perms}{\env}{\kacc(e.f)} } \and
\inferrule[AssertPredicate]
{ \multiple{x} = \fpredparams(p) \\
\multiple{\eval{\heap}{\env}{e}{v}} \\\\
\assertion{\heap}{\perms}{[\multiple{x \mapsto v}]}{\fpred(p)} }
{ \assertion{\heap}{\perms}{\env}{p(\multiple{e})} } \and
\inferrule[AssertConjunction]
{ \assertion{\heap}{\perms_1}{\env}{\phi_1} \\
\assertion{\heap}{\perms_2}{\env}{\phi_2} \\\\
\perms_1 \cap \perms_2 = \emptyset \\
\perms_1 \cup \perms_2 \subseteq \perms }
{ \assertion{\heap}{\perms}{\env}{\phi_1 * \phi_2} } \and
\inferrule[ExecAssignField]
{ \eval{\heap}{\env}{x}{\ell} \\
\eval{\heap}{\env}{e}{v} \\
\assertion{\heap}{\perms}{\env}{\kacc(x.f)} \\
\frm{\heap}{\perms}{\env}{e} \\
\heap' = \heap[\pair{\ell}{f} \mapsto v]}
{ \dexec{\heap}{\triple{\perms}{\env}{\sseq{x.f \kassign e}{s}} \cdot \stack}{\xperms}{\heap'}{\triple{\perms}{\env}{s} \cdot \stack} } \and
\inferrule[ExecCallEnter]
{ \multiple{x} = \fparams(m) \\
\multiple{\eval{\heap}{\env}{e}{v}} \\
\multiple{\frm{\heap}{\perms}{\env}{e}} \\\\
\env' = [\multiple{x \mapsto v}] \\
\assertion{\heap}{\perms \setminus \xperms}{\env'}{\fpre(m)} \\
\perms' = \foot{\heap}{\perms \setminus \xperms}{\env}{\fpre(m)} }
{ \dexec{\heap}{\triple{\perms}{\env}{\sseq{y = m(\multiple{e})}{s}} \cdot \stack}{\xperms}{\heap}{\triple{\perms'}{\env'}{\sseq{\fbody(m)}{\kskip}} \cdot \triple{\perms \setminus \perms'}{\env}{\sseq{y = m(\multiple{e})}{s}} \cdot \stack} } \and
\inferrule[ExecCallExit]
{ \assertion{\heap}{\perms'}{\env'}{\fpost(m)} \\
\env'' = \env[y \mapsto \env'(\kresult)] \\
\perms'' = \perms \cup \foot{\heap}{\perms'}{\env'}{\fpost(m)} }
{ \dexec{\heap}{\triple{\perms'}{\env'}{\kskip} \cdot \triple{\perms}{\env}{\sseq{y = m(\multiple{e})}{s}} \cdot \stack}{\xperms}{\heap}{\triple{\perms}{\env}{s} \cdot \stack} }
\end{mathpar}}
\caption{Selected formal rules for dynamic semantics of \gvl.}
\label{fig:dynamic-rules}
\end{figure}

\section{Correspondence}\label{sec:correspondence}

Before formalizing soundness, we must specify the correspondence between verification and dynamic states. We include invariants which depend on concrete values, such as separation, in this correspondence relation. Finally, we specify the behavior of run-time checks in a dynamic state.

\subsection{State correspondence}

A dynamic environment $\env$ \textit{models} a symbolic store $\senv$ via a valuation $V$ when $\simenv{V}{\senv}{\env}$. This denotes that $\universal{x \mapsto t \in \senv}{x \mapsto V(t) \in \env}$.

A heap $\heap$ and set of permissions $\perms$ model a precise heap $\sheap$ when $\simheap{V}{\sheap}{\heap}{\perms}$. This denotes that for all field chunks $\triple{f}{t}{t'} \in \sheap$, $\heap(V(t), f) = V(t')$ and $\pair{V(t)}{f} \in \perms$. Also, for all predicate chunks $\pair{p}{\multiple{t}}$, the corresponding predicate body is true using given arguments $\multiple{V(t)}$. Additionally, the footprint represented by each heap chunk must be disjoint.

The footprint of a heap chunk, given valuation $V$ and heap $\heap$, is denoted $\vfoot{V}{\heap}{h}$. The footprint of a field chunk $\triple{f}{t}{t'}$ is $\set{\pair{V(t)}{f}}$. The footprint of a predicate chunk $\pair{p}{\multiple{t}}$ is the exact footprint of the predicate when applied to the arguments $\multiple{V(t)}$.

$\heap$ and $\perms$ model an optimistic heap $\oheap$ when $\simheap{V}{\oheap}{\heap}{\perms}$. This has the same requirements as that for $\sheap$, except that heap chunks are allowed to overlap.

$\heap$, $\perms$, and $\perms$ model a symbolic state when $\simstate{V}{\sstate}{\heap}{\perms}{\env}$. This denotes that $\heap$ and $\perms$ model both $\sheap(\sstate)$ and $\oheap(\sstate)$, $\env$ models $\senv$, and the path condition is true---$V(\pc(\sstate)) = \ktrue$.

We also refer to these relations as correspondence---$\simstate{V}{\sstate}{\heap}{\perms}{\env}$ denotes that the symbolic state $\sstate$ \textit{corresponds} to $\heap$, $\perms$, and $\env$.

Finally, a verification state $\vstate$ corresponds to a dynamic state $\Gamma$ with valuation $V$ if $\vstate = \Gamma$ (i.e., $\vstate$ and $\Gamma$ are the same symbol), or $\simstate{V}{\sstate(\vstate)}{\heap(\heap)}{\perms(\Gamma)}{\env(\Gamma)}$ and $s(\Gamma) = s(\vstate)$. In other words, the heap and head stack frame of $\Gamma$ model the symbolic state of $\vstate$, and the statement in the head stack frame is syntactically the same statement as that of $\vstate$.

\subsection{Run-time checks}

We also define the semantics of run-time checks using valuations. The judgement $\rtassert{V}{\heap}{\perms}{r}$ denotes the assertion of a run-time check $r$, given a valuation $V$, a heap $\heap$, and a set of owned permissions $\perms$. Likewise, $\rtassert{V}{\heap}{\perms}{\scheck}$ denotes the assertion of all run-time checks contained in $\scheck$. Formal rules are given in Figure \ref{fig:rt-check-rules}.

\begin{figure}
\begin{mathpar}
\inferrule
{ V(t) = \ktrue }
{ \rtassert{V}{\heap}{\perms}{t} } \and
\inferrule
{ \pair{V(t)}{f} \in \perms }
{ \rtassert{V}{\heap}{\perms}{\pair{t}{f}} } \and
\inferrule
{ \vfoot{V}{\heap}{\sperms_1} \cap \vfoot{V}{\heap}{\sperms_2} = \emptyset }
{ \rtassert{V}{\heap}{\perms}{\fsep(\sperms_1, \sperms_2)} } \and
\inferrule
{ \assertion{\heap}{\perms}{[\multiple{x \mapsto V(t)}]}{\fpred(p)} \\\\
\multiple{x} = \fpredparams(p) }
{ \rtassert{V}{\heap}{\perms}{\pair{p}{\multiple{t}}} }
\end{mathpar}}
\caption{Rules for run-time check assertions}
\label{fig:rt-check-rules}
\end{figure}

\section{Soundness}\label{sec:soundness}

We can now state the soundness of our static verifier. We slightly modify a traditional progress/preservation statement of soundness in order to accommodate run-time checks.

\subsection{Corresponding valuations}

For most symbolic execution judgements, we define a \textit{corresponding valuation}, inspired by the valuations used in \citet{khoo10mix}. This defines how symbolic values used in the judgement are mapped to concrete values. To calculate the corresponding valuation we require an initial valuation, which defines the valuation for all symbolic values contained by the input symbolic state, and a dynamic heap, which defines the valuation for optimistically-added fields. A corresponding valuation $V'$ must extend the initial valuation $V$, i.e. $V'(t) = V(t)$ for all $t \in \dom(V)$.
%In addition, we only need to define the valuation for symbolic values. The application of a valuation to symbolic expressions is defined in \S\ref{sec:precise-representation}.

We denote the corresponding valuation for a judgement $\mathcal{J}$, initial valuation $V$, and heap $\heap$ by $V[\mathcal{J} \mid \heap]$. The definition for each judgement type is defined in \supplement{the supplement \citep{supplement}, along with the proofs for that judgement}{the appendix which contains the corresponding proofs for that judgement}. Each corresponding valuation is defined by induction on the judgement derivation, specifying the corresponding valuation for each derivation rule.  The judgment is nondeterministic if only the input state is considered, but knowing the output state resolves this nondeterminism.
When the judgement and heap are clear from context, we simply reference the \textit{corresponding valuation extending} $V$.

% The corresponding valuations are inspired by the valuations used by \citet{khoo10mix}.  However, they existentially qualify valuations in the theorem statements and define the valuation in the proof of the theorem. We have several types of judgements, each with its own notion of soundness and corresponding valuation, and certain proofs of soundness of one type depend on the specific corresponding valuation of another type. Therefore we explicitly define the corresponding valuation for each judgement so that this definition can be shared among the proofs of multiple theorems.

\subsection{Valid states}

A \textit{valid state} is a dynamic state which is completely characterized by verification states. If $\Gamma = \initsym$ this is trivially true. For a dynamic state $\pair{\heap}{\stack}$, we require that the head stack frame corresponds to a reachable verification state. We also require that all other stack frames are \textit{partially validated} by some reachable verification state.

If a stack frame is executing a method call, partial validation is characterized by the stack frame and heap modeling a reachable symbolic state for that program point, with the callee's precondition consumed.
%We require partial validation for proving soundness, but we ultimately only need the currently-executing state to model a verification state.
For the full definition refer to \supplement{\citet{supplement}}{definition \ref{def:partial-valid}}.

\subsection{Progress and preservation}

Our statement of progress is split into two parts. First, theorem \ref{thm:progress-1} states that if $\Gamma$ is a valid state and $\Gamma$ satisfies the run-time checks calculated by a guard with a path condition that matches the current dynamic state, then dynamic execution proceeds. Second, theorem \ref{thm:progress-2} states that we can always find the guard necessary to apply theorem \ref{thm:progress-1}---a guard whose path condition matches. Thus, theorem \ref{thm:progress-2} represents completeness of symbolic execution with respect to possible dynamic execution paths. Together these theorems show that, in a valid state, the only possible way for execution to be stuck is when the run-time checks cannot be asserted.

\begin{theorem}[Progress part 1] \label{thm:progress-1}
For some program $\prog$, let $\Gamma$ be some dynamic state validated by $\vstate$ and $V$. If $\sguard{\vstate}{\sstate}{\scheck}{\sperms}$, $V'$ is the corresponding valuation extending $V$, $V'(\pc(\sstate)) = \ktrue$, and $\rtassert{V'}{\heap}{\perms(\Gamma)}{\scheck}$, then $\dtrans{\prog}{\vfoot{V'}{\heap(\Gamma)}{\sperms}}{\Gamma}{\Gamma'}$ for some $\Gamma'$.
\end{theorem}

\begin{theorem}[Progress part 2] \label{thm:progress-2}
For some program $\prog$, let $\Gamma$ be some dynamic state validated by $\vstate$ and $V$. Then $\sguard{\vstate}{\sstate}{\scheck}{\sperms}$ for some $\sstate$, $\scheck$, and $\sperms$ such that $V'(\pc(\sstate)) = \ktrue$ where $V'$ is the corresponding valuation extending $V$.
\end{theorem}

Finally, our statement of preservation (theorem \ref{thm:preservation}) assumes the antecedent and conclusion of theorem \ref{thm:progress-1}---the initial state is valid and satisfies the run-time checks of some matching guard---as well as a dynamic execution step to $\Gamma'$. By theorem \ref{thm:progress-2}, we know that there is such a guard statement; i.e., we can always find the necessary set of run-time checks. Then preservation states that the resulting dynamic state $\Gamma'$ is also valid.

\begin{theorem}[Preservation] \label{thm:preservation}
For some program $\prog$, let $\Gamma$ be some dynamic state validated by $\vstate$ and $V$. If $\sguard{\vstate}{\sstate}{\scheck}{\sperms}$, $V'$ is the corresponding valuation extending $V$, $V'(\pc(\sstate)) = \ktrue$, $\rtassert{V'}{\heap}{\perms(\Gamma)}{\scheck}$, and $\dtrans{\prog}{\vfoot{V'}{\heap(\Gamma)}{\sperms}}{\Gamma}{\Gamma'}$, then $\Gamma'$ is a valid state.
\end{theorem}

Note that our assumptions for preservation require dynamic execution to not only assert the run-time checks represented symbolically by $\scheck$, but also respect the exclusion frame represented symbolically by $\sperms$.
The necessity and implications of this requirement are discussed in \S\ref{sec:unsoundness}.

Taken together, these theorems demonstrate that dynamic execution will never be stuck as long as the run-time checks calculated by static verification succeed. Further, it shows that we calculate run-time checks for all possible execution paths. Since the dynamic execution semantics ensures all necessary specifications are satisfied, this implies that the calculated run-time checks are sufficient.

\section{Challenges to formalism of static verification}

Our specification of static verification in \S\ref{sec:precise} and \S\ref{sec:gradual} is formalised using non-deterministic inference rules. This differs greatly from the specifications of \citet{schwerhoff16silicon} and \citet{divincenzo2022gradual}, which both use a CPS-style definition for algorithms.  The latter form is useful when specifying an implementation, but makes it difficult to formulate a syntactic soundness proof.
% in the style of \citet{WRIGHT199438}.
Furthermore, operational semantics allow a higher level of abstraction than pseudo-code definitions. However, we must carefully consider whether our operational semantics represent the system which is implemented.

\subsection{Previous approaches}

During development of our soundness proof, we attempted several formulations of soundness. Initially we abstractly defined a \emph{symbolic stack}---a list of symbolic states with the form of a dynamic stack. This approach allowed us to easily state correspondence of the entire dynamic state---each dynamic stack frame models a corresponding symbolic stack frame.

We found it challenging, however, to prove that this correspondence is maintained.  When the dynamic stack takes a step, we must verify that there is a corresponding symbolic stack. To address this issue, we defined an execution semantics for symbolic stacks.  Unfortunately, this increased the distance between our formalism and implementation, and now we also need to show that all symbolic states are reachable during static verification.  Perhaps due to the complexity of this approach, the proof of correspondence remained quite difficult even after defining this execution semantics.

Instead, we defined a valid state primarily by the correspondence of the currently executing dynamic stack frame with some \textit{reachable} symbolic state---a symbolic state which is computed during static verification, with no input from dynamic execution. This resulted in a much simpler definition of \textit{valid state}.

However, in order to completely prove preservation, we also must specify the behavior of intermediate stack frames -- frames contained in the dynamic stack below the currently-executing frame. Thus we provide a recursive definition for a valid \textit{partial state}. For intermediate frames containing a method call that is waiting to complete, this requires the frame to model a symbolic state that results from consuming the callee method's pre-condition from a reachable verification state. We use this to prove that the dynamic state after the method returns models the symbolic state after symbolically executing the method call.

\subsection{Verification of loops}\label{sec:loops}

Almost all of our symbolic execution rules are finitely non-deterministic. That is, given an input state, there are a finite number of derivations that can apply. This is necessary since all possible states must be computed during static verification.

While this property matches the finite branching of symbolic execution, we make an exception in the case of loops---specifically, the \textsc{SVerifyLoop} rule (Figure \ref{fig:verify-rules}). It consumes the loop pre-condition, havocs all variables modified by the loop body (i.e., replaces them with $\ffresh$ values), and produces the loop post-condition. Thus it replaces all symbolic values that could be modified by the loop body with fresh values. The loop is left in place, which means that the rule can be immediately applied again to derive yet another state. However, this is harmless because repeated applications of this rule result in isomorphic symbolic states---states which represent the same state but with different symbolic values. Since the exact symbolic values do not matter, these are equivalent states from the perspective of static verification.
% We relax this requirement in the case of loops -- specifically the \textsc{SVerifyLoop} rule. This rule symbolically executes a while loop, and leaves the while loop in place, meaning the rule can be immediately applied again.  This is harmless, however, because of the way the rule is defined.  It consumes the loop pre-condition, havocs all variables modified by the loop body (i.e. replacing them with $\ffresh$ values in the symbolic store), and produces the loop post-condition. Repeating this process results in an isomorphic symbolic state -- a state that represents the same state but with different symbolic values. Since the exact symbolic values do not matter, these are equivalent states from the perspective of static verification.  Recognizing this equivalence, our implementation does not symbolically execute a loop body more than once.
Therefore, even though we allow unbounded non-determinism, an implementation such as \gco can compute all possible states (as determined by our formal model) up to this equivalence. In other words, unbounded non-determinism is an artifact of our formalization that does not affect an implementation.

%permits an infinite number of applications, all of which result in the same statement to be executed. However, this reflects the choice of abstraction in run-time checks between our formalism and the implementation of \cite{divincenzo2022gradual}.

%In \cite{divincenzo2022gradual}, run-time checks are computed as source expressions and then inserted into the program before compilation. Thus every time a run-time check is asserted, it evaluates the expression in the current environment. \cite{divincenzo2022gradual} addresses several challenges with this approach, particularly in the case of branching.

This exception is motivated by a disconnect between our formal model and the implementation of \gco \citep{divincenzo2022gradual}.
In our formalism, run-time checks are computed as symbolic values and lack a representation in terms of the source. Furthermore, we interpret these run-time checks by means of the valuation function, which we only extend with fresh values as dynamic execution proceeds. Therefore, the references in a run-time check are fixed -- for example, the validity of a check does not change when the heap is updated, since the heap reference has already been fully evaluated against the symbolic heap.

Consider the example in Figure \ref{fig:loop-example}. A new object reference $\ell_1$ is allocated by \ttt{create} at line \ref{ln:loop-create-initial}. Then we consume the loop pre-condition $\simprecise{\ktrue}$, which results in an imprecise state with empty symbolic heaps. Thus we cannot statically assert access to \ttt{x.value} in the loop body (line \ref{ln:loop-assign}). However, we optimistically assume access and produce a run-time check representing $\kacc(\ttt{x.value})$. In our formalism, \ttt{x} is symbolically evaluated to a symbolic value $\nu_1$ and the corresponding valuation contains the mapping $\nu_1 \mapsto \ell_1$. Thus the symbolic run-time check is $\pair{\nu_1}{\ttt{value}}$, which succeeds since the dynamic state owns $\pair{\ell_1}{\ttt{value}}$. This permission is then lost when \ttt{consume} is executed (line \ref{ln:loop-consume}), but a new reference $\ell_2$ is allocated at line \ref{ln:loop-create-while}, and the dynamic environment is updated with $\ttt{x} \mapsto \ell_2$.

During the next iteration of the loop, if we directly applied the same run-time check, this would again require the run-time check $\pair{\nu_1}{\ttt{value}}$. However, this would fail since the dynamic state no longer owns $\pair{\ell_1}{\ttt{value}}$. But the run-time check should reference $\ell_2$, since the check is intended to represent $\kacc(\ttt{x.value})$, and $\ttt{x} \mapsto \ell_2$ in the dynamic state.

This contrasts with the implementation of run-time checks in \gco, which translates the symbolic checks into source expressions. For the example described, \gco directly inserts the assertion $\kacc(\ttt{x}.\ttt{value})$. The expression \ttt{x.value} is then re-evaluated every time this assertion is checked.

\textsc{SVerifyLoop} fixes this mismatch by allowing our formal model to be updated with new symbolic values. With this rule, we can continue execution using a new symbolic state where we havoc \ttt{x}, since it is modified by the loop body, and consume the loop invariant $\simprecise{\ktrue}$ again. Thus we begin with a symbolic state with empty symbolic heaps and a symbolic store containing $\ttt{x} \mapsto \nu_2$, where $\nu_2$ is a fresh value. We define a new valuation $V'$ where new symbolic values are mapped to the current dynamic state, i.e. $V'(\nu_2) = \ell_2$ since $\ttt{x} \mapsto \ell_2$ in the dynamic state. The new symbolic state is isomorphic to the state used during the initial symbolic execution, since it also began execution of the body with empty symbolic heaps. We will again optimistically evaluate \ttt{x.value}, which produces a new run-time check for the symbolic permission $\pair{\nu_2}{\ttt{value}}$, thus we will check access to $\pair{\ell_2}{\ttt{value}}$, and therefore our run-time checks succeed.

Finally, since this rule introduces \emph{more} symbolic states in our formal model, this means that our soundness theorems are stronger than they would be otherwise; i.e., the soundness result holds for strictly more cases. As our example demonstrates, we want to consider these additional cases since they are already permitted by \gco due to its source-level run-time checks. Therefore, this additional rule allows us to abstract away the re-evaluation of source-level checks, allowing us to reason with fixed symbolic values.

%Therefore, even though we allow unbounded non-determinism, we can compute all possible states at static verification, up to equivalence. Therefore completeness of static verification WRT execution paths is maintained. In other words, unbounded non-determinism is an artifact of our formalization, thus a sound implementation is possible.

\begin{figure}
\begin{minipage}[t]{.45\linewidth}
\begin{lstlisting}[name=loop-example]
Cell create()
requires true ensures ?
{ result = alloc(Cell); }

int consume(Cell c)
requires acc(c.value) ensures true
{ (*@ $\cdots$ @*) }
\end{lstlisting}
\end{minipage}
\begin{minipage}[t]{.45\linewidth}
\begin{lstlisting}[name=loop-example]
int main() {
x = create();(*@\label{ln:loop-create-initial}@*)
while (true) invariant ? * true {(*@\label{ln:loop-while-begin}@*)
x.value = 1;(*@\label{ln:loop-assign}@*)
x = create();(*@\label{ln:loop-create-while}@*)
result = 0;
\end{lstlisting}
\end{minipage}
\caption{Example illustrating the neccessity of the \textsc{SVerifyLoop} rule.}
\label{fig:loop-example}
\end{figure}

\section{Unsoundness of \gco}\label{sec:unsoundness}

While attempting to prove the soundness of \gco, we discovered that its implementation \citep{divincenzo2022gradual} allows unsound behavior, and have communicated this to the authors. This unsoundness results from the combination of imprecise specifications, static verification with isorecursive predicates, and run-time checking with equirecursive predicates.

\subsection{Example}

\begin{figure}
\begin{minipage}{.45\linewidth}
\begin{lstlisting}[name=gvc-unsound]
struct Cell { int value; }
predicate imprecise() = ? * true
void set(Cell c, int v)
requires imprecise()
ensures true
unfold imprecise();(*@\label{ln:unsound-unfold}@*)
c.value = v;(*@\label{ln:unsound-set-assign}@*)
\end{lstlisting}
\end{minipage}
\begin{minipage}{.45\linewidth}
\begin{lstlisting}[name=gvc-unsound]
int test()
requires true
ensures result == 0
fold imprecise();(*@\label{ln:unsound-fold}@*)
Cell c = alloc(Cell);(*@\label{ln:unsound-alloc}@*)
c.value = 0;(*@\label{ln:unsound-test-assign}@*)
set(c, 1);(*@\label{ln:unsound-test-set}@*)
result = c.value;(*@\label{ln:unsound-test-result}@*)
\end{lstlisting}
\end{minipage}
\caption[Example exhibiting unsoundness of \citet{divincenzo2022gradual}]
{Example exhibiting unsoundness of \citet{divincenzo2022gradual}.\protect\footnotemark}
\label{fig:unsound-example}
\end{figure}

We show an example which exhibits this behavior in Figure \ref{fig:unsound-example}. At line \ref{ln:unsound-fold} $\ttt{imprecise}()$ is folded, thus $\simprecise{\ktrue}$ is consumed, and the predicate chunk is added to the symbolic heap. At this point $\sheap = \set{\langle \ttt{imprecise} \rangle}$. In lines \ref{ln:unsound-alloc}-\ref{ln:unsound-test-assign} a new \ttt{Cell} is allocated and its value is initialized to $0$. At this point $\sheap = \set{\langle \ttt{imprecise} \rangle, \triple{\ttt{value}}{t_1}{0}}$, where $\ttt{c} \mapsto t_1$.

\footnotetext{\ttt{void} methods are used for clarity since they can be trivially translated to the formally defined grammar.}
At line \ref{ln:unsound-test-set}, the \ttt{set} method is called. Thus the precondition---\ttt{imprecise()}---is consumed, resulting in $\sheap = \set{\triple{\ttt{value}}{t_1}{0}}$. The postcondition---$\ktrue$---is then produced, which does not change the symbolic state. In this symbolic state $\ttt{c.value} \mapsto 0$. Then line \ref{ln:unsound-test-result} adds the mapping $\ttt{result} \mapsto 0$ to the symbolic store, which allows the postcondition $\kresult \keq 0$ to be consumed successfully. Now \ttt{test} is valid and no run-time checks are required in its body.  Symbolic execution of the \ttt{set} method shows that this method is also valid but requires a check representing $\kacc(\ttt{c.value})$ at line \ref{ln:unsound-test-assign}.

Now we consider dynamic execution of the \ttt{test} method. We first use no exclusion frame (i.e. using $\emptyset$ for every occurrence of $\xperms$ in the rules).

The fold at line \ref{ln:unsound-fold} is ignored, a new \ttt{Cell} is allocated and initialized at lines \ref{ln:unsound-alloc}-\ref{ln:unsound-test-assign}, and the \ttt{set} method is called at line \ref{ln:unsound-test-set}. The formula \ttt{imprecise()} is not completely precise, therefore $\foot{\heap}{\perms}{\env}{\ttt{imprecise}()} = \perms$. Thus all of the caller's owned permissions are passed to \ttt{set}. The assertion for \ttt{imprecise()} succeeds since its equirecursive unrolling is simply $\simprecise{\ktrue}$. Likewise, the assertion for $\kacc(\ttt{c.value})$ when executing line \ref{ln:unsound-set-assign} also succeeds since the required permissions were passed from \ttt{test}. After returning from \ttt{set}, $\ttt{c.value} \mapsto 1$ in the dynamic state, thus $\ttt{result} \mapsto 1$ after executing line \ref{ln:unsound-test-result}. However, the postcondition $\ttt{result} \keq 0$ cannot be asserted, therefore execution is stuck.

Since \citet{divincenzo2022gradual} does not implement an exclusion frame, execution proceeds as described above, except that only the calculated run-time checks are asserted. Therefore the \ttt{test} method returns $1$, which contradicts its contract. \citet{wise2020gradual} follows the dynamic execution behavior described above, but since it checks every assertion at run-time, execution halts and soundness is preserved.

\subsection{Diagnosis}

%Using our formalism we can precisely diagnose the issue with the verification described above.
% Our definition of a valid state requires all intermediate stack frames to model a verification state that is computed after consuming the callee's pre-condition (or loop invariant in the case of $\kwhile$). For example, let $\vstate$ be the verification state after executing lines 14-17. Then, suppose the dynamic stack has the form $\triple{\perms_2}{\env_2}{\text{(executing \ttt{set})}} \cdot \triple{\perms_1}{\env_1}{\text{(executing \ttt{test})}} \cdot \ldots$ during execution of the \ttt{set} method (after stepping into the method call at line 18).
% Our statement of soundness requires the stack frame $\triple{\perms_1}{\env_1}{\text{(executing \ttt{test})}}$ (when combined with the current heap) to model the symbolic state given by symbolically evaluation of the arguments $c$ and $1$, and consumption of $\fpre(\ttt{set})$ (in this case \ttt{imprecise()}).
As described above, the caller's permissions are passed to \ttt{set}, thus the set of permissions owned by \ttt{test} is empty during execution of \ttt{set}. But we calculated that after consuming $\fpre(\ttt{set})$ the symbolic heap still contains the field chunk representing $\ttt{c}.\ttt{value}$. Therefore heap chunks which are included in the frame of \ttt{set} during dynamic execution are not removed by consume during symbolic execution, thus symbolic execution does not accurately represent dynamic execution.
% soundness is violated since static verification determines that $\ttt{c}.\ttt{value}$ is \textit{not} included in the frame of \ttt{set}, but the corresponding permission is passed during dynamic execution.

\subsection{Possible solutions}

At first this appears to be an error of static verification, and thus we could address this by making static verification more conservative.
More specifically, we could require a stronger invariant of the precise heap: the \textit{maximal} footprint represented by predicate chunks cannot overlap. This contrasts with our current definition, where the exact footprint represented by a predicate chunk must be disjoint from that of all other predicate chunks.

For example, we could clear the symbolic heaps when consuming any formula that is not \textit{completely} precise (i.e., the recursive unfolding contains an imprecise formula). When this occurs, we would also need to use an imprecise state, so that the existence of the removed permissions can be optimistically assumed. This would result in empty symbolic heap after line \ref{ln:unsound-test-set} in Figure \ref{fig:unsound-example}, and a run-time check for the value of $\kresult$ would be required before returning from \ttt{test}, thus soundness is preserved.

This would allow maximal footprints of predicate chunks to overlap in the symbolic heap, but when consuming a predicate instance, all potentially overlapping predicate chunks would be removed. Thus, after some predicate instance is consumed, its maximal footprint would not overlap with any permission represented by a heap chunk contained in the symbolic heap.

Alternatively, we could achieve soundness by removing any predicate instance that is not completely precise when additional permissions are added to the precise heap. Similar to the previous option, we would also need to use an imprecise state when this occurs. In the example, that would (perhaps unintuitively) \emph{remove} the \ttt{imprecise()} predicate when adding permissions for the \ttt{alloc} statement. This would ensure that the maximal footprint of heap chunks in the symbolic heap never overlap.

Unfortunately, both of these options reduce the number of assertions that can be statically discharged when verifying gradual programs, thus more run-time checks would be necessary. Furthermore, the run-time checks require checking a predicate instance, which can be quite costly since this traverses the entire unfolding of the predicate.

Furthermore, allowing the predicate instance folded at line \ref{ln:unsound-fold} to affect permissions allocated afterward, at line \ref{ln:unsound-alloc}, seems counter-intuitive. This invalidates the intuitive assumption that the set of permissions represented by a folded predicate instqance will not change while it remains folded. Furthermore this behavior breaks the semantics of \ttt{?}, as specified in \citet{wise2020gradual}, since no logically consistent strengthening of the \ttt{imprecise} predicate allows it to include permissions allocated after its body is folded.

This indicates that the semantics of dynamic execution should be modified to exclude access permission for \ttt{c.value}, which is allocated after \ttt{imprecise()} is folded, from being passed to \ttt{set}, which is a precise formula that only requires \ttt{imprecise()}. Then execution would fail at line \ref{ln:unsound-set-assign} in Figure \ref{fig:unsound-example}. To accomplish this, we have introduced the concept of an \emph{exclusion frame} -- a set of permissions which cannot be passed to a callee. This exclusion frame is calculated by symbolic execution, and passed to dynamic execution in much the same way as run-time checks. It is represented by $\sperms$ in the guard judgement (\S\ref{fig:gradual-guard-rules}), which also calculates $\scheck$, and is translated to dynamic permissions using a valuation.

The guard rules in Figure \ref{fig:gradual-guard-rules} calculate the exclusion frame by the $\frem$ helper function, after consuming the pre-condition of a method. If the pre-condition is completely precise, then $\sperms = \emptyset$, thus execution of an \svl program is not affected. Otherwise, $\sperms$ contains all permissions currently contained in the symbolic heaps. In Figure \ref{fig:unsound-example}, since the pre-condition of \ttt{set} is not completely precise, $\sperms = \set{ \pair{t_1}{\ttt{value}} }$ when calculating the guard statement at line \ref{ln:unsound-test-set}. At run-time this is translated to $\xperms = \set{ \pair{\ell}{\ttt{value}} }$ where $\ttt{c} \mapsto \ell$. Then all permissions \textit{except} $\pair{\ell}{\ttt{value}}$ are passed to \ttt{set}. Thus the run-time check for $\ttt{acc(c.value)}$ at line \ref{ln:unsound-set-assign} cannot be asserted.

This addresses the intuitive and semantic problems described above. The isorecursive instance of \ttt{imprecise} referenced in the pre-condition of \ttt{set} \textit{should not} represent access to $\ttt{c.value}$ since it was folded before \ttt{c} was allocated. Under this interpretation we would expect a failure at line \ref{ln:unsound-set-assign}, since \ttt{set} does not require the necessary permissions. This also matches the semantics of \ttt{?}, as defined in \cite{wise2020gradual}, since the predicate instance folded at line \ref{ln:unsound-fold} cannot consistently imply access to the heap location allocated at line \ref{ln:unsound-alloc}.

%Finally, we prove in lemma \cz{appendix lemma} that an assertion of a formula which has been consumed can be asserted without relying on permissions in the exclusion frame. Thus the permissions eliminated by the exclusion frame will not result in a run-time failure when asserting the method's pre-condition. Instead, if a failure occurs due to the exclusion frame, it must occur in the method's implementation. \cz{Unsure of the usefulness of this paragraph}

\subsection{Implementation}

There are important implementation challenges that must be addressed before this change can be implemented in \gco \citep{divincenzo2022gradual}. Currently, \gco constructs sets of permissions at run-time---before calling a method, for example---by recursively unfolding the neccessary specification and collecting all permissions. However, this method cannot be used to create the exclusion frame, since these permissions are not necessarily represented by a specification. But we expect that a translation algorithm can be developed which generates the source code necessary to compute the exclusion frame at run time. This is similar to the existing translation algorithm described by \citet{divincenzo2022gradual}, which translates symbolic run-time checks into source code that implements the desired assertion.

Also, note that we calculate the exclusion frame using information from symbolic execution of a particular statement. In other words, if method \ttt{m} calls $\ttt{m}'$, we can calculate the exclusion frame necessary for calling $\ttt{m}'$ without considering the exclusion frame used to call \ttt{m}. This implies that exclusion frames can be dropped when entering a completely precise method, and then instantiated again when a precise method calls an imprecise method. This is similar to how \gco does not pass permission sets to precise methods, but reconstructs the permissions when a precise method calls an imprecise methods. Applying this technique to exclusion frames, as described, would ensure that exclusion frames do not affect the run-time performance of methods that are specified with completely precise specifications.

% CONRAD: I think this is actually incorrect, based on Jenna's implementation work
%When a method's contract is completely precise, \gco optimizes run-time performance by not passing a set of permissions. Instead, the set of accessible permissions is dynamically constructed when necessary using permissions calculated during symbolic execution.

%However, the exclusion frame affects the callee and all methods called during execution of the callee. Therefore it must be passed to all method calls, and the permissions it includes must be excluded when constructing a set of permissions dynamically, even for methods with a completely precise contract. It is unclear how this will affect the run-time performance that is evaluated in \cite{divincenzo2022gradual}. It may be possible to implement this exclusion frame by using system- or runtime-level facilities to mark a memory region inaccessible. It remains to be seen how often an exclusion frame is necessary in practice, or the performance impact of an exclusion frame on practical programs. The evaluation methods used in \cite{divincenzo2022gradual} could be used to evaluate possible implementation strategies.

\section{Future work}\label{sec:future-work}

There are many possible directions in which this work can be extended.
% As we noted previously, our work does not demonstrate the soundness of the run-time check implementations described in \cite{divincenzo2022gradual}. We have precisely formalized the necessary semantics of such checks, thus the gradual verifier could be proven sound end-to-end if the implementation was proven to adhere to these semantics.
% %Likewise, we have not evaluated the performance of the soundness fix that we described in \S\ref{sec:unsoundness}. This could be evaluated by the techniques used for evaluation in \cite{divincenzo2022gradual}.
We have not yet proven the gradual guarantees for gradual verification, as formalized in \citet{wise2020gradual}. These guarantees formalize the notion that, given a valid program, gradual specifications may be used in place of all static specifications without introducing errors (both during verification and at run time). This ensures that any errors do not arise from imprecision, but rather from an invalid program or specification, or (for precise specifications) from incompleteness of verification. Our formalization appears to satisfy this since, as described in \S\ref{sec:gradual}, we extend the underlying static verification algorithm mainly by adding optimistic capabilities while leaving the bulk of static verification intact. However, we have not completed a formal proof.

%As noted in \S\ref{sec:gradual-rt-checks}, we encode failure of static verification for a particular execution branch with the run-time check $\bot$. However, we do not define overall failure of static verification. \gco does implement an overall static failure of

Our formalization could also be used to extend gradual verification. Notably, gradual verification has not been implemented for quantified specifications or concurrent programs. Ghost code/parameters (i.e., code only necessary for supporting logical proofs) is also not supported in gradual verification, since the ``ghost'' code could be necessary for run-time checks. Our high-level definition of the gradual verifier could enable further development to support these techniques. Likewise, our formalization does not capture several important concepts in Viper such as domains, fractional permissions, and joining of symbolic execution paths. Formalizing the usage of these techniques in Viper and proving their soundness would provide further assurance of the correctness of Viper and provide a starting point for integrating these techniques with gradual verification. Our formalization provides a basis for formally proving properties of verification techniques (in our case, gradual verification) with a model that closely resembles the implementation (in our case, \gco). Thus modifications to our formal model can be more easily implemented and used, while modifications to the implementation can be reflected in the formal model and proven sound.

%Finally, we investigated a machine-checked proof but found this quite difficult due to our specific proof strategies, such as our usage of partial functions. However, a machine-checked proof could enable future extension, particularly if an extensible approach could be developed. A proof of soundness for Viper could be composed with translation and execution semantics for a specific front-end to yield a proof of soundness for a Viper frontend such as Prusti \cite{astrauskas2022prusti}, similar to our result for \gco.

\section{Related work}

As mentioned previously, implementations of verification using symbolic execution, such as Viper \cite{schwerhoff16silicon}, \gco \cite{divincenzo2022gradual}, Smallfoot \cite{berdine2006smallfoot}, Chalice \cite{leino2009chalice}, and jStar \cite{distefano2008jstar}, often lack formal soundness proofs. A notable exception is VeriFast \cite{jacobs2011verifast}, which implements verification using symbolic execution. The core of its verifier was proven sound in \citet{jacobs2015featherweight}. This soundness proof utilizes techniques from abstract interpretation, which may simplify proofs of verifiers using symbolic execution. However, VeriFast uses separation logic instead of IDF.

Several previous verifiers using WLP or verification condition generation (VCG) have been directly proven sound \citep{vogels2009machine, vogels2010machine, herms2012certified, smans2012implicit}. Several similar verifiers produce a proof during verification which may be checked to the validate soundness of an individual verification result \citep{filliatre2013why3, parthasarathy2021formally}.

Viper \citep{viper16} and \gco \citep{divincenzo2022gradual} rely on an SMT solver to implement their verification algorithms. While we have proved soundness of our formal model, this soundness is contingent on the soundness of the SMT solver. Other work has extended soundness to include soundness of the entire verification system. Notably, VeriSmall \citep{verismall22}, Diaframe \citep{diaframe22}, and RefinedC \citep{refinedc21} are all encoded in Iris/Coq, making them either foundational or self-verifying.

As described before, soundness of gradual verification based on WLP has been proven in both \citet{wise2020gradual} and \citet{bader2018gradual}. However, \citet{wise2020gradual} depends on dynamically checking all assertions, while \citet{bader2018gradual} does not handle abstract heap predicates.

\section{Conclusion}

The recent implementation of gradual verification in \citet{divincenzo2022gradual} promises a dramatic reduction in the effort required to verify programs. However, this requires confidence in the correctness of their gradual verification system, \gco, as well as its underlying static verification system, Viper. In this work, we formalized symbolic execution in (a subset of) Viper and proved it sound, in addition to formalizing gradual verification in \gco and proving it sound. During this work we found a soundness bug in \gco, which we communicated to \citet{divincenzo2022gradual} along with possible solutions. This illustrates that, while correctness in gradual verifiers can be guaranteed, it should not be assumed without rigorous proof. There are a few interesting directions we could take this work: (1) proving that \gco adheres to the gradual guarantee as formalized by \citet{wise2020gradual}, which is a very important property of gradual verifiers that should be straightforward to prove with our formal system, and (2) using our formalism to explore new directions in gradual verification like quantification or concurrency, and prove systems utilizing them sound. In general, we hope that this work serves as a strong basis for future proof work in static and gradual verification when using symbolic execution.

\begin{acks}
We thank Jana Dunfield for her helpful feedback.

This work was supported by the
\grantsponsor{NSF}{National Science Foundation}{https://www.nsf.gov/}
under Grant No. \grantnum[https://www.nsf.gov/awardsearch/showAward?AWD_ID=1901033]{NSF}{CCF-1901033}
and a \grantsponsor{Google}{Google PhD Fellowship}{https://research.google/outreach/phd-fellowship/}.
\end{acks}

\clearpage

%% Bibliography
%%% -*-BibTeX-*-
%%% Do NOT edit. File created by BibTeX with style
%%% ACM-Reference-Format-Journals [18-Jan-2012].

\begin{thebibliography}{29}

%%% ====================================================================
%%% NOTE TO THE USER: you can override these defaults by providing
%%% customized versions of any of these macros before the \bibliography
%%% command.  Each of them MUST provide its own final punctuation,
%%% except for \shownote{}, \showDOI{}, and \showURL{}.  The latter two
%%% do not use final punctuation, in order to avoid confusing it with
%%% the Web address.
%%% To suppress output of a particular field, define its macro to expand
%%% to an empty string, or better, \unskip, like this:
%%% \newcommand{\showDOI}[1]{\unskip}   % LaTeX syntax
%%% \def \showDOI #1{\unskip}           % plain TeX syntax
%%% ====================================================================

\ifx \showCODEN    \undefined \def \showCODEN     #1{\unskip}     \fi
\ifx \showDOI      \undefined \def \showDOI       #1{#1}\fi
\ifx \showISBNx    \undefined \def \showISBNx     #1{\unskip}     \fi
\ifx \showISBNxiii \undefined \def \showISBNxiii  #1{\unskip}     \fi
\ifx \showISSN     \undefined \def \showISSN      #1{\unskip}     \fi
\ifx \showLCCN     \undefined \def \showLCCN      #1{\unskip}     \fi
\ifx \shownote     \undefined \def \shownote      #1{#1}          \fi
\ifx \showarticletitle \undefined \def \showarticletitle #1{#1}   \fi
\ifx \showURL      \undefined \def \showURL       {\relax}        \fi
% The following commands are used for tagged output and should be
% invisible to TeX
\providecommand\bibfield[2]{#2}
\providecommand\bibinfo[2]{#2}
\providecommand\natexlab[1]{#1}
\providecommand\showeprint[2][]{arXiv:#2}

\bibitem[Arnold(2010)]%
\bibfield{author}{\bibinfo{person}{Rob Arnold}.}
\bibinfo{year}{2010}\natexlab{}.
\newblock \emph{\bibinfo{title}{C0, an Imperative Programming Language for
Novice Computer Scientists}}.
\newblock \bibinfo{thesistype}{Master's\ thesis}. \bibinfo{school}{Department
of Computer Science, Carnegie Mellon University}.
\newblock
\urldef\tempurl%
\url{http://reports-archive.adm.cs.cmu.edu/anon/anon/usr/ftp/home/ftp/2010/CMU-CS-10-145.pdf}
\showURL{%
\tempurl}

\bibitem[Astrauskas et~al\mbox{.}(2022)]%
\bibfield{author}{\bibinfo{person}{Vytautas Astrauskas}, \bibinfo{person}{Aurel
B{\'{\i}}l{\'{y}}}, \bibinfo{person}{Jon{\'{a}}s Fiala},
\bibinfo{person}{Zachary Grannan}, \bibinfo{person}{Christoph Matheja},
\bibinfo{person}{Peter M{\"{u}}ller}, \bibinfo{person}{Federico Poli}, {and}
\bibinfo{person}{Alexander~J. Summers}.} \bibinfo{year}{2022}\natexlab{}.
\newblock \showarticletitle{The Prusti Project: Formal Verification for Rust}.
In \bibinfo{booktitle}{\emph{{NASA} Formal Methods - 14th International
Symposium, {NFM} 2022, Pasadena, CA, USA, May 24-27, 2022, Proceedings}}
\emph{(\bibinfo{series}{Lecture Notes in Computer Science},
\bibfield{editor}{\bibinfo{person}{Jyotirmoy~V. Deshmukh},
\bibinfo{person}{Klaus Havelund}, {and} \bibinfo{person}{Ivan Perez}} (Eds.).
\bibinfo{publisher}{Springer}, \bibinfo{pages}{88--108}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-031-06773-0\_5}
\showDOI{\tempurl}

\bibitem[Bader et~al\mbox{.}(2018)]%
\bibfield{author}{\bibinfo{person}{Johannes Bader}, \bibinfo{person}{Jonathan
Aldrich}, {and} \bibinfo{person}{{\'{E}}ric Tanter}.}
\bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{Gradual Program Verification}. In
\bibinfo{booktitle}{\emph{Verification, Model Checking, and Abstract
Interpretation - 19th International Conference, {VMCAI} 2018, Los Angeles,
CA, USA, January 7-9, 2018, Proceedings}} \emph{(\bibinfo{series}{Lecture
Notes in Computer Science}, Vol.~\bibinfo{volume}{10747})},
\bibfield{editor}{\bibinfo{person}{Isil Dillig} {and} \bibinfo{person}{Jens
Palsberg}} (Eds.). \bibinfo{publisher}{Springer}, \bibinfo{pages}{25--46}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-319-73721-8\_2}
\showDOI{\tempurl}

\bibitem[Berdine et~al\mbox{.}(2005)]%
\bibfield{author}{\bibinfo{person}{Josh Berdine}, \bibinfo{person}{Cristiano
Calcagno}, {and} \bibinfo{person}{Peter~W. O'Hearn}.}
\bibinfo{year}{2005}\natexlab{}.
\newblock \showarticletitle{Smallfoot: Modular Automatic Assertion Checking
with Separation Logic}. In \bibinfo{booktitle}{\emph{Formal Methods for
Components and Objects, 4th International Symposium, {FMCO} 2005, Amsterdam,
The Netherlands, November 1-4, 2005, Revised Lectures}}
\emph{(\bibinfo{series}{Lecture Notes in Computer Science},
Vol.~\bibinfo{volume}{4111})}, \bibfield{editor}{\bibinfo{person}{Frank~S.
de~Boer}, \bibinfo{person}{Marcello~M. Bonsangue}, \bibinfo{person}{Susanne
Graf}, {and} \bibinfo{person}{Willem~P. de~Roever}} (Eds.).
\bibinfo{publisher}{Springer}, \bibinfo{pages}{115--137}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/11804192\_6}
\showDOI{\tempurl}

\bibitem[Blom et~al\mbox{.}(2017)]%
\bibfield{author}{\bibinfo{person}{Stefan Blom}, \bibinfo{person}{Saeed
Darabi}, \bibinfo{person}{Marieke Huisman}, {and} \bibinfo{person}{Wytse
Oortwijn}.} \bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{The VerCors Tool Set: Verification of Parallel and
Concurrent Software}. In \bibinfo{booktitle}{\emph{Integrated Formal Methods
- 13th International Conference, {IFM} 2017, Turin, Italy, September 20-22,
2017, Proceedings}} \emph{(\bibinfo{series}{Lecture Notes in Computer
Science}, Vol.~\bibinfo{volume}{10510})},
\bibfield{editor}{\bibinfo{person}{Nadia Polikarpova} {and}
\bibinfo{person}{Steve~A. Schneider}} (Eds.). \bibinfo{publisher}{Springer},
\bibinfo{pages}{102--110}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-319-66845-1\_7}
\showDOI{\tempurl}

\bibitem[Distefano and Parkinson(2008)]%
\bibfield{author}{\bibinfo{person}{Dino Distefano} {and}
\bibinfo{person}{Matthew~J. Parkinson}.} \bibinfo{year}{2008}\natexlab{}.
\newblock \showarticletitle{JStar: Towards Practical Verification for Java}.
\newblock \bibinfo{journal}{\emph{SIGPLAN Not.}} \bibinfo{volume}{43},
\bibinfo{number}{10} (\bibinfo{date}{oct} \bibinfo{year}{2008}),
\bibinfo{pages}{213--226}.
\newblock
\showISSN{0362-1340}
\urldef\tempurl%
\url{https://doi.org/10.1145/1449955.1449782}
\showDOI{\tempurl}

\bibitem[DiVincenzo et~al\mbox{.}(2022)]%
\bibfield{author}{\bibinfo{person}{Jenna DiVincenzo}, \bibinfo{person}{Ian
McCormack}, \bibinfo{person}{Hemant Gouni}, \bibinfo{person}{Jacob
Gorenburg}, \bibinfo{person}{Mona Zhang}, \bibinfo{person}{Conrad Zimmerman},
\bibinfo{person}{Joshua Sunshine}, \bibinfo{person}{{\'{E}}ric Tanter}, {and}
\bibinfo{person}{Jonathan Aldrich}.} \bibinfo{year}{2022}\natexlab{}.
\newblock \bibinfo{title}{Gradual C0: Symbolic Execution for Efficient Gradual
\newblock
\newblock
\showeprint[arxiv]{2210.02428}~[cs.LO]

\bibitem[Eilers and M{\"{u}}ller(2018)]%
\bibfield{author}{\bibinfo{person}{Marco Eilers} {and} \bibinfo{person}{Peter
M{\"{u}}ller}.} \bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{Nagini: {A} Static Verifier for Python}. In
\bibinfo{booktitle}{\emph{Computer Aided Verification - 30th International
Conference, {CAV} 2018, Held as Part of the Federated Logic Conference, FloC
2018, Oxford, UK, July 14-17, 2018, Proceedings, Part {I}}}
\emph{(\bibinfo{series}{Lecture Notes in Computer Science},
Vol.~\bibinfo{volume}{10981})}, \bibfield{editor}{\bibinfo{person}{Hana
Chockler} {and} \bibinfo{person}{Georg Weissenbacher}} (Eds.).
\bibinfo{publisher}{Springer}, \bibinfo{pages}{596--603}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-319-96145-3\_33}
\showDOI{\tempurl}

\bibitem[Filli{\^{a}}tre and Paskevich(2013)]%
\bibfield{author}{\bibinfo{person}{Jean{-}Christophe Filli{\^{a}}tre} {and}
\bibinfo{person}{Andrei Paskevich}.} \bibinfo{year}{2013}\natexlab{}.
\newblock \showarticletitle{Why3 - Where Programs Meet Provers}. In
\bibinfo{booktitle}{\emph{Programming Languages and Systems - 22nd European
Symposium on Programming, {ESOP} 2013, Held as Part of the European Joint
Conferences on Theory and Practice of Software, {ETAPS} 2013, Rome, Italy,
March 16-24, 2013. Proceedings}} \emph{(\bibinfo{series}{Lecture Notes in
Computer Science}, Vol.~\bibinfo{volume}{7792})},
\bibfield{editor}{\bibinfo{person}{Matthias Felleisen} {and}
\bibinfo{person}{Philippa Gardner}} (Eds.). \bibinfo{publisher}{Springer},
\bibinfo{pages}{125--128}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-642-37036-6\_8}
\showDOI{\tempurl}

\bibitem[Garcia et~al\mbox{.}(2016)]%
\bibfield{author}{\bibinfo{person}{Ronald Garcia}, \bibinfo{person}{Alison~M.
Clark}, {and} \bibinfo{person}{\'{E}ric Tanter}.}
\bibinfo{year}{2016}\natexlab{}.
\newblock \showarticletitle{Abstracting Gradual Typing}.
\newblock  (\bibinfo{year}{2016}), \bibinfo{pages}{429--442}.
\newblock
\showISBNx{9781450335492}
\urldef\tempurl%
\url{https://doi.org/10.1145/2837614.2837670}
\showDOI{\tempurl}

\bibitem[Herms et~al\mbox{.}(2012)]%
\bibfield{author}{\bibinfo{person}{Paolo Herms}, \bibinfo{person}{Claude
March{\'{e}}}, {and} \bibinfo{person}{Benjamin Monate}.}
\bibinfo{year}{2012}\natexlab{}.
\newblock \showarticletitle{A Certified Multi-prover Verification Condition
Generator}. In \bibinfo{booktitle}{\emph{Verified Software: Theories, Tools,
Experiments - 4th International Conference, {VSTTE} 2012, Philadelphia, PA,
USA, January 28-29, 2012. Proceedings}} \emph{(\bibinfo{series}{Lecture Notes
in Computer Science}, Vol.~\bibinfo{volume}{7152})},
\bibfield{editor}{\bibinfo{person}{Rajeev Joshi}, \bibinfo{person}{Peter
M{\"{u}}ller}, {and} \bibinfo{person}{Andreas Podelski}} (Eds.).
\bibinfo{publisher}{Springer}, \bibinfo{pages}{2--17}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-642-27705-4\_2}
\showDOI{\tempurl}

\bibitem[Hoare(1969)]%
\bibfield{author}{\bibinfo{person}{C.~A.~R. Hoare}.}
\bibinfo{year}{1969}\natexlab{}.
\newblock \showarticletitle{An Axiomatic Basis for Computer Programming}.
\newblock \bibinfo{journal}{\emph{Commun. ACM}} \bibinfo{volume}{12},
\bibinfo{number}{10} (\bibinfo{date}{oct} \bibinfo{year}{1969}),
\bibinfo{pages}{576--580}.
\newblock
\showISSN{0001-0782}
\urldef\tempurl%
\url{https://doi.org/10.1145/363235.363259}
\showDOI{\tempurl}

\bibitem[Jacobs et~al\mbox{.}(2011)]%
\bibfield{author}{\bibinfo{person}{Bart Jacobs}, \bibinfo{person}{Jan Smans},
\bibinfo{person}{Pieter Philippaerts}, \bibinfo{person}{Fr{\'{e}}d{\'{e}}ric
Vogels}, \bibinfo{person}{Willem Penninckx}, {and} \bibinfo{person}{Frank
Piessens}.} \bibinfo{year}{2011}\natexlab{}.