Semiautomated Reasoning About Nondeterminism in C Expressions
Abstract
Research into C verification often ignores that the C standard leaves the evaluation order of expressions unspecified, and assigns undefined behavior to writewrite or readwrite conflicts in subexpressions—so called “sequence point violations”. These aspects should be accounted for in verification because C compilers exploit them.
We present a verification condition generator (vcgen) that enables one to semiautomatically prove the absence of undefined behavior in a given C program for any evaluation order. The key novelty of our approach is a symbolic execution algorithm that computes a frame at the same time as a postcondition. The frame is used to automatically determine how resources should be distributed among subexpressions.
We prove correctness of our vcgen with respect to a new monadic definitional semantics of a subset of C. This semantics is modular and gives a concise account of nondeterminism in C.
We have implemented our vcgen as a tactic in the Coq interactive theorem prover, and have proved correctness of it using a separation logic for the new monadic definitional semantics of a subset of C.
1 Introduction
The ISO C standard [22]—the official specification of the C language—leaves many parts of the language semantics either unspecified (e.g., the order of evaluation of expressions), or undefined (e.g., dereferencing a NULL pointer or integer overflow). In case of undefined behavior a program may do literally anything, e.g., it may crash, or it may produce an arbitrary result and sideeffects. Therefore, to establish the correctness of a C program, one needs to ensure that the program has no undefined behavior for all possible choices of nondeterminism due to unspecified behavior.
One may expect that these programs can be easily ruled out statically using some form of static analysis, but this is not the case. Contrary to the simple program above, one can access the values of arbitrary pointers, making it impossible to statically establish the absence of writewrite or readwrite conflicts. Besides, one should not merely establish the absence of undefined behavior due to conflicting accesses to the same locations, but one should also establish that there are no other forms of undefined behavior (e.g., that no NULL pointers are dereferenced) for any evaluation order.

The rules are not algorithmic, and hence it is not clear how they could be implemented as part of an automated or interactive tool.

It is difficult to extend the logic with new features. Soundness was proven with respect to a monolithic and adhoc model of separation logic.
In this paper we address both of these problems.
We present a new algorithm for symbolic execution in separation logic. Contrary to ordinary symbolic execution in separation logic [5], our symbolic executor takes an expression and a precondition as its input, and computes not only the postcondition, but also simultaneously computes a frame that describes the resources that have not been used to prove the postcondition. The frame is used to infer the pre and postconditions of adjacent subexpressions. For example, in Open image in new window , we use the frame of Open image in new window to symbolically execute Open image in new window .
In order to enable semiautomated reasoning about C programs, we integrate our symbolic executor into a verification condition generator (vcgen). Our vcgen does not merely turn programs into proof goals, but constructs the proof goals only as long as it can discharge goals automatically using our symbolic executor. When an attempt to use the symbolic executor fails, our vcgen will return a new goal, from which the vcgen can be called back again after the user helped out. This approach is useful when integrated into an interactive theorem prover.
We prove soundness of the symbolic executor and verification condition generator with respect to a refined version of the separation logic by Krebbers [29, 30]. Our new logic has been developed on top of the Iris framework [24, 25, 26, 33], and thereby inherits all advanced features of Iris (like its expressive support for ghost state and invariants), without having to model these explicitly. To make our new logic better suited for proving the correctness of the symbolic executor and verification condition generator, our new logic comes with a weakest precondition connective instead of Hoare triples as in Krebbers’s original logic.
To streamline the soundness proof of our new program logic, we give a new monadic definitional translation of a subset of C relevant for nondeterminism and sequence points into an MLstyle functional language with concurrency. Contrary to the direct style operational semantics for a subset of C by Krebbers [29, 30], our approach leads to a semantics that is both easier to understand, and easier to extend with additional language features.
We have mechanized our whole development in the Coq interactive theorem prover. The symbolic executor and verification condition generator are defined as computable functions in Coq, and have been integrated into tactics in the Iris Proof Mode/MoSeL framework [32, 34]. To obtain endtoend correctness, we mechanized the proofs of soundness of our symbolic executor and verification condition generator with respect to our new separation logic and new monadic definitional semantics for a subset of C. The Coq development is available at [18].

We define \(\lambda \mathsf {MC} \): a small Cstyle language with a semantics by a monadic translation into an MLstyle functional language with concurrency (Sect. 2);

We present a separation logic with weakest preconditions for \(\lambda \mathsf {MC} \) based on the separation logic for nondeterminism in C by Krebbers [29, 30] (Sect. 3);

