Skip to main content
main-content
Top

About this book

This book constitutes the refereed proceedings of the 20th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2019, held in Cascais, Portugal, in January 2019.The 27 full papers presented together with the abstracts of 3 invited keynote talks were carefully reviewed and selected from 62 submissions. VMCAI provides topics including: program verification, model checking, abstract interpretation, program synthesis, static analysis, type systems, deductive methods, program certification, decision procedures, theorem proving, program certification, debugging techniques, program transformation, optimization, and hybrid and cyber-physical systems.

Table of Contents

Frontmatter

On the Semantics of Snapshot Isolation

Snapshot isolation (SI) is a standard transactional consistency model used in databases, distributed systems and software transactional memory (STM). Its semantics is formally defined both declaratively as an acyclicity axiom, and operationally as a concurrent algorithm with memory bearing timestamps.
We develop two simpler equivalent operational definitions of SI as lock-based reference implementations that do not use timestamps. Our first locking implementation is prescient in that requires a priori knowledge of the data accessed by a transaction and carries out transactional writes eagerly (in-place). Our second implementation is non-prescient and performs transactional writes lazily by recording them in a local log and propagating them to memory at commit time. Whilst our first implementation is simpler and may be better suited for developing a program logic for SI transactions, our second implementation is more practical due to its non-prescience. We show that both implementations are sound and complete against the declarative SI specification and thus yield equivalent operational definitions for SI.
We further consider, for the first time formally, the use of SI in a context with racy non-transactional accesses, as can arise in STM implementations of SI. We introduce robust snapshot isolation (RSI), an adaptation of SI with similar semantics and guarantees in this mixed setting. We present a declarative specification of RSI as an acyclicity axiom and analogously develop two operational models as lock-based reference implementations (one eager, one lazy). We show that these operational models are both sound and complete against the declarative RSI model.
Azalea Raad, Ori Lahav, Viktor Vafeiadis

Program Synthesis with Equivalence Reduction

We introduce program synthesis with equivalence reduction, a synthesis methodology that utilizes relational specifications over components of a given synthesis domain to reduce the search space. Leveraging a blend of classic and modern techniques from term rewriting, we use relational specifications to discover a canonical representative per equivalence class of programs. We show how to design synthesis procedures that only consider programs in normal form, thus pruning the search space. We discuss how to implement equivalence reduction using efficient data structures, and demonstrate the significant reductions it can achieve in synthesis time.
Calvin Smith, Aws Albarghouthi

Minimal Synthesis of String to String Functions from Examples

We study the problem of synthesizing string to string transformations from a set of input/output examples. The transformations we consider are expressed using a particular class of transducers: functional non-deterministic Mealy machines (f-NDMM). These are machines that read input letters one at a time, and output one letter at each step. The functionality constraint ensures that, even though the machine is locally non-deterministic, each input string is mapped to exactly one output string by the transducer.
We suggest that, given a set of input/output examples, the smallest f-NDMM consistent with the examples is a good candidate for the transformation the user was expecting. We therefore study the problem of, given a set of examples, finding a minimal f-NDMM consistent with the examples and satisfying the functionality and totality constraints mentioned above.
We prove that, in general, the decision problem corresponding to that question is \(\textsf {NP}\)-complete, and we provide several \(\textsf {NP}\)-hardness proofs that show the hardness of multiple variants of the problem.
Finally, we propose an algorithm for finding the minimal f-NDMM consistent with input/output examples, that uses a reduction to SMT solvers. We implemented the algorithm, and used it to evaluate the likelihood that the minimal f-NDMM indeed corresponds to the transformation expected by the user.
Jad Hamza, Viktor Kunčak

Automatic Program Repair Using Formal Verification and Expression Templates

