ABSTRACT. Data flow proofs, which are classically based on data flow graphs, bear a promising practical potential for automatic verification. We base a fundamental investigation of data flow proofs on the notion of a data flow tree, which allows us to capture data flow at a finer level of granularity than data flow graphs. In particular, we characterize the exact relation between the data flow in actual executions and the data flow represented by the data flow graph.

ABSTRACT. Counterexamples, execution traces of the system that illustrate how an error state is reachable from the initial state, are essential for understanding verification failures. They are one of the most important features of Model Checkers which distinguish them from Abstract Interpretation and other Static Analysis techniques by providing a user with an actionable information to debug their system and/or the specification. While in Hardware and Protocol verification, the counterexamples are re-playable in the system, in Software Model Checking, counterexamples take a form of a textual report (often presented as a semi-structured document). This is problematic since it complicates the debugging process by not allowing to use existing processes and tools such as debuggers, delta-debuggers, fault localization, fault minimization, etc.

In this paper, we argue that the most useful form of a counterexample is an \emph{executable harness} that can be linked with the code under analysis (CUA) to produce an executable that exhibits the fault witnessed by the counterexample. A harness is different from a unit test since it can control CUA directly bypassing potentially complex logic that interprets program inputs. This makes harnesses easier to construct compared to complete unit tests. We describe harness generation that we have developed in the SeaHorn verification framework. We identify key challenges for generating harness from Model Checking counterexamples of complex memory manipulating programs that use many third party libraries and external calls. We validate our prototype on the verification benchmarks from Linux Device Drivers in SV-COMP. Finally, we discuss many of the open challenges and suggests avenues for future work.

ABSTRACT. We have previously described a novel fully automated program verification system called VIAP primarily for verifying the safety properties of programs with integer assignments. In this paper, we extend it to programs with arrays. Our extension is not restricted to single dimensional arrays but general and works for multidimensional and nested arrays as well. In the most recent \textit{SV-COMP} 2018 competition, VIAP with array extension came in second in the ReachSafety-Arrays sub-category, behind \textit{VeriAbs}.

ABSTRACT. Abstract. In this paper we present an algorithm for bounded model-checking with SMT solvers of programs with library functions — either standard or user-defined. Typically, if the program correctness depends on the output of a library function, the model-checking process either treats this function as an uninterpreted function, or is required to use a theory under which the function in question is fully defined. The former approach leads to numerous spurious counter-examples, whereas the later faces the danger of the state-explosion problem, where the resulting formula is too large to be solved by means of modern SMT solvers.

We extend the approach of user-defined summaries and propose to represent the set of existing summaries for a given library function as a lattice of subsets of summaries, with the meet and join operations defined as intersection and union, respectively. The refinement process is then triggered by the lattice traversal, where in each node the SMT solver uses the subset of SMT summaries stored in this node to search for a satisfying assignment. The direction of the traversal is determined by the results of the concretisation of an abstract counterexample obtained at the current node. Our experimental results demonstrate that this approach allows to solve a number of instances that were previously unsolvable by the existing bounded model-checkers.

ABSTRACT. We introduce a new framework for verifying electronic vote counting results that are based on the Single Transferable Vote scheme (STV). Our approach frames electronic vote counting as certified computation where each execution of the counting algorithm is accompanied by a certificate that witnesses the correctness of the output. These certificates are then checked for correctness independently of how they are produced. We advocate to verify the verifier rather than the soft- ware used to produce the result. We use the theorem prover HOL to formalise the STV vote counting scheme, and obtain a fully verified certificate checker. By connecting HOL with the verified CakeML compiler, we then extract an executable that is guaranteed to behave correctly with respect to the formal specification of the protocol down to machine level. We demonstrate that our verifier can check certificates of real-size elections efficiently. Our encoding is modular, so repeating the same pro- cess for another different STV scheme would require a minimal amount of additional work.

ABSTRACT. Software verification tools that build machine-checked proofs of functional correctness usually focus on the algorithmic content of the code. Their proofs are not grounded in a formal semantic model of the environment that the program runs in, or the program’s interaction with that environment. As a result, several layers of translation and wrapper code must be trusted. In contrast, the CakeML project focuses on end-to-end verification to replace this trusted code with verified code in a cost-effective manner. In this paper, we present infrastructure for developing and verifying impure functional programs with I/O and imperative file handling. Specifically, we extend CakeML with a low-level model of file I/O, and verify a high-level file I/O library in terms of the model. We use this library to develop and verify several Unix-style command-line utilities: cat, sort, grep, diff and patch. The workflow we present is built around the HOL4 theorem prover, and therefore all our results have machine-checked proofs.

ABSTRACT. Type-preserving (or typed) compilation uses typing derivations to certify correctness properties of compilation. We have designed and implemented a type-preserving compiler for a simply-typed dialect of Prolog we call T-Prolog. The crux of our approach is a new certifying abstract machine which we call the Typed Warren Abstract Machine (TWAM). The TWAM has a dependent type system strong enough to specify the semantics of a logic program in the logical framework LF. We present a soundness metatheorem which constitutes a partial correctness guarantee: well-typed programs implement the logic program specified by their type. This metatheorem justifies our design and implementation of a certifying compiler from T-Prolog to TWAM.

ABSTRACT. This paper presents the first Coq formalisation of the full Java byte-code instruction set and its semantics. The set of instructions is organised in a hierarchy depending on how the instructions deal with the runtime structures of the Java Virtual Machine such as threads, stacks, heap etc. The hierarchical nature of Coq modules neatly reinforces this view and facilitates the understanding of the Java bytecode semantics. This approach makes it possible to both conduct verification of properties for programs and to prove metatheoretical results for the language. Based upon our formalisation experience, the deficiencies of the current informal bytecode language specification are discussed.

ABSTRACT. Formal models of low-level applications rely often on the distinction between executable layer and underlying hardware abstraction. On one hand, the formal development of the executable specification can benefit from a language designed to support theorem proving in connection with the specific domain of the application. A deep embedding makes it possible to manipulate such a language in a direct way, e.g. in formally translating the executable specification to an efficient program. On the other hand, the abstract character of the hardware specification makes it desirable to take full advantage of the expressive power of the theorem prover, relying on a shallow embedding. Implementing deeply embedded languages that allow importing shallow specifications can be an answer to the problem of combining the two approaches. We use Coq to formalise such a deep embedding, which we use to support the formal development of an OS kernel. We take advantage of the Coq logic in specifying the deep embedding relationally, using structural operational semantics, then extracting an executable interpreter from the type soundness proof.