We prove soundness of our separation logic with weakest preconditions by giving a modular model using the Iris framework [24, 25, 26, 33] (Sect. 4);

We present a new symbolic executor that not only computes the postcondition of a C expression, but also a frame, used to determine how resources should be distributed among subexpressions (Sect. 5);

On top of our symbolic executor, we define a verification condition generator that enables semiautomated proofs using an interactive theorem prover (Sect. 6);

We demonstrate that our approach can be implemented and proved sound using Coq for a superset of the \(\lambda \mathsf {MC} \) language considered in this paper (Sect. 7).
2 \(\lambda \mathsf {MC} \): A Monadic Definitional Semantics of C
In this section we describe a small Cstyle language called \(\lambda \mathsf {MC} \), which features nondeterminism in expressions. We define its semantics by translation into a MLstyle functional language with concurrency called HeapLang.
We briefly describe the \(\lambda \mathsf {MC} \) source language (Sect. 2.1) and the HeapLang target language (Sect. 2.2) of the translation. Then we describe the translation scheme itself (Sect. 2.3). We explain in several steps how to exploit concurrency and monadic programming to give a concise and clear definitional semantics.
2.1 The Source Language \(\lambda \mathsf {MC} \)
The sequenced bind operator Open image in new window generalizes the normal sequencing operator Open image in new window of C by binding the result of Open image in new window to the variable \(\mathtt {x}\) in Open image in new window . As such, Open image in new window can be thought of as the declaration of an immutable local variable \(\mathtt {x}\). We omit mutable local variables for now, but these can be easily added as an extension to our method, as shown in Sect. 7. We write Open image in new window for a sequenced bind Open image in new window in which we do not care about the return value of Open image in new window .
To focus on the key topics of the paper—nondeterminism and the sequence point restriction—we take a minimalistic approach and omit most other features of C. Notably, we omit nonlocal control (return, break, continue, and goto). Our memory model is simplified; it only supports structs with two fields (tuples), but no arrays, unions, or machine integers. In Sect. 7 we show that some of these features (arrays, pointer arithmetic, and mutable local variables) can be incorporated.
2.2 The Target Language HeapLang
2.3 The Monadic Definitional Semantics of \(\lambda \mathsf {MC} \)
We now give the semantics of \(\lambda \mathsf {MC} \) by translation into HeapLang. The translation is carried out in several stages, each iteration implementing and illustrating a specific aspect of C. First, we model nondeterminism in expressions by concurrency, parallelizing execution of subexpressions (step 1). After that, we add checks for sequence point violations in the translation of the assignment and dereferencing operations (step 2). Finally, we add function calls and demonstrate how the translation can be simplified using a monadic notation (step 3).
Step 2: Sequence Points. So far we have not accounted for undefined behavior due to sequence point violations. For instance, the program Open image in new window gets translated into a HeapLang expression that updates the value of the location Open image in new window nondeterministically to either 3 or 4, and returns 7. However, in C, the behavior of this program is undefined, as it exhibits a sequence point violation: there is a write conflict for the location Open image in new window .
Step 3: Noninterleaved Function Calls. As the final step, we present the correct translation scheme for function calls. Unlike the other expressions, function calls are not interleaved during the execution of subexpressions [22, 6.5.2.2p10]. For instance, in the program Open image in new window the possible orders of execution are: either all the instructions in Open image in new window followed by all the instructions in Open image in new window , or all the instructions in Open image in new window followed by all the instructions in Open image in new window .
To model this, we execute each function call atomically. In the previous step we used a global mutex for guarding the access to the environment. We could use that mutex for function calls too. However, reusing a single mutex for entering each critical section would not work because a body of a function may contain invocations of other functions. To that extent, we use multiple mutexes to reflect the hierarchical structure of function calls.
To handle multiple mutexes, each C expression is interpreted as a HeapLang function that receives a mutex and returns its result. That is, each C expression is modeled by a monadic expression in the reader monad Open image in new window . For consistency’s sake, we now also use the monad to thread through the reference to the environment ( Open image in new window ), instead of using a global variable Open image in new window as we did in the previous step.
A global function definition Open image in new window is translated as a top level letbinding. A function call is then just an atomically executed function invocation in HeapLang, modulo the fact that the function pointer and the arguments are computed in parallel. In addition, sequence points occur at the beginning of each function call and at the end of each function body [22, Annex C], and we reflect that in our translation by clearing the environment at appropriate places.
Our semantics by translation can easily be extended to cover other features of C, e.g., a more advanced memory model (see Sect. 7). However the fragment presented here already illustrates the challenges that nondeterminism and sequence point violations pose for verification. In the next section we describe a logic for reasoning about the semantics by translation given in this section.
3 Separation Logic with Weakest Preconditions for \(\lambda \mathsf {MC} \)
In this section we present a separation logic with weakest precondition propositions for reasoning about \(\lambda \mathsf {MC} \) programs. The logic tackles the main features of our semantics—nondeterminism in expressions evaluation and sequence point violations. We will discuss the highlevel rules of the logic pertaining to C connectives by going through a series of small examples.
The logic presented here is similar to the separation logic by Krebbers [29], but it is given in a weakest precondition style, and moreover, it is constructed synthetically on top of the separation logic framework Iris [24, 25, 26, 33], whereas the logic by Krebbers [29] is interpreted directly in a bespoke model.
As is common, Hoare triples Open image in new window are syntactic sugar for Open image in new window . The weakest precondition connective Open image in new window states that the program Open image in new window is safe (the program has defined behavior), and if Open image in new window terminates to a value \(\mathtt {\mathtt {v}}\), then \(\mathtt {\mathtt {v}}\) satisfies the predicate Open image in new window . We write Open image in new window for Open image in new window .
 1.