We present an automated approach to repair programs using formal verification and expression templates. In our approach, an input program is first verified against its formal specification to discover potentially buggy statements. For each of these statements, we identify the expression that needs to be repaired and set up a template patch which is a linear expression composed of the program’s variables and unknown coefficients. Then, we analyze the template-patched program against the original specification to collect a set of constraints of the template patch. This constraint set will be solved by a constraint solving technique using Farkas’ lemma to identify the unknown coefficients, consequently discovering the actual patch. We implement our approach in a tool called Maple and evaluate it with various buggy programs from a widely used benchmark TCAS, and a synthetic yet challenging benchmark containing recursive programs. Our tool can quickly discover the correct patches and outperforms the state-of-the-art program repair tools.
Thanh-Toan Nguyen, Quang-Trung Ta, Wei-Ngan Chin

Lazy but Effective Functional Synthesis

We present a new technique for generating a function implementation from a declarative specification formulated as a \(\forall \exists \)-formula in first-order logic. We follow a classic approach of eliminating existential quantifiers and extracting Skolem functions for the theory of linear arithmetic. Our method eliminates quantifiers lazily and produces a synthesis solution in the form of a decision tree. Compared to prior approaches, our decision trees have fewer nodes due to deriving theory terms that can be shared both within a single output as well as across multiple outputs. Our approach is implemented in a tool called AE-VAL, and its evaluation on a set of reactive synthesis benchmarks shows promise.
Grigory Fedyukovich, Arie Gurfinkel, Aarti Gupta

Static Analysis of Binary Code with Memory Indirections Using Polyhedra

In this paper we propose a new abstract domain for static analysis of binary code. Our motivation stems from the need to improve the precision of the estimation of the Worst-Case Execution Time (WCET) of safety-critical real-time code. WCET estimation requires computing information such as upper bounds on the number of loop iterations, unfeasible execution paths, etc. These estimations are usually performed on binary code, mainly to avoid making assumptions on how the compiler works. Our abstract domain, based to polyhedra and on two mapping functions that associate polyhedra variables with registers and memory, targets the precise computation of such information. We prove the correctness of the method, and demonstrate its effectiveness on benchmarks and examples from typical embedded code.
Clément Ballabriga, Julien Forget, Laure Gonnord, Giuseppe Lipari, Jordy Ruiz

Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis

Program analysis by abstract interpretation using relational abstract domains—like polyhedra or octagons—easily extends from state analysis (construction of reachable states) to relational analysis (construction of input-output relations). In this paper, we exploit this extension to enable interprocedural program analysis, by constructing relational summaries of procedures. In order to improve the accuracy of procedure summaries, we propose a method to refine them into disjunctions of relations, these disjunctions being directed by preconditions on input parameters.
Rémy Boutonnet, Nicolas Halbwachs

Exploiting Pointer Analysis in Memory Models for Deductive Verification

Cooperation between verification methods is crucial to tackle the challenging problem of software verification. The paper focuses on the verification of C programs using pointers and it formalizes a cooperation between static analyzers doing pointer analysis and a deductive verification tool based on first order logic. We propose a framework based on memory models that captures the partitioning of memory inferred by pointer analyses, and complies with the memory models used to generate verification conditions. The framework guided us to propose a pointer analysis that accommodates to various low-level operations on pointers while providing precise information about memory partitioning to the deductive verification. We implemented this cooperation inside the Frama-C platform and we show its effectiveness in reducing the task of deductive verification on a complex case study.
Quentin Bouillaguet, François Bobot, Mihaela Sighireanu, Boris Yakobowski

Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs

The increasing prevalence of soft errors and security concerns due to recent attacks like rowhammer have caused increased interest in the robustness of software against bit flips.
Arithmetic codes can be used as a protection mechanism to detect small errors injected in the program’s data. However, the accumulation of propagated errors can increase the number of bits flips in a variable - possibly up to an undetectable level.
The effect of error masking can occur: An error weight exceeds the limitations of the code and a new, valid, but incorrect code word is formed. Masked errors are undetectable, and it is crucial to check variables for bit flips before error masking can occur.
In this paper, we develop a theory of provably robust arithmetic programs. We focus on the interaction of bit flips that can happen at different locations in the program and the propagation and possible masking of errors. We show how this interaction can be formally modeled and how off-the-shelf model checkers can be used to show correctness. We evaluate our approach based on prominent and security relevant algorithms and show that even multiple faults injected at any time into any variables can be handled by our method.
Anja F. Karl, Robert Schilling, Roderick Bloem, Stefan Mangard

Relatively Complete Pushdown Analysis of Escape Continuations

Escape continuations are weaker than full, first-class continuations but nevertheless can express many common control operators. Although language and compiler designs profitably leverage escape continuations, all previous approaches to analyze them statically in a higher-order setting have been ad hoc or imprecise. We present \(\mathrm {MCCFA}2\), a generalization of \(\mathrm {CFA}2\) that analyzes them with pushdown precision in their most-general form. In particular, the summarization algorithm of \(\mathrm {MCCFA}2\) is both sound and complete with respect to a conservative extension of \(\mathrm {CFA}2\)’s abstract semantics. We also present an continuation age analysis as a client of \(\mathrm {MCCFA}2\) that reveals critical function call optimizations.
Kimball Germane, Matthew Might

Demand Control-Flow Analysis

Points-to analysis manifests in a functional setting as control-flow analysis. Despite the ubiquity of demand points-to analyses, there are no analogous demand control-flow analyses for functional languages in general. We present demand 0CFA, a demand control-flow analysis that offers clients in a functional setting the same pricing model that demand points-to analysis clients enjoy in an imperative setting. We establish demand 0CFA’s correctness via an intermediary exact semantics, demand evaluation, that can potentially support demand variants of more-precise analyses.
Kimball Germane, Jay McCarthy, Michael D. Adams, Matthew Might

Effect-Driven Flow Analysis

Traditional machine-based static analyses use a worklist algorithm to explore the analysis state space, and compare each state in the worklist against a set of seen states as part of their fixed-point computation. This may require many state comparisons, which gives rise to a computational overhead. Even an analysis with a global store has to clear its set of seen states each time the store updates because of allocation or side-effects, which results in more states being reanalyzed and compared.
In this work we present a static analysis technique, Modf, that does not rely on a set of seen states, and apply it to a machine-based analysis with global-store widening. Modf analyzes one function execution at a time to completion while tracking read, write, and call effects. These effects trigger the analysis of other function executions, and the analysis terminates when no new effects can be discovered.
We compared Modf to a traditional machine-based analysis implementation on a set of 20 benchmark programs and found that Modf is faster for 17 programs with speedups ranging between 1.4x and 12.3x. Furthermore, Modf exhibits similar precision as the traditional analysis on most programs and yields state graphs that are comparable in size.
Jens Nicolay, Quentin Stiévenart, Wolfgang De Meuter, Coen De Roover

Type-Directed Bounding of Collections in Reactive Programs

Our aim is to statically verify that in a given reactive program, the length of collection variables does not grow beyond a given bound. We propose a scalable type-based technique that checks that each collection variable has a given refinement type that specifies constraints about its length. A novel feature of our refinement types is that the refinements can refer to AST counters that track how many times an AST node has been executed. This feature enables type refinements to track limited flow-sensitive information. We generate verification conditions that ensure that the AST counters are used consistently, and that the types imply the given bound. The verification conditions are discharged by an off-the-shelf SMT solver. Experimental results demonstrate that our technique is scalable, and effective at verifying reactive programs with respect to requirements on length of collections.
Tianhan Lu, Pavol Černý, Bor-Yuh Evan Chang, Ashutosh Trivedi

Solving and Interpolating Constant Arrays Based on Weak Equivalences

We present a new solver and interpolation algorithm for the theory of arrays with constant arrays. It is based on our previous work on weakly equivalent arrays. Constant arrays store the same value at every index, which is useful for model checking of programs with initialised memory. Instead of using a store chain to explicitly initialise the memory, using a constant array can considerably simplify the queries and thus reduce the solving and interpolation time. We show that only a few new rules are required for constant arrays and prove the correctness of the decision procedure and the interpolation procedure. We implemented the algorithm in our interpolating solver SMTInterpol.
Jochen Hoenicke, Tanja Schindler