We do not have to manipulate the preconditions explicitly, e.g., by applying the consequence rule to the precondition.
 2.
The soundness of our symbolic executor (Theorem 5.1) can be stated more concisely using weakest precondition propositions.
 3.
It is more convenient to integrate weakest preconditions into the Iris Proof Mode/MoSeL framework in Coq that we use for our implementation (Sect. 7).
To see how one can use the rule wpbinop , let us verify Open image in new window . That is, we want to show that Open image in new window satisfies the postcondition Open image in new window assuming the precondition P. This goal can be proven by separating the precondition P into disjoint parts Open image in new window . Then using wpbinop the goal can be reduced to proving Open image in new window for \(i \in \{0,1\}\), and Open image in new window for any return values Open image in new window of the expressions Open image in new window .
However, the rule above is unsound, because it fails to account for sequence point violations. We could use the rule above to prove safety of undefined programs, e.g., the program Open image in new window .
4 Soundness of Weakest Preconditions for \(\lambda \mathsf {MC} \)
In this section we prove adequacy of the separation logic with weakest preconditions for \(\lambda \mathsf {MC} \) as presented in Sect. 3. We do this by giving a model using the Iris framework that is structured in a similar way as the translation that we gave in Sect. 2. This translation consisted of three layers: the target HeapLang language, the monadic combinators, and the \(\lambda \mathsf {MC}\) operations themselves. In the model, each corresponding layer abstracts from the details of the previous layer, in such a way that we never have to break the abstraction of a layer. At the end, putting all of this together, we get the following adequacy statement:
Theorem 4.1
(Adequacy of Weakest Preconditions). If Open image in new window is derivable, then Open image in new window has no undefined behavior for any evaluation order. In other words, Open image in new window does not assert false.
 1.
Because our translation targets HeapLang, we start by recalling the separation logic with weakest preconditions, for HeapLang part of Iris (Sect. 4.1).
 2.
On top of the logic for HeapLang, we define a notion of weakest preconditions Open image in new window for expressions Open image in new window built from our monadic combinators (Sect. 4.2).
 3.
Next, we define the lockable pointsto connective Open image in new window using Iris’s machinery for custom ghost state (Sect. 4.3).
 4.