A Decidable Logic for Tree Data-Structures with Measurements

We present \({\textsc {Dryad}}_\textit{dec}\), a decidable logic that allows reasoning about tree data-structures with measurements. This logic supports user-defined recursive measure functions based on Max or Sum, and recursive predicates based on these measure functions, such as AVL trees or red-black trees. We prove that the logic’s satisfiability is decidable. The crux of the decidability proof is a small model property which allows us to reduce the satisfiability of \({\textsc {Dryad}}_\textit{dec}\) to quantifier-free linear arithmetic theory which can be solved efficiently using SMT solvers. We also show that \({\textsc {Dryad}}_\textit{dec}\) can encode a variety of verification and synthesis problems, including natural proof verification conditions for functional correctness of recursive tree-manipulating programs, legality conditions for fusing tree traversals, synthesis conditions for conditional linear-integer arithmetic functions. We developed the decision procedure and successfully solved 220+ \({\textsc {Dryad}}_\textit{dec}\) formulae raised from these application scenarios, including verifying functional correctness of programs manipulating AVL trees, red-black trees and treaps, checking the fusibility of height-based mutually recursive tree traversals, and counterexample-guided synthesis from linear integer arithmetic specifications. To our knowledge, \({\textsc {Dryad}}_\textit{dec}\) is the first decidable logic that can solve such a wide variety of problems requiring flexible combination of measure-related, data-related and shape-related properties for trees.
Xiaokang Qiu, Yanjun Wang

A Practical Algorithm for Structure Embedding

This paper presents an algorithm for the structure embedding problem: given two finite first-order structures over a common relational vocabulary, does there exist an injective homomorphism from one to the other? The structure embedding problem is NP-complete in the general case, but for monadic structures (each predicate has arity \(\le 1\)) we observe that it can be solved in polytime by reduction to bipartite graph matching. Our algorithm, MatchEmbeds, extends the bipartite matching approach to the general case by using it as the foundation of a backtracking search procedure. We show that MatchEmbeds outperforms state-of-the-art SAT, CSP, and subgraph isomorphism solvers on difficult random instances and significantly improves the performance of a client model checker for multi-threaded programs.
Charlie Murphy, Zachary Kincaid

euforia: Complete Software Model Checking with Uninterpreted Functions

We introduce and evaluate an algorithm for an https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-11245-5_17/479230_1_En_17_IEq1_HTML.gif -style software model checker that operates entirely at the level of equality with uninterpreted functions (EUF). Our checker, called https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-11245-5_17/479230_1_En_17_IEq2_HTML.gif , targets control properties by treating a program’s data operations/relations as uninterpreted functions/predicates. This results in an EUF abstract transition system that https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-11245-5_17/479230_1_En_17_IEq3_HTML.gif analyzes to either (1) discover an inductive strengthening EUF formula that proves the property or (2) produce an abstract counterexample that corresponds to zero, one, or many concrete counterexamples. Infeasible counterexamples are eliminated by an efficient refinement method that constrains the EUF abstraction until the property is proved or a feasible counterexample is produced. We formalize the EUF transition system, prove our algorithm correct, and demonstrate our results on a subset of benchmarks from the software verification competition (SV-COMP) 2017.
Denis Bueno, Karem A. Sakallah

Fast BGP Simulation of Large Datacenters