Finally, we define weakest preconditions for \(\lambda \mathsf {MC} \) by combining the weakest preconditions for monadic expressions with our translation scheme (Sect. 4.4).
4.1 Weakest Preconditions for HeapLang
4.2 Weakest Preconditions for Monadic Expressions
Using this definition we derive the monadic rules in Fig. 5. In a monad, the expression evaluation order is made explicit via the bind operation Open image in new window . To that extent, contrary to HeapLang, we no longer have a rule like wp _{hl} bind , which allows to bind an expression in a general evaluation context. Instead, we have the rule wpbind , which reflects that the only evaluation context we have is the monadic bind Open image in new window .
4.3 Modeling the Heap
The monadic rules in Fig. 5 are expressive enough to derive some of the \(\lambda \mathsf {MC} \)level rules, but we are still missing one crucial part: handling of the heap. In order to do that, we need to define lockable pointsto connectives Open image in new window in such a way that they are linked to the HeapLang pointsto connectives Open image in new window .
The key idea is the following. The environment invariant \(\mathsf {env\_inv}\) of monadic weakest preconditions will track all HeapLang pointsto connectives Open image in new window that have ever been allocated at the \(\lambda \mathsf {MC}\) level. Via Iris ghost state, we then connect this knowledge to the lockable pointsto connectives Open image in new window . We refer to the construction that allows us to carry this out as the lockable heap. Note that the description of lockable heap is fairly technical and requires an understanding of the ghost state mechanism in Iris.
4.4 Deriving the \(\lambda \mathsf {MC} \) Rules
To model weakest preconditions for \(\lambda \mathsf {MC}\) (Fig. 3) we compose the construction we have just defined with the translation of Sect. 2 Open image in new window Here, Open image in new window is the obvious lifting of Open image in new window from \(\lambda \mathsf {MC} \) values to HeapLang values. Using the rules from Figs. 5 and 6 we derive the highlevel \(\lambda \mathsf {MC} \) rules without unfolding the definition of the monadic Open image in new window .
Example 4.2
Consider the rule wpstore for assignments Open image in new window . Using wpbind and wppar , the soundness of wpstore can be reduced to verifying the assignment with Open image in new window being \(\mathtt {l}\), Open image in new window being \(\mathtt {\mathtt {v}}'\), under the assumption Open image in new window . We use wpatomicenv to turn our goal into a HeapLang weakest precondition proposition and to gain access an environment \({\textit{env}}\), and to the proposition \(\mathsf {env\_inv}({\textit{env}})\), from which we extract the lockable heap \(\sigma \). We then use heapupd to get access to the underlying HeapLang location and obtain that Open image in new window is not locked according to \(\sigma \). Due to the environment invariant, we obtain that Open image in new window is not in \({\textit{env}}\), which allows us to prove the Open image in new window for sequence point violation in the interpretation of the assignment. Finally, we perform the physical update of the location.
5 A Symbolic Executor for \(\lambda \mathsf {MC} \)
In order to turn our program logic into an automated procedure, it is important to have rules for weakest preconditions that have an algorithmic form. However, the rules for binary operators in our separation logic for \(\lambda \mathsf {MC} \) do not have such a form. Take for example the rule wpbinop for binary operators Open image in new window . This rule cannot be applied in an algorithmic manner. To use the rule one should supply the postconditions for Open image in new window and Open image in new window , and frame the resources from the context into two disjoint parts. This is generally impossible to do automatically.
To address this problem, we first describe how the rules for binary operators can be transformed into algorithmic rules by exploiting the notion of symbolic execution [5] (Sect. 5.1). We then show how to implement these algorithmic rules as part of an automated symbolic execution procedure (Sect. 5.2).
5.1 Rules for Symbolic Execution
5.2 An Algorithm for Symbolic Execution

Open image in new window sets the entry Open image in new window to Open image in new window ;

Open image in new window removes the entry Open image in new window from Open image in new window ;

Open image in new window merges the symbolic heaps Open image in new window and Open image in new window in such a way that for each Open image in new window , we have: Open image in new window
With this representation of propositions, we define the symbolic execution algorithm as a partial function Open image in new window , which satisfies the specification stated in Sect. 5.1, i.e., for which the following holds:
Theorem 5.1
Given an expression Open image in new window and an symbolic heap Open image in new window , if Open image in new window returns a tuple Open image in new window , then Open image in new window
The algorithm proceeds by case analysis on the expression Open image in new window . In each case, the expected output is described by the equation Open image in new window . The results of the intermediate computations appear on separate lines under the clause “ Open image in new window ”. If one of the corresponding equations does not hold, e.g., a recursive call fails, then the failure is propagated. Let us now explain the case for the assignment operator.
If Open image in new window is an assignment operator Open image in new window , we first evaluate Open image in new window and then Open image in new window . Fixing the order of symbolic execution from left to right does not compromise the nondeterminism underlying the C semantics of binary operators. Indeed, when Open image in new window , we evaluate the expression Open image in new window , using the frame \(m_1\), i.e., only the resources of \(m\) that remain after the execution of Open image in new window . When Open image in new window , with Open image in new window Open image in new window , and Open image in new window , the function Open image in new window checks whether Open image in new window contains the write permission Open image in new window . If this holds, it removes the location Open image in new window , so that the write permission is now consumed. Finally, we merge Open image in new window with the output heap \(m_3^o\), so that after assignment, the write permission Open image in new window is given back in a locked state.
6 A Verification Condition Generator for \(\lambda \mathsf {MC} \)
To establish correctness of programs, we need to prove goals Open image in new window . To prove such a goal, one has to repeatedly apply the rules for weakest preconditions, intertwined with logical reasoning. In this section we will automate this process for \(\lambda \mathsf {MC} \) by means of a verification condition generator (vcgen).
It should come as no surprise that we can automate this process, by applying rules, such as the one we have given above, recursively, and threading through symbolic heaps. Formally, we do this by defining the vcgen as a total function: Open image in new window where Open image in new window is the type of propositions of our logic. The definition of \(\mathsf {vcg} \) is given in Fig. 8. Before explaining the details, let us state its correctness theorem:
Theorem 6.1
This theorem reflects the general shape of the rules we previously described. We start off with a goal Open image in new window , and after using the vcgen, we should prove that the generated goal follows from \(P'\). It is important to note that the continuation in the vcgen is not only parameterized by the return value, but also by a symbolic heap corresponding to the resources that remain. To get these resources back, the vcgen is initiated with the continuation Open image in new window .
Most clauses of the definition of the vcgen (Fig. 8) follow the approach we described so far. For unary expressions like load we generate a condition that corresponds to the weakest precondition rule. For binary expressions, we symbolically execute either operand, and proceed recursively in the other. There are a number of important bells and whistles that we will discuss now.
Handling Failure. In the case of binary operators Open image in new window , it could be that the symbolic executor fails on both Open image in new window and Open image in new window , because neither of the arguments were of the right shape (i.e., not an element of \(\overline{\mathsf {expr}}\)), or the required resources were not present in the symbolic heap. In this case the vcgen generates the goal of the form Open image in new window where Open image in new window . What appears here is that the current symbolic heap Open image in new window is given back to the user, which they can use to prove the weakest precondition of Open image in new window by hand. Through the postcondition Open image in new window the user can resume the vcgen, by choosing a new symbolic heap \(m'\) and invoking the continuation Open image in new window .
For assignments Open image in new window we have a similar situation. Symbolic execution of both Open image in new window and Open image in new window may fail, and then we generate a goal similar to the one for binary operators. If the location Open image in new window that we wish to assign to is not in the symbolic heap, we use the continuation Open image in new window As before, the user gets back the current symbolic heap \(\llbracket m \rrbracket \), and could resume the vcgen through the postcondition Open image in new window by picking a new symbolic heap.
7 Discussion
Extensions of the Language. The memory model that we have presented in this paper was purposely oversimplified. In Coq, the memory model for \(\lambda \mathsf {MC} \) additionally supports mutable local variables, arrays, and pointer arithmetic. Adding support for these features was relatively easy and required only local changes to the definitional semantics and the separation logic.
For implementing mutable local variables, we tag each location with a Boolean that keeps track of whether it is an allocated or a local variable. That way, we can forbid deallocating local variables using the \(\mathtt {free}\texttt {(} \mathtt {}\texttt {)}\) operator.
Our extended memory model is block/offsetbased like CompCert’s memory model [38]. Pointers are not simply represented as locations, but as pairs \((\ell , i)\), where \(\ell \) is a HeapLang reference to a memory block containing a list of values, and i is an offset into that block. The pointsto connectives of our separation logic then correspondingly range over block/offsetbased pointers.
To temporarily transfer resources into the invariant, one can use the first rule. Because function calls are not interleaved, one can use the last rule to gain access to the shared resource invariant for the duration of the function call.
Krebbers could only prove that Open image in new window returns 0, 3 or 4, whereas we can prove it returns 3 or 4 by combining resource invariants with Iris’s ghost state.

Defined \(\lambda \mathsf {MC} \) with the extensions described above, as well as the monadic combinators, as a shallow embedding on top of Iris’s HeapLang [21, 25].

Modeled the separation logic for \(\lambda \mathsf {MC} \) and the monadic combinators as a shallow embedding on top of the Iris’s program logic for HeapLang.

Implemented the symbolic executor and vcgen as computable Coq functions, and proved their soundness w.r.t. our separation logic.

Turned the verification condition generator into a tactic that integrates into the Iris Proof Mode/MoSeL framework [32, 34].
This last point allowed us to leverage the existing machinery for separation logic proofs in Coq. Firstly, we get basic building blocks for implementing the vcgen tactic for free. Secondly, when the vcgen is unable to solve the goal, one can use the Iris Proof Mode/MoSeL tactics to help out in a convenient manner.
To implement the symbolic executor and vcgen, we had to reify the terms and values of \(\lambda \mathsf {MC} \). To see why reification is needed, consider the data type for symbolic heaps, which uses locations as keys. In proofs, those locations appear as universally quantified variables. To compute using these, we need to reify them into some symbolic representation. We have implemented the reification mechanism using type classes, following Spitters and van der Weegen [47].
We proved Open image in new window in 11 lines of Coq code. The vcgen can automatically process the program up until the while loop. At that point, the user has to manually perform an induction on the array, providing a suitable induction hypothesis. The vcgen is then able to discharge the base case automatically. In the inductive case, it will automatically process the program until the next iteration of the while loop, where the user has to apply the induction hypothesis.
8 Related Work
C Semantics. There has been a considerable body of work on formal semantics for the C language, including several large projects that aimed to formalize substantial subsets of C [17, 20, 30, 37, 41, 44], and projects that focused on specific aspects like its memory model [10, 13, 27, 28, 31, 38, 40, 41], weak memory concurrency [4, 36, 43], nonlocal control flow [35], verified compilation [37, 48], etc.
The focus of this paper—nondeterminism in C expressions—has been treated formally a number of times, notably by Norrish [44], Ellison and Rosu [17], Krebbers [31], and Memarian et al. [41]. The first three have in common that they model the sequence point restriction by keeping track of the locations that have been written to. The treatment of sequence points in our definitional semantics is closely inspired by the work of Ellison and Rosu [17], which resembles closely what is in the C standard. Krebbers [31] used a more restrictive version of the semantics by Ellison and Rosu—he assigned undefined behavior in some corner cases to ease the soundness theorem of his logic. We directly proved soundness of the logic w.r.t. the more faithful model by Ellison and Rosu.
Memarian et al. [41] give a semantics to C by elaboration into a language they call Core. Unspecified evaluation order in Core is modeled using an unseq operation, which is similar to our \(\mathbin {_{\textsf {\tiny HL}}}\) operation. Compared to our translation, Core is much closer to C (it has function calls, memory operations, etc. as primitives, while we model them with monadic combinators), and supports concurrency.
Reasoning Tools and Program Logics for C. Apart from formalizing the semantics of C, there have been many efforts to create reasoning tools for the C language in one way or another. There are standalone tools, like VeriFast [23], VCC [12], and the Jessie plugin of FramaC [42], and there are tools built on top of general purpose proof assistants like VST [1, 10] in Coq, or AutoCorres [19] in Isabelle/HOL. Although, admittedly, all of these tools cover larger subsets of C than we do, as far as we know, they all ignore nondeterminism in expressions.
There are a few exceptions. Norrish proved confluence for a certain class of C expressions [45]. Such a confluence result may be used to justify proofs in a tool that does not have an underlying nondeterministic semantics.

We have proved soundness with respect to a definitional semantics for a subset of C. We believe that this approach is more modular, since the semantics can be specified at a higher level of abstraction.

We have built our logic on top of the Iris framework. This makes the development more modular (since we can use all the features as well as the Coq infrastructure of Iris) and more expressive (as shown in Sect. 7).

There was no automation like our vcgen, so one had to subdivide resources between subexpressions manually all the time. Also, there was not even tactical support for carrying out proofs manually. Our logic is redesigned to get such support from the Iris Proof Mode/MoSeL framework.
To handle missing features of C as part of our vcgen, we plan to explore approaches by other verification projects in proof assistants. A notable example of such a project is VST, which supports machine arithmetic [16] and data types like structs and unions [10] as part of its tactics for symbolic execution.
Separation Logic and Symbolic Execution. In their seminal work, Berdine et al. [5] demonstrate the application of symbolic execution to automated reasoning in separation logic. In their setting, frame inference is used to perform symbolic execution of function calls. The frame has to be computed when the call site has more resources than needed to invoke a function. In our setting we compute frames for subexpressions, which, unlike functions, do not have predefined specifications. Due to that, we have to perform frame inference simultaneously with symbolic execution. The symbolic execution algorithm of Berdine et al. can handle inductive predicates, and can be extended with shape analysis [15]. We do not support such features, and leave them to future work.
Caper [14] is a tool for automated reasoning in concurrent separation logic, and it also deals with nondeterminism, although the nature of nondeterminism in Caper is different. Nondeterminism in Caper arises due to branching on unknown conditionals and due to multiple possible ways to apply ghost state related rules (rules pertaining to abstract regions and guards). The former cause is tackled by considering sets of symbolic execution traces, and the latter is resolved by employing heuristics based on biabduction [9]. Applications of abductive reasoning to our approach to symbolic execution are left for future work.
Recently, Bannister et al. [2, 3] proposed a new separation logic connective for performing forwards reasoning whilst avoiding frame inference. This approach, however, is aimed at sequential deterministic programs, focusing on a notion of partial correctness that allows for failed executions. Another approach to verification of sequential stateful programs is based on characteristic formulae [11]. A stateful program is transformed into a higherorder logic predicate, implicitly encoding the frame rule. The resulting formula is then proved by a user in Coq.
When implementing a vcgen in a proof assistant (see e.g., [10, 39]) it is common to let the vcgen return a new goal when it gets stuck, from which the user can help out and call back the vcgen. The novelty of our work is that this approach is applied to operations that are called in parallel.
Footnotes
 1.
And righttoleft, although our monadic translation does not rely on that.
Notes
Acknowledgments
We are grateful to Gregory Malecha and the anonymous reviewers and for their comments and suggestions. This work was supported by the Netherlands Organisation for Scientific Research (NWO), project numbers STW.14319 (first and second author) and 016.Veni.192.259 (third author).
References
 1.Appel, A.W. (ed.): Program Logics for Certified Compilers. Cambridge University Press, New York (2014)zbMATHGoogle Scholar
 2.Bannister, C., Höfner, P.: False failure: creating failure models for separation logic. In: Desharnais, J., Guttmann, W., Joosten, S. (eds.) RAMiCS 2018. LNCS, vol. 11194, pp. 263–279. Springer, Cham (2018). https://doi.org/10.1007/9783030021498_16CrossRefGoogle Scholar
 3.Bannister, C., Höfner, P., Klein, G.: Backwards and forwards with separation logic. In: Avigad, J., Mahboubi, A. (eds.) ITP 2018. LNCS, vol. 10895, pp. 68–87. Springer, Cham (2018). https://doi.org/10.1007/9783319948218_5CrossRefGoogle Scholar
 4.Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: POPL, pp. 55–66 (2011)Google Scholar
 5.Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52–68. Springer, Heidelberg (2005). https://doi.org/10.1007/11575467_5CrossRefGoogle Scholar
 6.Birkedal, L., Bizjak, A.: Lecture Notes on Iris: HigherOrder Concurrent Separation Logic, August 2018. https://irisproject.org/tutorialmaterial.html
 7.Bornat, R., Calcagno, C., O’Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: POPL, pp. 259–270 (2005)Google Scholar
 8.Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003). https://doi.org/10.1007/3540448985_4CrossRefGoogle Scholar
 9.Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional shape analysis by means of biabduction. J. ACM 58(6), 26:1–26:66 (2011)MathSciNetCrossRefGoogle Scholar
 10.Cao, Q., Beringer, L., Gruetter, S., Dodds, J., Appel, A.W.: VSTFloyd: a separation logic tool to verify correctness of C programs. JAR 61(1–4), 367–422 (2018)MathSciNetCrossRefGoogle Scholar
 11.Charguéraud, A.: Characteristic formulae for the verification of imperative programs. SIGPLAN Not. 46(9), 418–430 (2011)CrossRefGoogle Scholar
 12.Cohen, E., et al.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009). https://doi.org/10.1007/9783642033599_2CrossRefGoogle Scholar
 13.Cohen, E., Moskal, M., Tobies, S., Schulte, W.: A precise yet efficient memory model for C. ENTCS 254, 85–103 (2009)Google Scholar
 14.DinsdaleYoung, T., da Rocha Pinto, P., Andersen, K.J., Birkedal, L.: Caper  automatic verification for finegrained concurrency. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 420–447. Springer, Heidelberg (2017). https://doi.org/10.1007/9783662544341_16CrossRefGoogle Scholar
 15.Distefano, D., O’Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287–302. Springer, Heidelberg (2006). https://doi.org/10.1007/11691372_19CrossRefzbMATHGoogle Scholar
 16.Dodds, J., Appel, A.W.: Mostly sound type system improves a foundational program verifier. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 17–32. Springer, Cham (2013). https://doi.org/10.1007/9783319035451_2CrossRefGoogle Scholar
 17.Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: POPL, pp. 533–544 (2012)Google Scholar
 18.Frumin, D., Gondelman, L., Krebbers, R.: Semiautomated reasoning about nondeterminism in C expressions: Coq development, February 2019. https://cs.ru.nl/~dfrumin/wpc/
 19.Greenaway, D., Lim, J., Andronick, J., Klein, G.: Don’t sweat the small stuff: formal verification of C code without the pain. In: PLDI, pp. 429–439 (2014)Google Scholar
 20.Hathhorn, C., Ellison, C., Roşu, G.: Defining the undefinedness of C. In: PLDI, pp. 336–345 (2015)Google Scholar
 21.Iris: Iris Project, November 2018. https://irisproject.org/
 22.ISO: ISO/IEC 9899–2011: Programming Languages  C. ISO Working Group 14 (2012)Google Scholar
 23.Jacobs, B., Smans, J., Piessens, F.: A quick tour of the VeriFast program verifier. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 304–311. Springer, Heidelberg (2010). https://doi.org/10.1007/9783642171642_21CrossRefGoogle Scholar
 24.Jung, R., Krebbers, R., Birkedal, L., Dreyer, D.: Higherorder ghost state. In: ICFP, pp. 256–269 (2016)Google Scholar
 25.Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higherorder concurrent separation logic. J. Funct. Program. 28, e20 (2018). https://doi.org/10.1017/S0956796818000151MathSciNetCrossRefzbMATHGoogle Scholar
 26.Jung, R., et al.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: POPL, pp. 637–650 (2015)Google Scholar
 27.Kang, J., Hur, C., Mansky, W., Garbuzov, D., Zdancewic, S., Vafeiadis, V.: A formal C memory model supporting integerpointer casts. In: POPL, pp. 326–335 (2015)Google Scholar
 28.Krebbers, R.: Aliasing restrictions of C11 formalized in Coq. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 50–65. Springer, Cham (2013). https://doi.org/10.1007/9783319035451_4CrossRefGoogle Scholar
 29.Krebbers, R.: An operational and axiomatic semantics for nondeterminism and sequence points in C. In: POPL, pp. 101–112 (2014)Google Scholar
 30.Krebbers, R.: The C standard formalized in Coq. Ph.D. thesis, Radboud University Nijmegen (2015)Google Scholar
 31.Krebbers, R.: A formal C memory model for separation logic. JAR 57(4), 319–387 (2016)MathSciNetCrossRefGoogle Scholar
 32.Krebbers, R., et al.: MoSeL: a general, extensible modal framework for interactive proofs in separation logic. PACMPL 2(ICFP), 77:1–77:30 (2018)Google Scholar
 33.Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.H., Dreyer, D., Birkedal, L.: The Essence of higherorder concurrent separation logic. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 696–723. Springer, Heidelberg (2017). https://doi.org/10.1007/9783662544341_26CrossRefGoogle Scholar
 34.Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higherorder concurrent separation logic. In: POPL, pp. 205–217 (2017)Google Scholar
 35.Krebbers, R., Wiedijk, F.: Separation logic for nonlocal control flow and block scope variables. In: Pfenning, F. (ed.) FoSSaCS 2013. LNCS, vol. 7794, pp. 257–272. Springer, Heidelberg (2013). https://doi.org/10.1007/9783642370755_17CrossRefzbMATHGoogle Scholar
 36.Lahav, O., Vafeiadis, V., Kang, J., Hur, C., Dreyer, D.: Repairing Sequential Consistency in C/C++11. In: PLDI, pp. 618–632 (2017)Google Scholar
 37.Leroy, X.: Formal verification of a realistic compiler. CACM 52(7), 107–115 (2009)CrossRefGoogle Scholar
 38.Leroy, X., Blazy, S.: Formal verification of a Clike memory model and its uses for verifying program transformations. JAR 41(1), 1–31 (2008)MathSciNetCrossRefGoogle Scholar
 39.Malecha, G.: Extensible proof engineering in intensional type theory. Ph.D. thesis, Harvard University (2014)Google Scholar
 40.Memarian, K., et al.: Exploring C semantics and pointer provenance. PACMPL 3(POPL), 67:1–67:32 (2019)Google Scholar
 41.Memarian, K., et al.: Into the depths of C: elaborating the De Facto Standards. In: PLDI, pp. 1–15 (2016)Google Scholar
 42.Moy, Y., Marché, C.: The Jessie Plugin for Deduction Verification in FramaC, Tutorial and Reference Manual (2011)Google Scholar
 43.Nienhuis, K., Memarian, K., Sewell, P.: An operational semantics for C/C++11 concurrency. In: OOPSLA, pp. 111–128 (2016)Google Scholar
 44.Norrish, M.: C Formalised in HOL. Ph.D. thesis, University of Cambridge (1998)Google Scholar
 45.Norrish, M.: Deterministic expressions in C. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 147–161. Springer, Heidelberg (1999). https://doi.org/10.1007/354049099X_10CrossRefGoogle Scholar
 46.O’Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1), 271–307 (2007). Festschrift for John C. Reynolds’s 70th birthdayMathSciNetCrossRefGoogle Scholar
 47.Spitters, B., Van der Weegen, E.: Type classes for mathematics in type theory. Math. Struct. Comput. Sci. 21(4), 795–825 (2011)MathSciNetCrossRefGoogle Scholar
 48.Stewart, G., Beringer, L., Cuellar, S., Appel, A.W.: Compositional CompCert. In: POPL, pp. 275–287 (2015)Google Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.