Frequent configuration churn caused by maintenance, upgrades, hardware and firmware failures regularly leads to costly outages. Preventing network outages caused by misconfigurations is important for ensuring high network availability. Dealing with production datacenters with thousands of routers is a major challenge.
Network verification inspects the forwarding tables of routers. These tables are determined by the so-called control plane, which is given by the steady state of the routing protocols. The ability to simulate routing protocols given router configuration files and thus obtain the control plane is a key enabling technology.
In this paper, we present FastPlane, an efficient BGP simulator. BGP support is mandated by modern datacenter designs, which choose BGP as the routing protocol. The key to FastPlane’s performance is our insight into the routing policy of cloud datacenters that allows the usage of a generalized Dijkstra’s algorithm. The insight reveals that these networks are monotonic, i.e., route advertisements decrease preference when propagated through the network.
The evaluation on real world, production datacenters of a major cloud provider shows that FastPlane (1) is two orders of magnitude faster than the state-of-the-art on small and medium datacenters, and (2) goes beyond the state-of-the-art by scaling to large datacenters. FastPlane was instrumental in finding several production bugs in router firmware, routing policy, and network architecture.
Nuno P. Lopes, Andrey Rybalchenko

Verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model Checking

The election of a leader in a network is a challenging task, especially when the processes are asynchronous, i. e., execute an algorithm with time-varying periods. Thales developed an industrial election algorithm with an arbitrary number of processes, that can possibly fail. In this work, we prove the correctness of a variant of this industrial algorithm. We use a method combining abstraction, the SafeProver solver, and a parametric timed model-checker. This allows us to prove the correctness of the algorithm for a large number p of processes (\(p=5000\)).
Étienne André, Laurent Fribourg, Jean-Marc Mota, Romain Soulat

Application of Abstract Interpretation to the Automotive Electronic Control System

The verification and validation of industrial automotive systems is increasingly challenging as they become larger and more complex. Recent automotive Electric Control Units (ECUs) have approximately one half to one million of lines of code, and a modern automobile can contain hundreds of controllers. Significant work-hours are needed to understand and manage systems of this level of complexity. One particular challenge is understanding the changes to the software across development phases and revisions. To this end, we present a code dependency analysis tool that enhances designer understanding. It combines abstract interpretation and graph based data analysis to generate visualized dependency graphs on demand to support designer’s understanding of the code. We demonstrate its value by presenting dependency graph visuals for an industrial application, and report results showing significant reduction of work-hours and enhancement of the ability to understand the software.
Tomoya Yamaguchi, Martin Brain, Chirs Ryder, Yosikazu Imai, Yoshiumi Kawamura

Syntactic Partial Order Compression for Probabilistic Reachability

The state space explosion problem is among the largest impediments to the performance of any model checker. Modelling languages for compositional systems contribute to this problem by placing each instruction of an instruction sequence onto a dedicated transition, giving concurrent processes opportunities to interleave after every instruction. Users wishing to avoid the excessive number of interleavings caused by this default can choose to explicitly declare instruction sequences as atomic, which however requires careful considerations regarding the impact this might have on the model as well as on the properties that are to be checked. We instead propose a preprocessing technique that automatically identifies instruction sequences that can safely be considered atomic. This is done in the context of concurrent variable-decorated Markov Decision Processes. Our approach is compatible with any off-the-shelf probabilistic model checker. We prove that our transformation preserves maximal reachability probabilities and present case studies to illustrate its usefulness.
Gereon Fox, Daniel Stan, Holger Hermanns

Termination of Nondeterministic Probabilistic Programs

We study the termination problem for nondeterministic probabilistic programs. We consider the bounded termination problem that asks whether the supremum of the expected termination time over all schedulers is bounded. First, we show that ranking supermartingales (RSMs) are both sound and complete for proving bounded termination over nondeterministic probabilistic programs. For nondeterministic probabilistic programs a previous result claimed that RSMs are not complete for bounded termination, whereas our result corrects the previous flaw and establishes completeness with a rigorous proof. Second, we present the first sound approach to establish lower bounds on expected termination time through RSMs.
Hongfei Fu, Krishnendu Chatterjee

Parametric Timed Broadcast Protocols

In this paper we consider state reachability in networks composed of many identical processes running a parametric timed broadcast protocol (PTBP). PTBP are a new model extending both broadcast protocols and parametric timed automata. This work is, up to our knowledge, the first to consider the combination of both a parametric network size and timing parameters in clock guard constraints. Since the communication topology is of utmost importance in broadcast protocols, we investigate reachability problems in both clique semantics where every message reaches every processes, and in reconfigurable semantics where the set of receivers is chosen non-deterministically. In addition, we investigate the decidability status depending on whether the timing parameters in guards appear only as upper bounds in guards, as lower bounds or when the set of parameters is partitioned in lower-bound and upper-bound parameters.
Étienne André, Benoit Delahaye, Paulin Fournier, Didier Lime

Flat Model Checking for Counting LTL Using Quantifier-Free Presburger Arithmetic

This paper presents an approximation approach to verifying counter systems with respect to properties formulated in an expressive counting extension of linear temporal logic. It can express, e.g., that the number of acknowledgements never exceeds the number of requests to a service, by counting specific positions along a run and imposing arithmetic constraints. The addressed problem is undecidable and therefore solved on flat under-approximations of a system. This provides a flexibly adjustable trade-off between exhaustiveness and computational effort, similar to bounded model checking. Recent techniques and results for model-checking frequency properties over flat Kripke structures are lifted and employed to construct a parametrised encoding of the (approximated) problem in quantifier-free Presburger arithmetic. A prototype implementation based on the z3 SMT solver demonstrates the effectiveness of the approach based on problems from the RERS Challange.
Normann Decker, Anton Pirogov

A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization

Symbolic computation using BDDs and bisimulation minimization are alternative ways to cope with the state space explosion in model checking. The combination of both techniques opens up many parameters that can be tweaked for further optimization. Most importantly, the bisimulation can either be represented as equivalence classes or as a relation. While recent work argues that storing partitions is more efficient, we show that the relation-based approach is preferable. We do so by deriving a relation-based minimization algorithm based on new coarse-grained BDD operations. The implementation demonstrates that the relational approach uses fewer memory and performs better.
Richard Huybers, Alfons Laarman

Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics

Parametric models abstract part of the specification of dynamical models by integral parameters. They are for example used in computational systems biology, notably with parametric regulatory networks, which specify the global architecture (interactions) of the networks, while parameterising the precise rules for drawing the possible temporal evolutions of the states of the components. A key challenge is then to identify the discrete parameters corresponding to concrete models with desired dynamical properties. This paper addresses the restriction of the abstract execution of parametric regulatory (discrete) networks by the means of static analysis of reachability properties (goal states). Initially defined at the level of concrete parameterised models, the goal-oriented reduction of dynamics is lifted to parametric networks, and is proven to preserve all the minimal traces to the specified goal states. It results that one can jointly perform the refinement of parametric networks (restriction of domain of parameters) while reducing the necessary transitions to explore and preserving reachability properties of interest.
Stefan Haar, Juraj Kolčák, Loïc Paulevé

Mechanically Proving Determinacy of Hierarchical Block Diagram Translations

Hierarchical block diagrams (HBDs) are at the heart of embedded system design tools, including Simulink. Numerous translations exist from HBDs into languages with formal semantics, amenable to formal verification. However, none of these translations has been proven correct, to our knowledge.
We present in this paper the first mechanically proven HBD translation algorithm. The algorithm translates HBDs into an algebra of terms with three basic composition operations (serial, parallel, and feedback). In order to capture various translation strategies resulting in different terms achieving different tradeoffs, the algorithm is nondeterministic. Despite this, we prove its semantic determinacy: for every input HBD, all possible terms that can be generated by the algorithm are semantically equivalent. We apply this result to show how three Simulink translation strategies introduced previously can be formalized as determinizations of the algorithm, and derive that these strategies yield semantically equivalent results (a question left open in previous work). All results are formalized and proved in the Isabelle theorem-prover and the code is publicly available.
Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis

Backmatter

Additional information

Premium Partner

image credits