title: Lazy Abstractions for Timed Automata

authors:
Frédéric Herbreteau
B. Srivathsan
Igor Walukiewicz

abstract: We consider the reachability problem for timed automata. A standard solution to this problem involves computing a search tree whose nodes are abstractions of zones. For efficiency reasons, they are parametrized by the maximal lower and upper bounds (LU-bounds) occurring in the guards of the automaton. We propose an algorithm that dynamically updates LU-bounds during exploration of the search tree. In order to keep them as small as possible, the bounds are refined only when they enable a transition that is impossible in the unabstracted system. So our algorithm can be seen as a kind of lazy CEGAR algorithm for timed automata. We show that on several standard benchmarks, the algorithm is capable of keeping very small LU-bounds, and in consequence is able to reduce the search space substantially.


venue: cav

title: Fully Automated Shape Analysis Based on Forest Automata

authors:
Lukás Holík
Ondrej Lengál
Adam Rogalewicz
Jirí Simácek
Tomás Vojnar

abstract: Forest automata (FA) have recently been proposed as a tool for shape analysis of complex heap structures. FA encode sets of tree decompositions of heap graphs in the form of tuples of tree automata. In order to allow for representing complex heap graphs, the notion of FA allowed one to provide user-defined FA (called boxes) that encode repetitive graph patterns of shape graphs to be used as alphabet symbols of other, higher-level FA. In this paper, we propose a novel technique of automatically learning the FA to be used as boxes that avoids the need of providing them manually. Further, we propose a significant improvement of the automata abstraction used in the analysis. The result is an efficient, fully-automated analysis that can handle even as complex data structures as skip lists, with the performance comparable to state-of-the-art fully-automated tools based on separation logic, which, however, specialise in dealing with linked lists only.


title: Effectively-Propositional Reasoning about Reachability in Linked Data Structures

authors:
Shachar Itzhaky
Anindya Banerjee
Neil Immerman
Aleksandar Nanevski
Mooly Sagiv


title: Importance Splitting for Statistical Model Checking Rare Properties

authors:
Cyrille Jégourel
Axel Legay
Sean Sedwards


title: PARTY Parameterized Synthesis of Token Rings

authors:
Ayrat Khalimov
Swen Jacobs
Roderick Bloem


title: Incremental, Inductive Coverability

authors:
Johannes Kloos
Rupak Majumdar
Filip Niksic
Ruzica Piskac

abstract:
We give an incremental, inductive (IC3) procedure to check coverability of well-structured transition systems. Our procedure generalizes the IC3 procedure for safety verification that has been successfully applied in finite-state hardware verification to infinite-state well-structured transition systems. We show that our procedure is sound, complete, and terminating for downward-finite well-structured transition systems --where each state has a finite number of states below it-- a class that contains extensions of Petri nets, broadcast protocols, and lossy channel systems.

We have implemented our algorithm for checking coverability of Petri nets. We describe how the algorithm can be efficiently implemented without the use of SMT solvers. Our experiments on standard Petri net benchmarks show that IC3 is competitive with state-of-the-art implementations for coverability based on symbolic backward analysis or expand-enlarge-and-check algorithms both in time and space usage.


title: Automatic Abstraction in SMT-Based Unbounded Software Model Checking

authors:
Anvesh Komuravelli
Arie Gurfinkel
Sagar Chaki
Edmund M. Clarke

abstract: Software model checkers based on under-approximations and SMT solvers are very successful at verifying safety (i.e., reachability) properties. They combine two key ideas --- (a) concreteness: a counterexample in an under-approximation is a counterexample in the original program as well, and (b) generalization: a proof of safety of an under-approximation, produced by an SMT solver, are generalizable to proofs of safety of the original program. In this paper, we present a combination of automatic abstraction with the under-approximation-driven framework. We explore two iterative approaches for obtaining and refining abstractions --- proof based and counterexample based --- and show how they can be combined into a unified algorithm. To the best of our knowledge, this is the first application of Proof-Based Abstraction, primarily used to verify hardware, to Software Verification. We have implemented a prototype of the framework using Z3, and evaluate it on many benchmarks from the Software Verification Competition. We show experimentally that our combination is quite effective on hard instances.


title: Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems

authors:
Hui Kong
Fei He
Xiaoyu Song
William N. N. Hung
Ming Gu

abstract: A barrier certificate is an inductive invariant function which can be used for the safety verification of a hybrid system. Safety verification based on barrier certificate has the benefit of avoiding explicit computation of the exact reachable set which is usually intractable for nonlinear hybrid systems. In this paper, we propose a new barrier certificate condition, called Exponential Condition, for the safety verification of semi-algebraic hybrid systems. The most important benefit of Exponential Condition is that it has a lower conservativeness than the existing convex conditions and meanwhile it possesses the convexity. On the one hand, a less conservative barrier certificate forms a tighter over-approximation for the reachable set and hence is able to verify critical safety properties. On the other hand, the convexity guarantees its solvability by semidefinite programming method. Some examples are presented to illustrate the effectiveness and practicality of our method.


title: First-Order Theorem Proving and Vampire

authors:
Laura Kovács
Andrei Voronkov


title: Under-Approximating Loops in C Programs for Fast Counterexample Detection

authors:
Daniel Kroening
Matt Lewis
Georg Weissenbacher


title: Multi-core Emptiness Checking of Timed Büchi Automata Using Inclusion Abstraction

authors:
Alfons Laarman
Mads Chr. Olesen
Andreas Engelbredt Dalsgaard
Kim Guldstrand Larsen
Jaco van de Pol


title: CacBDD: A BDD Package with Dynamic Cache Management

authors:
Guanfeng Lv
Kaile Su
Yanyan Xu


title: System Level Formal Verification via Model Checking Driven Simulation

authors:
Toni Mancini
Federico Mari
Annalisa Massini
Igor Melatti
Fabio Merli
Enrico Tronci


title: ILP Modulo Theories

authors:
Panagiotis Manolios
Vasilis Papavasileiou

abstract: We present Integer Linear Programming (ILP) Modulo Theories (IMT). An IMT instance is an Integer Linear Programming instance, where some symbols have interpretations in background theories. In previous work, the IMT approach has been applied to industrial synthesis and design problems with real-time constraints arising in the development of the Boeing 787. Many other problems ranging from operations research to software verification routinely involve linear constraints and optimization. Thus, a general ILP Modulo Theories framework has the potential to be widely applicable. The logical next step in the development of IMT and the main goal of this paper is to provide theoretical underpinnings. This is accomplished by means of BC(T), the Branch and Cut Modulo T abstract transition system. We show that BC(T) provides a sound and complete optimization procedure for the ILP Modulo T problem, as long as T is a decidable, stably-infinite theory. We compare a prototype of BC(T) against leading SMT solvers.


title: Minimal Sets over Monotone Predicates in Boolean Formulae

authors:
João Marques-Silva
Mikolás Janota
Anton Belov


title: The TAMARIN Prover for the Symbolic Analysis of Security Protocols

authors:
Simon Meier
Benedikt Schmidt
Cas Cremers
David A. Basin


title: Multi-solver Support in Symbolic Execution

authors:
Hristina Palikareva
Cristian Cadar


title: Under-Approximating Cut Sets for Reachability in Large Scale Automata Networks

authors:
Loïc Paulevé
Geoffroy Andrieux
Heinz Koeppl

abstract:
In the scope of discrete finite-state models of interacting components, we present a novel algorithm for identifying sets of local states of components whose activity is necessary for the reachability of a given local state. If all the local states from such a set are disabled in the model, the concerned reachability is impossible.

Those sets are referred to as cut sets and are computed from a particular abstract causality structure, so-called Graph of Local Causality, inspired from previous work and generalised here to finite automata networks. The extracted sets of local states form an under-approximation of the complete minimal cut sets of the dynamics: there may exist smaller or additional cut sets for the given reachability.

Applied to qualitative models of biological systems, such cut sets provide potential therapeutic targets that are proven to prevent molecules of interest to become active, up to the correctness of the model. Our new method makes tractable the formal analysis of very large scale networks, as illustrated by the computation of cut sets within a Boolean model of biological pathways interactions gathering more than 9000 components.


title: Automating Separation Logic Using SMT

authors:
Ruzica Piskac
Thomas Wies
Damien Zufferey


title: Abstraction Based Model-Checking of Stability of Hybrid Systems

authors:
Pavithra Prabhakar
Miriam Garcia Soto


title: Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties

authors:
Alberto Puggelli
Wenchao Li
Alberto L. Sangiovanni-Vincentelli
Sanjit A. Seshia


title: TTP: Tool for Tumor Progression

authors:
Johannes G. Reiter
Ivana Bozic
Krishnendu Chatterjee
Martin A. Nowak

abstract: In this work we present a flexible tool for tumor progression, which simulates the evolutionary dynamics of cancer. Tumor progression implements a multi-type branching process where the key parameters are the fitness landscape, the mutation rate, and the average time of cell division. The fitness of a cancer cell depends on the mutations it has accumulated. The input to our tool could be any fitness landscape, mutation rate, and cell division time, and the tool produces the growth dynamics and all relevant statistics.


title: Finite Model Finding in SMT

authors:
Andrew Reynolds
Cesare Tinelli
Amit Goel
Sava Krstic


title: Disjunctive Interpolants for Horn-Clause Verification

authors:
Philipp Rümmer
Hossein Hojjat
Viktor Kuncak

abstract: One of the main challenges in software verification is efficient and precise compositional analysis of programs with procedures and loops. Interpolation methods remains one of the most promising techniques for such verification, and are closely related to solving Horn clause constraints. We introduce a new notion of interpolation, disjunctive interpolation, which solves a more general class of problems in one step compared to previous notions of interpolants, such as tree interpolants or inductive sequences of interpolants. We present algorithms and complexity for construction of disjunctive interpolants, as well as their use within an abstraction-refinement loop. We have implemented Horn clause verification algorithms that use disjunctive interpolants and evaluate them on benchmarks expressed as Horn clauses over the theory of integer linear arithmetic.


title: Shrinktech: A Tool for the Robustness Analysis of Timed Automata


title: Finding Security Vulnerabilities in a Network Protocol Using Parameterized Systems

authors:
Adi Sosnovich
Orna Grumberg
Gabi Nakibly


title: Upper Bounds for Newton's Method on Monotone Polynomial Systems, and P-Time Model Checking of Probabilistic One-Counter Automata

authors:
Alistair Stewart
Kousha Etessami
Mihalis Yannakakis


title: GOAL for Games, Omega-Automata, and Logics

authors:
Ming-Hsien Tsai
Yih-Kuen Tsay
Yu-Shiang Hwang


title: Smten: Automatic Translation of High-Level Symbolic Computations into SMT Queries

authors:
Richard Uhler
Nirav Dave


title: Efficient Generation of Small Interpolants in CNF

authors:
Yakir Vizel
Vadim Ryvchin
Alexander Nadel


title: Programs from Proofs - A PCC Alternative

authors:
Daniel Wonisch
Alexander Schremmer
Heike Wehrheim


title: From Invariant Checking to Invariant Inference Using Randomized Search

authors:
Rahul Sharma
Alex Aiken


title: ICE: A Robust Framework for Learning Invariants

authors:
Pranav Garg
Christof Löding
P. Madhusudan
Daniel Neider


title: String Constraints for Verification

authors:
Parosh Aziz Abdulla
Mohamed Faouzi Atig
Yu-Fang Chen
Lukás Holík
Ahmed Rezine
Philipp Rümmer
Jari Stenman


title: Don't Sit on the Fence - A Static Analysis Approach to Automatic Fence Insertion

authors:
Jade Alglave
Daniel Kroening
Vincent Nimal
Daniel Poetzl


title: Engineering a Static Verification Tool for GPU Kernels

authors:
Ethel Bardsley
Adam Betts
Nathan Chong
Peter Collingbourne
Pantazis Deligiannis
Alastair F. Donaldson
Jeroen Ketema
Daniel Liew
Shaz Qadeer


title: Software Verification in the Google App-Engine Cloud

authors:
Dirk Beyer
Georg Dresler
Philipp Wendler


title: Verifying Relative Error Bounds Using Symbolic Simulation

authors:
Jesse Bingham
Joe Leslie-Hurd


title: Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR)

authors:
Johannes Birgmeier
Aaron R. Bradley
Georg Weissenbacher


title: Safraless Synthesis for Epistemic Temporal Specifications

authors:
Rodica Bozianu
Catalin Dima
Emmanuel Filiot

abstract:
In this paper we address the synthesis problem for specifications given in linear temporal single-agent epistemic logic, KLTL (or KL 1), over single-agent systems having imperfect information of the environment state. [17] have shown that this problem is 2Exptime complete. However, their procedure relies on complex automata constructions that are notoriously resistant to efficient implementations as they use Safra-like determinization.

We propose a "Safraless" synthesis procedure for a large fragment of KLTL. The construction transforms first the synthesis problem into the problem of checking emptiness for universal co-Buchi tree automata using an information-set construction. Then we build a safety game that can be solved using an antichain-based symbolic technique exploiting the structure of the underlying automata. The technique is implemented and applied to a couple of case studies.


title: Minimizing Running Costs in Consumption Systems

authors:
Tomás Brázdil
David Klaska
Antonín Kucera
Petr Novotný

abstract: A standard approach to optimizing long-run running costs of discrete systems is based on minimizing the mean-payoff, i.e., the long-run average amount of resources ("energy") consumed per transition. However, this approach inherently assumes that the energy source has an unbounded capacity, which is not always realistic. For example, an autonomous robotic device has a battery of finite capacity that has to be recharged periodically, and the total amount of energy consumed between two successive charging cycles is bounded by the capacity. Hence, a controller minimizing the mean-payoff must obey this restriction. In this paper we study the controller synthesis problem for consumption systems with a finite battery capacity, where the task of the controller is to minimize the mean-payoff while preserving the functionality of the system encoded by a given linear-time property. We show that an optimal controller always exists, and it may either need only finite memory or require infinite memory (it is decidable in polynomial time which of the two cases holds). Further, we show how to compute an effective description of an optimal controller in polynomial time. Finally, we consider the limit values achievable by larger and larger battery capacity, show that these values are computable in polynomial time, and we also analyze the corresponding rate of convergence. To the best of our knowledge, these are the first results about optimizing the long-run running costs in systems with bounded energy stores.


title: The nuXmv Symbolic Model Checker

authors:
Roberto Cavada
Alessandro Cimatti
Michele Dorigatti
Alberto Griggio
Alessandro Mariotti
Andrea Micheli
Sergio Mover
Marco Roveri
Stefano Tonetta


title: MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications

authors:
Petr Cermák
Alessio Lomuscio
Fabio Mogavero
Aniello Murano

abstract: Model checking has come of age. A number of techniques are increasingly used in industrial setting to verify hardware and software systems, both against models and concrete implementations. While it is generally accepted that obstacles still remain, notably handling infinite state systems efficiently, much of current work involves refining and improving existing techniques such as predicate abstraction.


title: Regression-Free Synthesis for Concurrency

authors:
Pavol Cerný
Thomas A. Henzinger
Arjun Radhakrishna
Leonid Ryzhyk
Thorsten Tarrach

abstract: While fixing concurrency bugs, program repair algorithms may introduce new concurrency bugs. We present an algorithm that avoids such regressions. The solution space is given by a set of program transformations we consider in for repair process. These include reordering of instructions within a thread and inserting atomic sections. The new algorithm learns a constraint on the space of candidate solutions, from both positive examples (error-free traces) and counterexamples (error traces). From each counterexample, the algorithm learns a constraint necessary to remove the errors. From each positive examples, it learns a constraint that is necessary in order to prevent the repair from turning the trace into an error trace. We implemented the algorithm and evaluated it on simplified Linux device drivers with known bugs.


title: CEGAR for Qualitative Analysis of Probabilistic Systems

authors:
Krishnendu Chatterjee
Martin Chmelik
Przemyslaw Daca

abstract: We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems.We focus on qualitative properties forMDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation ofMDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.We present an automated technique for assume-guarantee style reasoning for compositional analysis ofMDPs with qualitative properties by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We have implemented our algorithms and show that the compositional analysis leads to significant improvements.


title: G4LTL-ST: Automatic Generation of PLC Programs

authors:
Chih-Hong Cheng
Chung-Hao Huang
Harald Ruess
Stefan Stattelmann

abstract: G4LTL-ST automatically synthesizes control code for industrial Programmable Logic Controls (PLC) from timed behavioral specifications of input-output signals. These specifications are expressed in a linear temporal logic (LTL) extended with non-linear arithmetic constraints and timing constraints on signals. G4LTL-ST generates code in IEC 61131-3-compatible Structured Text, which is compiled into executable code for a large number of industrial field-level devices. The synthesis algorithm of G4LTL-ST implements pseudo-Boolean abstraction of data constraints and the compilation of timing constraints into LTL, together with a counterstrategy-guided abstraction-refinement synthesis loop. Since temporal logic specifications are notoriously difficult to use in practice, G4LTL-ST supports engineers in specifying realizable control problems by suggesting suitable restrictions on the behavior of the control environment from failed synthesis attempts.


title: Temporal Mode-Checking for Runtime Monitoring of Privacy Policies

authors:
Omar Chowdhury
Limin Jia
Deepak Garg
Anupam Datta


title: Verifying LTL Properties of Hybrid Systems with K-Liveness

authors:
Alessandro Cimatti
Alberto Griggio
Sergio Mover
Stefano Tonetta


title: Finding Instability in Biological Models

authors:
Byron Cook
Jasmin Fisher
Benjamin A. Hall
Samin Ishtiaq
Garvit Juniwal
Nir Piterman


title: QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers

authors:
Arlen Cox
Bor-Yuh Evan Chang
Sriram Sankaranarayanan


title: Symbolic Visibly Pushdown Automata

authors:
Loris D'Antoni
Rajeev Alur


title: Optimal Guard Synthesis for Memory Safety

authors:
Thomas Dillig
Isil Dillig
Swarat Chaudhuri


title: Yices 2.2


title: Synthesis of Masking Countermeasures against Side Channel Attacks

authors:
Hassan Eldib
Chao Wang


title: From LTL to Deterministic Automata: A Safraless Compositional Approach

authors:
Javier Esparza
Jan Kretínský


title: An SMT-Based Approach to Coverability Analysis

authors:
Javier Esparza
Ruslán Ledesma-Garza
Rupak Majumdar
Philipp J. Meyer
Filip Niksic


title: Vac - Verifier of Administrative Role-Based Access Control Policies

authors:
Anna Lisa Ferrara
P. Madhusudan
Truc L. Nguyen
Gennaro Parlato


title: The Spirit of Ghost Code

authors:
Jean-Christophe Filliâtre
Léon Gondelman
Andrei Paskevich


title: Regression Test Selection for Distributed Software Histories

authors:
Milos Gligoric
Rupak Majumdar
Rohan Sharma
Lamyaa Eloussi
Darko Marinov


title: A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors

authors:
Liana Hadarean
Kshitij Bansal
Dejan Jovanovic
Clark W. Barrett
Cesare Tinelli


title: Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections


title: Diamonds Are a Girl's Best Friend: Partial Order Reduction for Timed Automata with Abstractions

authors:
Henri Hansen
Shang-Wei Lin
Yang Liu
Truong Khanh Nguyen
Jun Sun


title: Termination Analysis by Learning Terminating Programs

authors:
Matthias Heizmann
Jochen Hoenicke
Andreas Podelski

abstract: We present a novel approach to termination analysis. In a first step, the analysis uses a program as a black-box which exhibits only a finite set of sample traces. Each sample trace is infinite but can be represented by a finite lasso. The analysis can "learn" a program from a termination proof for the lasso, a program that is terminating by construction. In a second step, the analysis checks that the set of sample traces is representative in a sense that we can make formal. An experimental evaluation indicates that the approach is a potentially useful addition to the portfolio of existing approaches to termination analysis.


title: Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells

authors:
Zhenqi Huang
Chuchu Fan
Alexandru Mereacre
Sayan Mitra
Marta Z. Kwiatkowska


title: Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization

authors:
Omar Inverso
Ermenegildo Tomasco
Bernd Fischer
Salvatore La Torre
Gennaro Parlato


title: Property-Directed Shape Analysis

authors:
Shachar Itzhaky
Nikolaj S. Bjørner
Thomas W. Reps
Mooly Sagiv
Aditya V. Thakur


title: A Conference Management System with Verified Document Confidentiality

authors:
Sudeep Kanav
Peter Lammich
Andrei Popescu


title: SMT-Based Model Checking for Recursive Programs

authors:
Anvesh Komuravelli
Arie Gurfinkel
Sagar Chaki


title: Causal Termination of Multi-threaded Programs

authors:
Andrey Kupriyanov
Bernd Finkbeiner


title: Proving Non-termination Using Max-SMT

authors:
Daniel Larraz
Kaustubh Nimkar
Albert Oliveras
Enric Rodríguez-Carbonell
Albert Rubio


title: Shape Analysis via Second-Order Bi-Abduction

authors:
Quang Loc Le
Cristian Gherghina
Shengchao Qin
Wei-Ngan Chin

abstract: We present a new modular shape analysis that can synthesize heap memory specification on a per method basis. We rely on a second-order biabduction mechanism that can give interpretations to unknown shape predicates. There are several novel features in our shape analysis. Firstly, it is grounded on second-order bi-abduction. Secondly, we distinguish unknown pre-predicates in pre-conditions, from unknown post-predicates in post-condition; since the former may be strengthened, while the latter may be weakened. Thirdly, we provide a new heap guard mechanism to support more precise preconditions for heap specification. Lastly, we formalise a set of derivation and normalization rules to give concise definitions for unknown predicates. Our approach has been proven sound and is implemented on top of an existing automated verification system.We show its versatility in synthesizing a wide range of intricate shape specifications.


title: Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction

authors:
Suho Lee
Karem A. Sakallah


title: Automatic Atomicity Verification for Clients of Concurrent Data Structures

authors:
Mohsen Lesani
Todd D. Millstein
Jens Palsberg


title: A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions

authors:
Tianyi Liang
Andrew Reynolds
Cesare Tinelli
Clark W. Barrett
Morgan Deters


title: Symbolic Resource Bound Inference for Functional Programs

authors:
Ravichandhran Madhavan
Viktor Kuncak


title: Lazy Annotation Revisited


title: Bit-Vector Rewriting with Automatic Rule Generation


title: Solving Games without Controllable Predecessor

authors:
Nina Narodytska
Alexander Legg
Fahiem Bacchus
Leonid Ryzhyk
Adam Walker


title: Analyzing and Synthesizing Genomic Logic Functions

authors:
Nicola Paoletti
Boyan Yordanov
Youssef Hamadi
Christoph M. Wintersteiger
Hillel Kugler


title: Automating Separation Logic with Trees and Data

authors:
Ruzica Piskac
Thomas Wies
Damien Zufferey


title: SMACK: Decoupling Source Language Details from Verifier Implementations

authors:
Zvonimir Rakamaric
Michael Emmi


title: LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes

authors:
Alejandro Sánchez
César Sánchez


title: A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis

authors:
Moritz Sinn
Florian Zuleger
Helmut Veith

abstract: We present the first scalable bound analysis that achieves amortized complexity analysis. In contrast to earlier work, our bound analysis is not based on general purpose reasoners such as abstract interpreters, software model checkers or computer algebra tools. Rather, we derive bounds directly from abstract program models, which we obtain from programs by comparatively simple invariant generation and symbolic execution techniques. As a result, we obtain an analysis that is more predictable and more scalable than earlier approaches. We demonstrate by a thorough experimental evaluation that our analysis is fast and at the same time able to compute bounds for challenging loops in a large real-world benchmark. Technically, our approach is based on lossy vector addition systems (VASS). Our bound analysis first computes a lexicographic ranking function that proves the termination of a VASS, and then derives a bound from this ranking function. Our methodology achieves amortized analysis based on a new insight how lexicographic ranking functions can be used for bound analysis.


title: A Nonlinear Real Arithmetic Fragment

authors:
Ashish Tiwari
Patrick Lincoln


title: Monadic Decomposition

authors:
Margus Veanes
Nikolaj S. Bjørner
Lev Nachmanson
Sergey Bereg


title: Interpolating Property Directed Reachability

authors:
Yakir Vizel
Arie Gurfinkel


title: AVATAR: The Architecture for First-Order Theorem Provers


title: GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components

authors:
Anton Wijs
Joost-Pieter Katoen
Dragan Bosnacki


title: Boosting k-Induction with Continuously-Refined Invariants

authors:
Dirk Beyer
Matthias Dangl
Philipp Wendler


title: Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks

authors:
Alessandro Abate
Lubos Brim
Milan Ceska
Marta Z. Kwiatkowska


title: Norn: An SMT Solver for String Constraints

authors:
Parosh Aziz Abdulla
Mohamed Faouzi Atig
Yu-Fang Chen
Lukás Holík
Ahmed Rezine
Philipp Rümmer
Jari Stenman


title: Time Robustness in MTL and Expressivity in Hybrid System Falsification

authors:
Takumi Akazaki
Ichiro Hasuo

abstract: Building on the work by Fainekos and Pappas and the one by Donze and Maler, we introduce \(\mathbf{AvSTL }\), an extension of metric interval temporal logic by averaged temporal operators. Its expressivity in capturing both space and time robustness helps solving falsification problems (searching for a critical path in hybrid system models); it does so by communicating a designer’s intention more faithfully to the stochastic optimization engine employed in a falsification solver. We also introduce a sliding window-like algorithm that keeps the cost of computing truth/robustness values tractable.


title: Synthesis Through Unification

authors:
Rajeev Alur
Pavol Cerný
Arjun Radhakrishna

abstract: Given a specification and a set of candidate programs (program space), the program synthesis problem is to find a candidate program that satisfies the specification. We present the synthesis through unification (STUN) approach, which is an extension of the counter-example guided inductive synthesis (CEGIS) approach. In CEGIS, the synthesizer maintains a subset S of inputs and a candidate program \(\mathtt {Prog}\) that is correct for S. The synthesizer repeatedly checks if there exists a counterexample input c such that the execution of \(\mathtt {Prog}\) is incorrect on c. If so, the synthesizer enlarges S to include c, and picks a program from the program space that is correct for the new set S.


title: Automatic Completion of Distributed Protocols with Symmetry

authors:
Rajeev Alur
Mukund Raghothaman
Christos Stergiou
Stavros Tripakis
Abhishek Udupa

abstract:
A distributed protocol is typically modeled as a set of communicating processes, where each process is described as an extended state machine along with fairness assumptions. Correctness is specified using safety and liveness requirements. Designing correct distributed protocols is a challenging task. Aimed at simplifying this task, we allow the designer to leave some of the guards and updates to state variables in the description of the protocol as unknown functions. The protocol completion problem then is to find interpretations for these unknown functions while guaranteeing correctness. In many distributed protocols, process behaviors are naturally symmetric, and thus, synthesized expressions are further required to obey symmetry constraints. Our counterexample-guided synthesis algorithm consists of repeatedly invoking two phases. In the first phase, candidates for unknown expressions are generated using the SMT solver Z3. This phase requires carefully orchestrating constraints to enforce the desired symmetry constraints. In the second phase, the resulting completed protocol is checked for correctness using a custom-built model checker that handles fairness assumptions, safety and liveness requirements, and exploits symmetry. When model checking fails, our tool examines a set of counterexamples to safety/liveness properties to generate constraints on unknown functions that must be satisfied by subsequent completions. For evaluation, we show that our prototype is able to automatically discover interesting missing details in distributed protocols for mutual exclusion, self stabilization, and cache coherence.
Open image in new window


title: Automata-Based Model Counting for String Constraints

authors:
Abdulbaki Aydin
Lucas Bang
Tevfik Bultan


title: The Hanoi Omega-Automata Format

authors:
Tomás Babiak
Frantisek Blahoudek
Alexandre Duret-Lutz
Joachim Klein
Jan Kretínský
David Müller
David Parker
Jan Strejcek


title: Using Minimal Correction Sets to More Efficiently Compute Minimal Unsatisfiable Sets

authors:
Fahiem Bacchus
George Katsirelos


title: Deciding Local Theory Extensions via E-matching

authors:
Kshitij Bansal
Andrew Reynolds
Tim King
Clark W. Barrett
Thomas Wies

abstract: Satisfiability Modulo Theories (SMT) solvers incorporate decision procedures for theories of data types that commonly occur in software. This makes them important tools for automating verification problems. A limitation frequently encountered is that verification problems are often not fully expressible in the theories supported natively by the solvers. Many solvers allow the specification of application-specific theories as quantified axioms, but their handling is incomplete outside of narrow special cases.


title: Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions

authors:
Amir M. Ben-Amram
Samir Genaim

abstract: In this paper we turn the spotlight on a class of lexicographic ranking functions introduced by Bradley, Manna and Sipma in a seminal CAV 2005 paper, and establish for the first time the complexity of some problems involving the inference of such functions for linear-constraint loops (without precondition). We show that finding such a function, if one exists, can be done in polynomial time in a way which is sound and complete when the variables range over the rationals (or reals). We show that when variables range over the integers, the problem is harder—deciding the existence of a ranking function is coNP-complete. Next, we study the problem of minimizing the number of components in the ranking function (a.k.a. the dimension). This number is interesting in contexts like computing iteration bounds and loop parallelization. Surprisingly, and unlike the situation for some other classes of lexicographic ranking functions, we find that even deciding whether a two-component ranking function exists is harder than the unrestricted problem: NP-complete over the rationals and \(\varSigma ^P_2\)-complete over the integers.


title: Efficient Anytime Techniques for Model-Based Safety Analysis

authors:
Marco Bozzano
Alessandro Cimatti
Alberto Griggio
Cristian Mattarei


title: Formal Design and Safety Analysis of AIR6110 Wheel Brake System

authors:
Marco Bozzano
Alessandro Cimatti
Anthony Fernandes Pires
David Jones
Greg Kimberly
T. Petri
R. Robinson
Stefano Tonetta


title: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes

authors:
Tomás Brázdil
Krishnendu Chatterjee
Martin Chmelik
Andreas Fellner
Jan Kretínský

abstract: For deterministic systems, a counterexample to a property can simply be an error trace, whereas counterexamples in probabilistic systems are necessarily more complex. For instance, a set of erroneous traces with a sufficient cumulative probability mass can be used. Since these are too large objects to understand and manipulate, compact representations such as subchains have been considered. In the case of probabilistic systems with non-determinism, the situation is even more complex. While a subchain for a given strategy (or scheduler, resolving non-determinism) is a straightforward choice, we take a different approach. Instead, we focus on the strategy itself, and extract the most important decisions it makes, and present its succinct representation.


title: Pareto Curves of Multidimensional Mean-Payoff Games

authors:
Romain Brenguier
Jean-François Raskin


title: From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis

authors:
Pavol Cerný
Edmund M. Clarke
Thomas A. Henzinger
Arjun Radhakrishna
Leonid Ryzhyk
Roopsha Samanta
Thorsten Tarrach


title: Word-Level Symbolic Trajectory Evaluation

authors:
Supratik Chakraborty
Zurab Khasidashvili
Carl-Johan H. Seger
Rajkumar Gajavelly
Tanmay Haldankar
Dinesh Chhatani
Rakesh Mistry

abstract: Symbolic trajectory evaluation (STE) is a model checking technique that has been successfully used to verify industrial designs. Existing implementations of STE, however, reason at the level of bits, allowing signals to take values in \(\{0, 1, X\}\). This limits the amount of abstraction that can be achieved, and presents inherent limitations to scaling. The main contribution of this paper is to show how much more abstract lattices can be derived automatically from RTL descriptions, and how a model checker for the general theory of STE instantiated with such abstract lattices can be implemented in practice. This gives us the first practical word-level STE engine, called \(\mathsf {STEWord}\). Experiments on a set of designs similar to those used in industry show that \(\mathsf {STEWord}\) scales better than word-level BMC and also bit-level STE.


title: Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs

authors:
Krishnendu Chatterjee
Rasmus Ibsen-Jensen
Andreas Pavlogiannis

abstract:
We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff property, the ratio property, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with constant treewidth, and it is well-known that the control-flow graphs of most programs have constant treewidth. Let n denote the number of nodes of a graph, m the number of edges (for constant treewidth graphs \(m=O(n)\)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a multiplicative factor of \(\epsilon \) in time \(O(n \cdot \log (n/\epsilon ))\) and linear space, as compared to the classical algorithms that require quadratic time. Second, for the ratio property we present an algorithm that for constant treewidth graphs works in time \(O(n \cdot \log (|a\cdot b|))=O(n\cdot \log (n\cdot W))\), when the output is \(\frac{a}{b}\), as compared to the previously best known algorithm with running time \(O(n^2 \cdot \log (n\cdot W))\). Third, for the minimum initial credit problem we show that (i) for general graphs the problem can be solved in \(O(n^2\cdot m)\) time and the associated decision problem can be solved in \(O(n\cdot m)\) time, improving the previous known \(O(n^3\cdot m\cdot \log (n\cdot W))\) and \(O(n^2 \cdot m)\) bounds, respectively; and (ii) for constant treewidth graphs we present an algorithm that requires \(O(n\cdot \log n)\) time, improving the previous known \(O(n^4 \cdot \log (n \cdot W))\) bound. We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks.
Open image in new window


title: Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation

authors:
Yu-Fang Chen
Chih-Duo Hong
Bow-Yaw Wang
Lijun Zhang

abstract: We apply multivariate Lagrange interpolation to synthesizing polynomial quantitative loop invariants for probabilistic programs. We reduce the computation of a quantitative loop invariant to solving constraints over program variables and unknown coefficients. Lagrange interpolation allows us to find constraints with less unknown coefficients. Counterexample-guided refinement furthermore generates linear constraints that pinpoint the desired quantitative invariants. We evaluate our technique by several case studies with polynomial quantitative loop invariants in the experiments.


title: Cutting the Mix

authors:
Jürgen Christ
Jochen Hoenicke


title: On Automation of CTL* Verification for Infinite-State Systems

authors:
Byron Cook
Heidy Khlaaf
Nir Piterman

abstract: In this paper we introduce the first known fully automated tool for symbolically proving CTL \(^*\) properties of (infinite-state) integer programs. The method uses an internal encoding which facilitates reasoning about the subtle interplay between the nesting of path and state temporal operators that occurs within CTL \(^*\) proofs. A precondition synthesis strategy is then used over a program transformation which trades nondeterminism in the transition relation for nondeterminism explicit in variables predicting future outcomes when necessary. We show the viability of our approach in practice using examples drawn from device drivers and various industrial examples.


title: Conflict-Driven Conditional Termination

authors:
Vijay D'Silva
Caterina Urban


title: Angelic Verification: Precise Verification Modulo Unknowns

authors:
Ankush Das
Shuvendu K. Lahiri
Akash Lal
Yi Li


title: PROPhESY: A PRObabilistic ParamEter SYnthesis Tool

authors:
Christian Dehnert
Sebastian Junges
Nils Jansen
Florian Corzilius
Matthias Volk
Harold Bruintjes
Joost-Pieter Katoen
Erika Ábrahám


title: Empirical Software Metrics for Benchmarking of Verification Tools

authors:
Yulia Demyanova
Thomas Pani
Helmut Veith
Florian Zuleger


title: Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems

authors:
Ankush Desai
Sanjit A. Seshia
Shaz Qadeer
David Broman
John C. Eidson


title: Quantifying Conformance Using the Skorokhod Metric

authors:
Jyotirmoy V. Deshmukh
Rupak Majumdar
Vinayak S. Prabhu


title: Fairness Modulo Theory: A New Approach to LTL Software Model Checking

authors:
Daniel Dietsch
Matthias Heizmann
Vincent Langenfeld
Andreas Podelski


title: Meeting a Powertrain Verification Challenge

authors:
Parasara Sridhar Duggirala
Chuchu Fan
Sayan Mitra
Mahesh Viswanathan


title: Model Checking Parameterized Asynchronous Shared-Memory Systems

authors:
Antoine Durand-Gasselin
Javier Esparza
Pierre Ganty
Rupak Majumdar


title: Finding Bounded Path in Graph Using SMT for Automatic Clock Routing

authors:
Amit Erez
Alexander Nadel


title: Measuring with Timed Patterns

authors:
Thomas Ferrère
Oded Maler
Dejan Nickovic
Dogan Ulus


title: Adam: Causality-Based Synthesis of Distributed Systems

authors:
Bernd Finkbeiner
Manuel Gieseking
Ernst-Rüdiger Olderog


title: Algorithms for Model Checking HyperLTL and HyperCTL ^*

authors:
Bernd Finkbeiner
Markus N. Rabe
César Sánchez


title: Synthesising Executable Gene Regulatory Networks from Single-Cell Gene Expression Data

authors:
Jasmin Fisher
Ali Sinan Köksal
Nir Piterman
Steven Woodhouse

abstract: Recent experimental advances in biology allow researchers to obtain gene expression profiles at single-cell resolution over hundreds, or even thousands of cells at once. These single-cell measurements provide snapshots of the states of the cells that make up a tissue, instead of the population-level averages provided by conventional high-throughput experiments. This new data therefore provides an exciting opportunity for computational modelling. In this paper we introduce the idea of viewing single-cell gene expression profiles as states of an asynchronous Boolean network, and frame model inference as the problem of reconstructing a Boolean network from its state space. We then give a scalable algorithm to solve this synthesis problem. We apply our technique to both simulated and real data. We first apply our technique to data simulated from a well established model of common myeloid progenitor differentiation. We show that our technique is able to recover the original Boolean network rules. We then apply our technique to a large dataset taken during embryonic development containing thousands of cell measurements. Our technique synthesises matching Boolean networks, and analysis of these models yields new predictions about blood development which our experimental collaborators were able to verify.


title: A Trusted Mechanised Specification of JavaScript: One Year On

authors:
Philippa Gardner
Gareth Smith
Conrad Watt
Thomas Wood


title: Learning Commutativity Specifications

authors:
Timon Gehr
Dimitar Dimitrov
Martin T. Vechev


title: Symbolic Polytopes for Quantitative Interpolation and Verification

authors:
Klaus von Gleissenthall
Boris Köpf
Andrey Rybalchenko


title: OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case

authors:
Stijn de Gouw
Jurriaan Rot
Frank S. de Boer
Richard Bubel
Reiner Hähnle


title: Tree Buffers

authors:
Radu Grigore
Stefan Kiefer

abstract: In runtime verification, the central problem is to decide if a given program execution violates a given property. In online runtime verification, a monitor observes a program's execution as it happens. If the program being observed has hard real-time constraints, then the monitor inherits them. In the presence of hard real-time constraints it becomes a challenge to maintain enough information to produce error traces, should a property violation be observed. In this paper we introduce a data structure, called tree buffer, that solves this problem in the context of automata-based monitors: If the monitor itself respects hard real-time constraints, then enriching it by tree buffers makes it possible to provide error traces, which are essential for diagnosing defects. We show that tree buffers are also useful in other application domains. For example, they can be used to implement functionality of capturing groups in regular expressions. We prove optimal asymptotic bounds for our data structure, and validate them using empirical data from two sources: regular expression searching through Wikipedia, and runtime verification of execution traces obtained from the Dacapo test suite.


title: The SeaHorn Verification Framework

authors:
Arie Gurfinkel
Temesghen Kahsai
Anvesh Komuravelli
Jorge A. Navas


title: Automated and Modular Refinement Reasoning for Concurrent Programs

authors:
Chris Hawblitzel
Erez Petrank
Shaz Qadeer
Serdar Tasiran


title: The Open-Source LearnLib - A Framework for Active Automata Learning

authors:
Malte Isberner
Falk Howar
Bernhard Steffen


title: Skipping Refinement

authors:
Mitesh Jain
Panagiotis Manolios

abstract: We introduce skipping refinement, a new notion of correctness for reasoning about optimized reactive systems. Reasoning about reactive systems using refinement involves defining an abstract, highlevel specification system and a concrete, low-level implementation system. One then shows that every behavior allowed by the implementation is also allowed by the specification. Due to the difference in abstraction levels, it is often the case that the implementation requires many steps to match one step of the specification, hence, it is quite useful for refinement to directly account for stuttering. Some optimized implementations, however, can actually take multiple specification steps at once. For example, a memory controller can buffer the commands to the memory and at a later time simultaneously update multiple memory locations, thereby skipping several observable states of the abstract specification, which only updates one memory location at a time. We introduce skipping simulation refinement and provide a sound and complete characterization consisting of “local” proof rules that are amenable to mechanization and automated verification. We present case studies that highlight the applicability of skipping refinement: a JVM-inspired stack machine, a simple memory controller and a scalar to vector compiler transformation. Our experimental results demonstrate that current model-checking and automated theorem proving tools have difficultly automatically analyzing these systems using existing notions of correctness, but they can analyze the systems if we use skipping refinement.


title: Adaptive Concretization for Parallel Program Synthesis

authors:
Jinseong Jeon
Xiaokang Qiu
Armando Solar-Lezama
Jeffrey S. Foster

abstract:
Program synthesis tools work by searching for an implementation that satisfies a given specification. Two popular search strategies are symbolic search, which reduces synthesis to a formula passed to a SAT solver, and explicit search, which uses brute force or random search to find a solution. In this paper, we propose adaptive concretization, a novel synthesis algorithm that combines the best of symbolic and explicit search. Our algorithm works by partially concretizing a randomly chosen, but likely highly influential, subset of the unknowns to be synthesized. Adaptive concretization uses an online search process to find the optimal size of the concretized subset using a combination of exponential hill climbing and binary search, employing a statistical test to determine when one degree of concretization is sufficiently better than another. Moreover, our algorithm lends itself to a highly parallel implementation, further speeding up search. We implemented adaptive concretization for Sketch and evaluated it on a range of benchmarks. We found adaptive concretization is very effective, outperforming Sketch in many cases, sometimes significantly, and has good parallel scalability.
Open image in new window


title: Property-Directed Inference of Universal Invariants or Proving Their Absence

authors:
Aleksandr Karbyshev
Nikolaj S. Bjørner
Shachar Itzhaky
Noam Rinetzky
Sharon Shoham


title: Deductive Program Repair

authors:
Etienne Kneuss
Manos Koukoutos
Viktor Kuncak

abstract: We present an approach to program repair and its application to programs with recursive functions over unbounded data types. Our approach formulates program repair in the framework of deductive synthesis that uses existing program structure as a hint to guide synthesis. We introduce a new specification construct for symbolic tests. We rely on such user-specified tests as well as automatically generated ones to localize the fault and speed up synthesis. Our implementation is able to eliminate errors within seconds from a variety of functional programs, including symbolic computation code and implementations of functional data structures. The resulting programs are formally verified by the Leon system.


title: SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms

authors:
Igor Konnov
Helmut Veith
Josef Widder


title: Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs

authors:
Takuya Kuwahara
Ryosuke Sato
Hiroshi Unno
Naoki Kobayashi


title: Automatic Rootcausing for Program Equivalence Failures in Binaries

authors:
Shuvendu K. Lahiri
Rohit Sinha
Chris Hawblitzel


title: Fine-Grained Caching of Verification Results

authors:
K. Rustan M. Leino
Valentin Wüstholz


title: Verifying Linearizability of Intel® Software Guard Extensions

authors:
Rebekah Leslie-Hurd
Dror Caspi
Matthew Fernandez


title: Bbs: A Phase-Bounded Model Checker for Asynchronous Programs

authors:
Rupak Majumdar
Zilong Wang


title: The Inez Mathematical Programming Modulo Theories Framework

authors:
Panagiotis Manolios
Jorge Pais
Vasilis Papavasileiou


title: An Axiomatic Specification for Sequential Memory Models

authors:
William Mansky
Dmitri Garbuzov
Steve Zdancewic


title: PVSio-web 2.0: Joining PVS to HCI

authors:
Paolo Masci
Patrick Oladimeji
Yi Zhang
Paul L. Jones
Paul Curzon
Harold W. Thimbleby


title: Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation

authors:
Mendes Oulamara
Arnaud J. Venet

abstract: The inference and the verification of numerical relationships among variables of a program is one of the main goals of static analysis. In this paper, we propose an Abstract Interpretation framework based on higher-dimensional ellipsoids to automatically discover symbolic quadratic invariants within loops, using loop counters as implicit parameters. In order to obtain non-trivial invariants, the diameter of the set of values taken by the numerical variables of the program has to evolve (sub-)linearly during loop iterations. These invariants are called ellipsoidal cones and can be seen as an extension of constructs used in the static analysis of digital filters. Semidefinite programming is used to both compute the numerical results of the domain operations and provide proofs (witnesses) of their correctness.


title: Systematic Asynchrony Bug Exploration for Android Apps

authors:
Burcu Kulahcioglu Ozkan
Michael Emmi
Serdar Tasiran


title: Percentile Queries in Multi-dimensional Markov Decision Processes

authors:
Mickael Randour
Jean-François Raskin
Ocan Sankur


title: A Type-Directed Approach to Program Repair

authors:
Alex Reinking
Ruzica Piskac


title: Counterexample-Guided Quantifier Instantiation for Synthesis in SMT

authors:
Andrew Reynolds
Morgan Deters
Viktor Kuncak
Cesare Tinelli
Clark W. Barrett

abstract:
We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided techniques for quantifier instantiation that we use to make finding such proofs practically feasible. A particularly important class of specifications are single-invocation properties, for which we present a dedicated algorithm. To support syntax restrictions on generated solutions, our approach can transform a solution found without restrictions into the desired syntactic form. As an alternative, we show how to use evaluation function axioms to embed syntactic restrictions into constraints over algebraic datatypes, and then use an algebraic datatype decision procedure to drive synthesis. Our experimental evaluation on syntax-guided synthesis benchmarks shows that our implementation in the CVC4 SMT solver is competitive with state-of-the-art tools for synthesis.
Open image in new window


title: Alchemist: Learning Guarded Affine Functions

authors:
Shambwaditya Saha
Pranav Garg
P. Madhusudan


title: OptiMathSAT: A Tool for Optimization Modulo Theories

authors:
Roberto Sebastiani
Patrick Trentin


title: Predicting a Correct Program in Programming by Example

authors:
Rishabh Singh
Sumit Gulwani


title: Time-Aware Abstractions in HybridSal


title: Modular Deductive Verification of Multiprocessor Hardware Designs

authors:
Muralidaran Vijayaraghavan
Adam Chlipala
Arvind
Nirav Dave

abstract: We present a new framework for modular verification of hardware designs in the style of the Bluespec language. That is, we formalize the idea of components in a hardware design, with well-defined input and output channels; and we show how to specify and verify components individually, with machine-checked proofs in the Coq proof assistant. As a demonstration, we verify a fairly realistic implementation of a multicore shared-memory system with two types of components: memory system and processor. Both components include nontrivial optimizations, with the memory system employing an arbitrary hierarchy of cache nodes that communicate with each other concurrently, and with the processor doing speculative execution of many concurrent read operations. Nonetheless, we prove that the combined system implements sequential consistency. To our knowledge, our memory-system proof is the first machine verification of a cache-coherence protocol parameterized over an arbitrary cache hierarchy, and our full-system proof is the first machine verification of sequential consistency for a multicore hardware design that includes caches and speculative processors.


title: Fast Interpolating BMC

authors:
Yakir Vizel
Arie Gurfinkel
Sharad Malik


title: Effective Search-Space Pruning for Solvers of String Equations, Regular Expressions and Length Constraints

authors:
Yunhui Zheng
Vijay Ganesh
Sanu Subramanian
Omer Tripp
Julian Dolby
Xiangyu Zhang


title: Poling: SMT Aided Linearizability Proofs

authors:
He Zhu
Gustavo Petri
Suresh Jagannathan


title: Automatic Verification of Stability and Safety for Delay Differential Equations

authors:
Liang Zou
Martin Fränzle
Naijun Zhan
Peter Nazier Mosaad


title: Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses

authors:
Dirk Beyer
Matthias Dangl


title: Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution

authors:
Peter Müller
Malte Schwerhoff
Alexander J. Summers

abstract:
In permission logics such as separation logic, the iterated separating conjunction is a quantifier denoting access permission to an unbounded set of heap locations. In contrast to recursive predicates, iterated separating conjunctions do not prescribe a structure on the locations they range over, and so do not restrict how to traverse and modify these locations. This flexibility is important for the verification of random-access data structures such as arrays and data structures that can be traversed in multiple ways such as graphs. Despite its usefulness, no automatic program verifier natively supports iterated separating conjunctions; they are especially difficult to incorporate into symbolic execution engines, the prevalent technique for building verifiers for these logics.
In this paper, we present the first symbolic execution technique to support general iterated separating conjunctions. We propose a novel representation of symbolic heaps and flexible support for logical specifications that quantify over heap locations. Our technique exhibits predictable and fast performance despite employing quantifiers at the SMT level, by carefully controlling quantifier instantiations. It is compatible with other features of permission logics such as fractional permissions, recursive predicates, and abstraction functions. Our technique is implemented as an extension of the Viper verification infrastructure.


title: Stateless Model Checking for POWER

authors:
Parosh Aziz Abdulla
Mohamed Faouzi Atig
Bengt Jonsson
Carl Leonardsson

abstract: We present the first framework for efficient application of stateless model checking (SMC) to programs running under the relaxed memory model of POWER. The framework combines several contributions. The first contribution is that we develop a scheme for systematically deriving operational execution models from existing axiomatic ones. The scheme is such that the derived execution models are well suited for efficient SMC. We apply our scheme to the axiomatic model of POWER from [8]. Our main contribution is a technique for efficient SMC, called Relaxed Stateless Model Checking (RSMC), which systematically explores the possible inequivalent executions of a program. RSMC is suitable for execution models obtained using our scheme. We prove that RSMC is sound and optimal for the POWER memory model, in the sense that each complete program behavior is explored exactly once. We show the feasibility of our technique by providing an implementation for programs written in C/pthreads.


title: Compositional Synthesis of Reactive Controllers for Multi-agent Systems

authors:
Rajeev Alur
Salar Moarref
Ufuk Topcu


title: Markov Chains and Unambiguous Büchi Automata

authors:
Christel Baier
Stefan Kiefer
Joachim Klein
Sascha Klüppelholz
David Müller
James Worrell


title: Synthesizing Probabilistic Invariants via Doob's Decomposition

authors:
Gilles Barthe
Thomas Espitau
Luis María Ferrer Fioriti
Justin Hsu

abstract:
When analyzing probabilistic computations, a powerful approach is to first find a martingale---an expression on the program variables whose expectation remains invariant---and then apply the optional stopping theorem in order to infer properties at termination time. One of the main challenges, then, is to systematically find martingales.
We propose a novel procedure to synthesize martingale expressions from an arbitrary initial expression. Contrary to state-of-the-art approaches, we do not rely on constraint solving. Instead, we use a symbolic construction based on Doob's decomposition. This procedure can produce very complex martingales, expressed in terms of conditional expectations.
We show how to automatically generate and simplify these martingales, as well as how to apply the optional stopping theorem to infer properties at termination time. This last step typically involves some simplification steps, and is usually done manually in current approaches. We implement our techniques in a prototype tool and demonstrate our process on several classical examples. Some of them go beyond the capability of current semi-automatic approaches.


title: Solving Parity Games via Priority Promotion

authors:
Massimo Benerecetti
Daniele Dell'Erba
Fabio Mogavero


title: Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems

authors:
Roderick Bloem
Nicolas Braud-Santoni
Swen Jacobs

abstract: Fault-tolerant distributed algorithms play an increasingly important role in many applications, and their correct and efficient implementation is notoriously difficult. We present an automatic approach to synthesise provably correct fault-tolerant distributed algorithms from formal specifications in linear-time temporal logic. The supported system model covers synchronous reactive systems with finite local state, while the failure model includes strong self-stabilisation as well as Byzantine failures. The synthesis approach for a fixed-size network of processes is complete for realisable specifications, and can optimise the solution for small implementations and short stabilisation time. To solve the bounded synthesis problem with Byzantine failures more efficiently, we design an incremental, CEGIS-like loop. Finally, we define two classes of problems for which our synthesis algorithm obtains solutions that are not only correct in fixed-size networks, but in networks of arbitrary size.


title: Symbolic Optimal Reachability in Weighted Timed Automata

authors:
Patricia Bouyer
Maximilien Colange
Nicolas Markey

abstract: Weighted timed automata have been defined in the early 2000 s for modelling resource-consumption or -allocation problems in real-time systems. Optimal reachability is decidable in weighted timed automata, and a symbolic forward algorithm has been developed to solve that problem. This algorithm uses so-called priced zones, an extension of standard zones with cost functions. In order to ensure termination, the algorithm requires clocks to be bounded. For unpriced timed automata, much work has been done to develop sound abstractions adapted to the forward exploration of timed automata, ensuring termination of the model-checking algorithm without bounding the clocks. In this paper, we take advantage of recent developments on abstractions for timed automata, and propose an algorithm allowing for symbolic analysis of all weighted timed automata, without requiring bounded clocks.


title: The Kind 2 Model Checker

authors:
Adrien Champion
Alain Mebsout
Christoph Sticksel
Cesare Tinelli


title: Termination Analysis of Probabilistic Programs Through Positivstellensatz's

authors:
Krishnendu Chatterjee
Hongfei Fu
Amir Kafshdar Goharshady

abstract: We consider nondeterministic probabilistic programs with the most basic liveness property of termination. We present efficient methods for termination analysis of nondeterministic probabilistic programs with polynomial guards and assignments. Our approach is through synthesis of polynomial ranking supermartingales, that on one hand significantly generalizes linear ranking supermartingales and on the other hand is a counterpart of polynomial ranking-functions for proving termination of nonprobabilistic programs. The approach synthesizes polynomial ranking-supermartingales through Positivstellensatz’s, yielding an efficient method which is not only sound, but also semi-complete over a large subclass of programs. We show experimental results to demonstrate that our approach can handle several classical programs with complex polynomial guards and assignments, and can synthesize efficient quadratic ranking-supermartingales when a linear one does not exist even for simple affine programs.


title: The Commutativity Problem of the MapReduce Framework: A Transducer-Based Approach

authors:
Yu-Fang Chen
Lei Song
Zhilin Wu

abstract: MapReduce is a popular programming model for data parallel computation. In MapReduce, the reducer produces an output from a list of inputs. Due to the scheduling policy of the platform, the inputs may arrive at the reducers in different order. The commutativity problem of reducers asks if the output of a reducer is independent of the order of its inputs. Although the problem is undecidable in general, the MapReduce programs in practice are usually used for data analytics and thus require very simple control flow. By exploiting the simplicity, we propose a programming language for reducers where the commutativity problem is decidable. The main idea of the reducer language is to separate the control and data flow of programs and disallow arithmetic operations in the control flow. The decision procedure for the commutativity problem is obtained through a reduction to the equivalence problem of streaming numerical transducers (SNTs), a novel automata model over infinite alphabets introduced in this paper. The design of SNTs is inspired by streaming transducers (Alur and Cerny, POPL 2011). Nevertheless, the two models are intrinsically different since the outputs of SNTs are integers while those of streaming transducers are data words. The decidability of the equivalence of SNTs is achieved with an involved combinatorial analysis of the evolvement of the values of the integer variables during the runs of SNTs.


title: Structural Synthesis for GXW Specifications

authors:
Chih-Hong Cheng
Yassine Hamza
Harald Ruess

abstract: We define the \(\textsf {\small {GXW}} \) fragment of linear temporal logic (LTL) as the basis for synthesizing embedded control software for safety-critical applications. Since \(\textsf {\small {GXW}} \) includes the use of a weak-until operator we are able to specify a number of diverse programmable logic control (PLC) problems, which we have compiled from industrial training sets. For \(\textsf {\small {GXW}} \) controller specifications, we develop a novel approach for synthesizing a set of synchronously communicating actor-based controllers. This synthesis algorithm proceeds by means of recursing over the structure of \(\textsf {\small {GXW}} \) specifications, and generates a set of dedicated and synchronously communicating sub-controllers according to the formula structure. In a subsequent step, 2QBF constraint solving identifies and tries to resolve potential conflicts between individual \(\textsf {\small {GXW}} \) specifications. This structural approach to \(\textsf {\small {GXW}} \) synthesis supports traceability between requirements and the generated control code as mandated by certification regimes for safety-critical software. Our experimental results suggest that GXW synthesis scales well to industrial-sized control synthesis problems with 20 input and output ports and beyond.


title: Hitting Families of Schedules for Asynchronous Programs

authors:
Dmitry Chistikov
Rupak Majumdar
Filip Niksic

abstract: We consider the following basic task in the testing of concurrent systems. The input to the task is a partial order of events, which models actions performed on or by the system and specifies ordering constraints between them. The task is to determine if some scheduling of these events can result in a bug. The number of schedules to be explored can, in general, be exponential.


title: A Decision Procedure for Sets, Binary Relations and Partial Functions

authors:
Maximiliano Cristiá
Gianfranco Rossi


title: Qlose: Program Repair with Quantitative Objectives

authors:
Loris D'Antoni
Roopsha Samanta
Rishabh Singh


title: Array Folds Logic

authors:
Przemyslaw Daca
Thomas A. Henzinger
Andrey Kupriyanov

abstract: We present an extension to the quantifier-free theory of integer arrays which allows us to express counting. The properties expressible in Array Folds Logic (AFL) include statements such as “the first array cell contains the array length,” and “the array contains equally many minimal and maximal elements.” These properties cannot be expressed in quantified fragments of the theory of arrays, nor in the theory of concatenation. Using reduction to counter machines, we show that the satisfiability problem of AFL is PSPACE-complete, and with a natural restriction the complexity decreases to NP. We also show that adding either universal quantifiers or concatenation leads to undecidability.


title: Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations

authors:
Jakub Daniel
Alessandro Cimatti
Alberto Griggio
Stefano Tonetta
Sergio Mover


title: Proving Parameterized Systems Safe by Generalizing Clausal Proofs of Small Instances

authors:
Michael Dooley
Fabio Somenzi


title: Effectively Propositional Interpolants

authors:
Samuel Drews
Aws Albarghouthi


title: Parsimonious, Simulation Based Verification of Linear Systems

authors:
Parasara Sridhar Duggirala
Mahesh Viswanathan


title: Slugs: Extensible GR(1) Synthesis

authors:
Rüdiger Ehlers
Vasumathi Raman


title: Synthesis of Fault-Attack Countermeasures for Cryptographic Circuits

authors:
Hassan Eldib
Meng Wu
Chao Wang


title: Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement

authors:
Karam Abd Elkader
Orna Grumberg
Corina S. Pasareanu
Sharon Shoham


title: Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2

authors:
Chuchu Fan
Bolun Qi
Sayan Mitra
Mahesh Viswanathan
Parasara Sridhar Duggirala


title: Property Directed Equivalence via Abstract Simulation

authors:
Grigory Fedyukovich
Arie Gurfinkel
Natasha Sharygina


title: Bounded Cycle Synthesis

authors:
Bernd Finkbeiner
Felix Klein

abstract: We introduce a new approach for the synthesis of Mealy machines from specifications in linear-time temporal logic (LTL), where the number of cycles in the state graph of the implementation is limited by a given bound. Bounding the number of cycles leads to implementations that are structurally simpler and easier to understand. We solve the synthesis problem via an extension of SAT-based bounded synthesis, where we additionally construct a witness structure that limits the number of cycles. We also establish a triple-exponential upper and lower bound for the potential blow-up between the length of the LTL formula and the number of cycles in the state graph.


title: Combining Model Learning and Model Checking to Analyze TCP Implementations

authors:
Paul Fiterau-Brostean
Ramon Janssen
Frits W. Vaandrager


title: BDD-Based Boolean Functional Synthesis

authors:
Dror Fried
Lucas M. Tabajara
Moshe Y. Vardi


title: XSat: A Fast Floating-Point Satisfiability Solver

authors:
Zhoulai Fu
Zhendong Su


title: Model Checking at Scale: Automated Air Traffic Control Design Space Exploration

authors:
Marco Gario
Alessandro Cimatti
Cristian Mattarei
Stefano Tonetta
Kristin Yvonne Rozier


title: PSI: Exact Symbolic Inference for Probabilistic Programs

authors:
Timon Gehr
Sasa Misailovic
Martin T. Vechev


title: RV-Match: Practical Semantics-Based Program Analysis

authors:
Dwight Guth
Chris Hathhorn
Manasvi Saxena
Grigore Rosu


title: A Simple Algorithm for Solving Qualitative Probabilistic Parity Games

authors:
Ernst Moritz Hahn
Sven Schewe
Andrea Turrini
Lijun Zhang


title: Learning-Based Assume-Guarantee Regression Verification

authors:
Fei He
Shu Mao
Bow-Yaw Wang


title: ParCoSS: Efficient Parallelized Compiled Symbolic Simulation

authors:
Vladimir Herdt
Hoang Minh Le
Daniel Große
Rolf Drechsler


title: Soufflé: On Synthesis of Program Analyzers

authors:
Herbert Jordan
Bernhard Scholz
Pavle Subotic


title: Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata

authors:
Bishoksan Kafle
John P. Gallagher
José F. Morales


title: JayHorn: A Framework for Verifying Java programs

authors:
Temesghen Kahsai
Philipp Rümmer
Huascar Sanchez
Martin Schäf


title: Fast, Flexible, and Minimal CTL Synthesis via SMT

authors:
Tobias Klenze
Sam Bayless
Alan J. Hu


title: Satisfiability Modulo Heap-Based Programs

authors:
Quang Loc Le
Jun Sun
Wei-Ngan Chin


title: A SAT-Based Counterexample Guided Method for Unbounded Synthesis

authors:
Alexander Legg
Nina Narodytska
Leonid Ryzhyk


title: Trigger Selection Strategies to Stabilize Program Verifiers

authors:
K. Rustan M. Leino
Clément Pit-Claudel

abstract: SMT-based program verifiers often suffer from the so-called butterfly effect, in which minor modifications to the program source cause significant instabilities in verification times, which in turn may lead to spurious verification failures and a degraded user experience. This paper identifies matching loops (ill-behaved quantifiers causing an SMT solver to repeatedly instantiate a small set of quantified formulas) as a significant contributor to these instabilities, and describes some techniques to detect and prevent them. At their core, the contributed techniques move the trigger selection logic away from the SMT solver and into the high-level verifier: this move allows authors of verifiers to annotate, rewrite, and analyze user-written quantifiers to improve the solver’s performance, using information that is easily available at the source level but would be hard to extract from the heavily encoded terms that the solver works with. The paper demonstrates three core techniques (quantifier splitting, trigger sharing, and matching loop detection) by extending the Dafny verifier with its own trigger selection routine, and demonstrates significant predictability and performance gains on both Dafny’s test suite and large verification efforts using Dafny.


title: Liveness of Randomised Parameterised Systems under Arbitrary Schedulers

authors:
Anthony W. Lin
Philipp Rümmer

abstract: We consider the problem of verifying liveness for systems with a finite, but unbounded, number of processes, commonly known as parameterised systems. Typical examples of such systems include distributed protocols (e.g. for the dining philosopher problem). Unlike the case of verifying safety, proving liveness is still considered extremely challenging, especially in the presence of randomness in the system. In this paper we consider liveness under arbitrary (including unfair) schedulers, which is often considered a desirable property in the literature of self-stabilising systems. We introduce an automatic method of proving liveness for randomised parameterised systems under arbitrary schedulers. Viewing liveness as a two-player reachability game (between Scheduler and Process), our method is a CEGAR approach that synthesises a progress relation for Process that can be symbolically represented as a finite-state automaton. The method is incremental and exploits both Angluin-style L*-learning and SAT-solvers. Our experiments show that our algorithm is able to prove liveness automatically for well-known randomised distributed protocols, including Lehmann-Rabin Randomised Dining Philosopher Protocol and randomised self-stabilising protocols (such as the Israeli-Jalfon Protocol). To the best of our knowledge, this is the first fully-automatic method that can prove liveness for randomised protocols.


title: From Shape Analysis to Termination Analysis in Linear Time

authors:
Roman Manevich
Boris Dogadov
Noam Rinetzky


title: PSCV: A Runtime Verification Tool for Probabilistic SystemC Models

authors:
Van Chan Ngo
Axel Legay
Vania Joloboff


title: Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories

authors:
Aina Niemetz
Mathias Preiner
Armin Biere


title: Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers

authors:
Stuart Pernsteiner
Calvin Loncaric
Emina Torlak
Zachary Tatlock
Xi Wang
Michael D. Ernst
Jonathan Jacky


title: Counterexample Guided Abstraction Refinement for Stability Analysis

authors:
Pavithra Prabhakar
Miriam Garcia Soto


title: End-to-End Verification of Processors with ISA-Formal

authors:
Alastair Reid
Rick Chen
Anastasios Deligiannis
David Gilday
David Hoyes
Will Keen
Ashan Pathirane
Owen Shepherd
Peter Vrabel
Ali Zaidi


title: Probabilistic Automated Language Learning for Configuration Files

authors:
Mark Santolucito
Ennan Zhai
Ruzica Piskac


title: BigraphER: Rewriting and Analysis Engine for Bigraphs

authors:
Michele Sevegnani
Muffy Calder


title: Limit-Deterministic Büchi Automata for Linear Temporal Logic

authors:
Salomon Sickert
Javier Esparza
Stefan Jaax
Jan Kretínský


title: Progressive Reasoning over Recursively-Defined Strings

authors:
Minh-Thai Trinh
Duc-Hiep Chu
Joxan Jaffar


title: String Analysis via Automata Manipulation with Logic Circuit Representation

authors:
Hung-En Wang
Tzung-Lin Tsai
Chun-Han Lin
Fang Yu
Jie-Hong R. Jiang


title: BFS-Based Model Checking of Linear-Time Properties with an Application on GPUs


title: A Practical Verification Framework for Preemptive OS Kernels

authors:
Fengwei Xu
Ming Fu
Xinyu Feng
Xiaoran Zhang
Hui Zhang
Zhaohui Li


title: Under-Approximating Backward Reachable Sets by Polytopes

authors:
Bai Xue
Zhikun She
Arvind Easwaran


title: Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants

authors:
Alessandro Abate
Iury Bessa
Dario Cattaruzza
Lucas C. Cordeiro
Cristina David
Pascal Kesseli
Daniel Kroening
Elizabeth Polgreen

abstract: We present a sound and automated approach to synthesize safe digital feedback controllers for physical plants represented as linear, time-invariant models. Models are given as dynamical equations with inputs, evolving over a continuous state space and accounting for errors due to the digitization of signals by the controller. Our counterexample guided inductive synthesis (CEGIS) approach has two phases: We synthesize a static feedback controller that stabilizes the system but that may not be safe for all initial conditions. Safety is then verified either via BMC or abstract acceleration; if the verification step fails, a counterexample is provided to the synthesis engine and the process iterates until a safe controller is obtained. We demonstrate the practical value of this approach by automatically synthesizing safe controllers for intricate physical plant models from the digital control literature.


title: Classification and Coverage-Based Falsification for Embedded Control Systems

authors:
Arvind Adimoolam
Thao Dang
Alexandre Donzé
James Kapinski
Xiaoqing Jin


title: Repairing Decision-Making Programs Under Uncertainty

authors:
Aws Albarghouthi
Loris D'Antoni
Samuel Drews


title: Context-Sensitive Dynamic Partial Order Reduction

authors:
Elvira Albert
Puri Arenas
Maria Garcia de la Banda
Miguel Gómez-Zamalloa
Peter J. Stuckey


title: Quantitative Assume Guarantee Synthesis

authors:
Shaull Almagor
Orna Kupferman
Jan Oliver Ringert
Yaron Velner

abstract: In assume-guarantee synthesis, we are given a specification \(\langle A,G \rangle \), describing an assumption on the environment and a guarantee for the system, and we construct a system that interacts with an environment and is guaranteed to satisfy G whenever the environment satisfies A. While assume-guarantee synthesis is 2EXPTIME-complete for specifications in LTL, researchers have identified the \(\text {GR(1)}\) fragment of LTL, which supports assume-guarantee reasoning and for which synthesis has an efficient symbolic solution. In recent years we see a transition to quantitative synthesis, in which the specification formalism is multi-valued and the goal is to generate high-quality systems, namely ones that maximize the satisfaction value of the specification.


title: GPUDrano: Detecting Uncoalesced Accesses in GPU Programs

authors:
Rajeev Alur
Joseph Devietti
Omar S. Navarro Leija
Nimit Singhania


title: Verified Compilation of Space-Efficient Reversible Circuits

authors:
Matthew Amy
Martin Roetteler
Krysta M. Svore

abstract: The generation of reversible circuits from high-level code is an important problem in several application domains, including low-power electronics and quantum computing. Existing tools compile and optimize reversible circuits for various metrics, such as the overall circuit size or the total amount of space required to implement a given function reversibly. However, little effort has been spent on verifying the correctness of the results, an issue of particular importance in quantum computing. There, compilation allows not only mapping to hardware, but also the estimation of resources required to implement a given quantum algorithm, a process that is crucial for identifying which algorithms will outperform their classical counterparts. We present a reversible circuit compiler called ReVerC, which has been formally verified in F* and compiles circuits that operate correctly with respect to the input program. Our compiler compiles the Revs language to combinational reversible circuits with as few ancillary bits as possible, and provably cleans temporary values.


title: Value Iteration for Long-Run Average Reward in Markov Decision Processes

authors:
Pranav Ashok
Krishnendu Chatterjee
Przemyslaw Daca
Jan Kretínský
Tobias Meggendorfer

abstract: Markov decision processes (MDPs) are standard models for probabilistic systems with non-deterministic behaviours. Long-run average rewards provide a mathematically elegant formalism for expressing long term performance. Value iteration (VI) is one of the simplest and most efficient algorithmic approaches to MDPs with other properties, such as reachability objectives. Unfortunately, a naive extension of VI does not work for MDPs with long-run average rewards, as there is no known stopping criterion. In this work our contributions are threefold. (1) We refute a conjecture related to stopping criteria for MDPs with long-run average rewards. (2) We present two practical algorithms for MDPs with long-run average rewards based on VI. First, we show that a combination of applying VI locally for each maximal end-component (MEC) and VI for reachability objectives can provide approximation guarantees. Second, extending the above approach with a simulation-guided on-demand variant of VI, we present an anytime algorithm that is able to deal with very large models. (3) Finally, we present experimental results showing that our methods significantly outperform the standard approaches on several benchmarks.


title: Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes

authors:
Christel Baier
Joachim Klein
Linda Leuschner
David Parker
Sascha Wunderlich


title: Simulation-Equivalent Reachability of Large Linear Systems with Inputs

authors:
Stanley Bak
Parasara Sridhar Duggirala


title: Runtime Verification of Temporal Properties over Out-of-Order Data Streams

authors:
David A. Basin
Felix Klaedtke
Eugen Zalinescu

abstract: We present a monitoring approach for verifying systems at runtime. Our approach targets systems whose components communicate with the monitors over unreliable channels, where messages can be delayed or lost. In contrast to prior works, whose property specification languages are limited to propositional temporal logics, our approach handles an extension of the real-time logic MTL with freeze quantifiers for reasoning about data values. We present its underlying theory based on a new three-valued semantics that is well suited to soundly and completely reason online about event streams in the presence of message delay or loss. We also evaluate our approach experimentally. Our prototype implementation processes hundreds of events per second in settings where messages are received out of order.


title: Towards Verifying Nonlinear Integer Arithmetic

authors:
Paul Beame
Vincent Liew

abstract: We eliminate a key roadblock to efficient verification of nonlinear integer arithmetic using CDCL SAT solvers, by showing how to construct short resolution proofs for many properties of the most widely used multiplier circuits. Such short proofs were conjectured not to exist. More precisely, we give \(n^{O(1)}\) size regular resolution proofs for arbitrary degree 2 identities on array, diagonal, and Booth multipliers and \(n^{O(\log n)}\) size proofs for these identities on Wallace tree multipliers.


title: On Multiphase-Linear Ranking Functions

authors:
Amir M. Ben-Amram
Samir Genaim

abstract: Multiphase ranking functions (\( M\varPhi \)RFs) were proposed as a means to prove the termination of a loop in which the computation progresses through a number of “phases”, and the progress of each phase is described by a different linear ranking function. Our work provides new insights regarding such functions for loops described by a conjunction of linear constraints (single-path loops). We provide a complete polynomial-time solution to the problem of existence and of synthesis of \( M\varPhi \)RF of bounded depth (number of phases), when variables range over rational or real numbers; a complete solution for the (harder) case that variables are integer, with a matching lower-bound proof, showing that the problem is coNP-complete; and a new theorem which bounds the number of iterations for loops with \( M\varPhi \)RFs. Surprisingly, the bound is linear, even when the variables involved change in non-linear way. We also consider a type of lexicographic ranking functions more expressive than types of lexicographic functions for which complete solutions have been given so far. We prove that for the above type of loops, lexicographic functions can be reduced to \( M\varPhi \)RFs, and thus the questions of complexity of detection, synthesis, and iteration bounds are also answered for this class.


title: Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-affine Dynamical Systems

authors:
Nikola Benes
Lubos Brim
Martin Demko
Samuel Pastva
David Safránek


title: Learning a Static Analyzer from Data

authors:
Pavol Bielik
Veselin Raychev
Martin T. Vechev

abstract: To be practically useful, modern static analyzers must precisely model the effect of both, statements in the programming language as well as frameworks used by the program under analysis. While important, manually addressing these challenges is difficult for at least two reasons: (i) the effects on the overall analysis can be non-trivial, and (ii) as the size and complexity of modern libraries increase, so is the number of cases the analysis must handle.


title: Proving Linearizability Using Forward Simulations

authors:
Ahmed Bouajjani
Michael Emmi
Constantin Enea
Suha Orhun Mutluergil

abstract: Linearizability is the standard correctness criterion for concurrent data structures such as stacks and queues. It allows to establish observational refinement between a concurrent implementation and an atomic reference implementation. Proving linearizability requires identifying linearization points for each method invocation along all possible computations, leading to valid sequential executions, or alternatively, establishing forward and backward simulations. In both cases, carrying out proofs is hard and complex in general. In particular, backward reasoning is difficult in the context of programs with data structures, and strategies for identifying statically linearization points cannot be defined for all existing implementations. In this paper, we show that, contrary to common belief, many such complex implementations, including, e.g., the Herlihy and Wing Queue and the Time-Stamped Stack, can be proved correct using only forward simulation arguments. This leads to simple and natural correctness proofs for these implementations that are amenable to automation.


title: MightyL: A Compositional Translation from MITL to Timed Automata

authors:
Thomas Brihaye
Gilles Geeraerts
Hsi-Ming Ho
Benjamin Monmege


title: Automated Resource Analysis with Coq Proof Objects

authors:
Quentin Carbonneaux
Jan Hoffmann
Thomas W. Reps
Zhong Shao


title: Syntax-Guided Optimal Synthesis for Chemical Reaction Networks

authors:
Luca Cardelli
Milan Ceska
Martin Fränzle
Marta Z. Kwiatkowska
Luca Laurenti
Nicola Paoletti
Max Whitby


title: Data-Driven Synthesis of Full Probabilistic Programs

authors:
Sarah E. Chasins
Phitchaya Mangpo Phothilimthana


title: Non-polynomial Worst-Case Analysis of Recursive Programs

authors:
Krishnendu Chatterjee
Hongfei Fu
Amir Kafshdar Goharshady

abstract: We study the problem of developing efficient approaches for proving worst-case bounds of non-deterministic recursive programs. Ranking functions are sound and complete for proving termination and worst-case bounds of non-recursive programs. First, we apply ranking functions to recursion, resulting in measure functions. We show that measure functions provide a sound and complete approach to prove worst-case bounds of non-deterministic recursive programs. Our second contribution is the synthesis of measure functions in non-polynomial forms. We show that non-polynomial measure functions with logarithm and exponentiation can be synthesized through abstraction of logarithmic or exponentiation terms, Farkas Lemma, and Handelman’s Theorem using linear programming. While previous methods obtain polynomial worst-case bounds, our approach can synthesize bounds of various forms including O( n log n ) and O( n r ), where r is not an integer. We present experimental results to demonstrate that our approach can efficiently obtain worst-case bounds of classical recursive algorithms such as (i) Merge sort, Heap sort, and the divide-and-conquer algorithm for the Closest Pair problem, where we obtain O( n log n ) worst-case bound, and (ii) Karatsuba’s algorithm for polynomial multiplication and Strassen’s algorithm for matrix multiplication, for which we obtain O( n r ) bounds such that r is not an integer and is close to the best-known bound for the respective algorithm. Besides the ability to synthesize non-polynomial bounds, we also show that our approach is equally capable of obtaining polynomial worst-case bounds for classical programs such as Quick sort and the dynamic programming algorithm for computing Fibonacci numbers.


title: Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds

authors:
Krishnendu Chatterjee
Hongfei Fu
Aniket Murhekar

abstract: We consider the problem of developing automated techniques for solving recurrence relations to aid the expected-runtime analysis of programs. Several classical textbook algorithms have quite efficient expected-runtime complexity, whereas the corresponding worst-case bounds are either inefficient (e.g., QUICK-SORT), or completely ineffective (e.g., COUPON-COLLECTOR). Since the main focus of expected-runtime analysis is to obtain efficient bounds, we consider bounds that are either logarithmic, linear, or almost-linear ($\mathcal{O}(\log n)$, $\mathcal{O}(n)$, $\mathcal{O}(n\cdot\log n)$, respectively, where n represents the input size). Our main contribution is an efficient (simple linear-time algorithm) sound approach for deriving such expected-runtime bounds for the analysis of recurrence relations induced by randomized algorithms. Our approach can infer the asymptotically optimal expected-runtime bounds for recurrences of classical randomized algorithms, including RANDOMIZED-SEARCH, QUICK-SORT, QUICK-SELECT, COUPONCOLLECTOR, where the worst-case bounds are either inefficient (such as linear as compared to logarithmic of expected-runtime, or quadratic as compared to linear or almost-linear of expected-runtime), or ineffective. We have implemented our approach, and the experimental results show that we obtain the bounds efficiently for the recurrences of various classical algorithms.


title: A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT

authors:
Sylvain Conchon
Mohamed Iguernelala
Kailiang Ji
Guillaume Melquiond
Clément Fumex


title: Lagrangian Reachabililty

authors:
Jacek Cyranka
Md. Ariful Islam
Greg Byrne
Paul L. Jones
Scott A. Smolka
Radu Grosu

abstract: We introduce LRT, a new Lagrangian-based ReachTube computation algorithm that conservatively approximates the set of reachable states of a nonlinear dynamical system. LRT makes use of the Cauchy-Green stretching factor (SF), which is derived from an over-approximation of the gradient of the solution flows. The SF measures the discrepancy between two states propagated by the system solution from two initial states lying in a well-defined region, thereby allowing LRT to compute a reachtube with a ball-overestimate in a metric where the computed enclosure is as tight as possible. To evaluate its performance, we implemented a prototype of LRT in C++/Matlab, and ran it on a set of well-established benchmarks. Our results show that LRT compares very favorably with respect to the CAPD and Flow* tools.


title: The Power of Symbolic Automata and Transducers

authors:
Loris D'Antoni
Margus Veanes


title: Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts

authors:
Andrei Marian Dan
Manu Sridharan
Satish Chandra
Jean-Baptiste Jeannin
Martin T. Vechev


title: A Storm is Coming: A Modern Probabilistic Model Checker

authors:
Christian Dehnert
Sebastian Junges
Joost-Pieter Katoen
Matthias Volk

abstract: We launch the new probabilistic model checker Storm. It features the analysis of discrete- and continuous-time variants of both Markov chains and MDPs. It supports the Prism and JANI modeling languages, probabilistic programs, dynamic fault trees and generalized stochastic Petri nets. It has a modular set-up in which solvers and symbolic engines can easily be exchanged. It offers a Python API for rapid prototyping by encapsulating Storm’s fast and scalable algorithms. Experiments on a variety of benchmarks show its competitive performance.


title: Synthesis with Abstract Examples

authors:
Dana Drachsler-Cohen
Sharon Shoham
Eran Yahav


title: SMTCoq: A Plug-In for Integrating SMT Solvers into Coq

authors:
Burak Ekici
Alain Mebsout
Cesare Tinelli
Chantal Keller
Guy Katz
Andrew Reynolds
Clark W. Barrett


title: Network-Wide Configuration Synthesis

authors:
Ahmed El-Hassany
Petar Tsankov
Laurent Vanbever
Martin T. Vechev

abstract: Computer networks are hard to manage. Given a set of high-level requirements (e.g., reachability, security), operators have to manually figure out the individual configuration of potentially hundreds of devices running complex distributed protocols so that they, collectively, compute a compatible forwarding state. Not surprisingly, operators often make mistakes which lead to downtimes.


title: DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems

authors:
Chuchu Fan
Bolun Qi
Sayan Mitra
Mahesh Viswanathan

abstract: We present the DryVR framework for verifying hybrid control systems that are described by a combination of a black-box simulator for trajectories and a white-box transition graph specifying mode switches. The framework includes (a) a probabilistic algorithm for learning sensitivity of the continuous trajectories from simulation data, (b) a bounded reachability analysis algorithm that uses the learned sensitivity, and (c) reasoning techniques based on simulation relations and sequential composition, that enable verification of complex systems under long switching sequences, from the reachability analysis of a simpler system under shorter sequences. We demonstrate the utility of the framework by verifying a suite of automotive benchmarks that include powertrain control, automatic transmission, and several autonomous and ADAS features like automatic emergency braking, lane-merge, and auto-passing controllers.


title: BoSy: An Experimentation Framework for Bounded Synthesis

authors:
Peter Faymonville
Bernd Finkbeiner
Leander Tentrup

abstract: We present \(\textsf {BoSy}\), a reactive synthesis tool based on the bounded synthesis approach. Bounded synthesis ensures the minimality of the synthesized implementation by incrementally increasing a bound on the size of the solutions it considers. For each bound, the existence of a solution is encoded as a logical constraint solving problem that is solved by an appropriate solver. \(\textsf {BoSy}\) constructs bounded synthesis encodings into SAT, QBF, DQBF, EPR, and SMT, and interfaces to solvers of the corresponding type. When supported by the solver, \(\textsf {BoSy}\) extracts solutions as circuits, which can, if desired, be verified with standard hardware model checkers. \(\textsf {BoSy}\) won the LTL synthesis track at SYNTCOMP 2016. In addition to its use as a synthesis tool, \(\textsf {BoSy}\) can also be used as an experimentation and performance evaluation framework for various types of satisfiability solvers.


title: Efficient Parallel Strategy Improvement for Parity Games

abstract: We study strategy improvement algorithms for solving parity games. While these algorithms are known to solve parity games using a very small number of iterations, experimental studies have found that a high step complexity causes them to perform poorly in practice. In this paper we seek to address this situation. Every iteration of the algorithm must compute a best response, and while the standard way of doing this uses the Bellman-Ford algorithm, we give experimental results that show that one-player strategy improvement significantly outperforms this technique in practice. We then study the best way to implement one-player strategy improvement, and we develop an efficient parallel algorithm for carrying out this task, by reducing the problem to computing prefix sums on a linked list. We report experimental results for these algorithms, and we find that a GPU implementation of this algorithm shows a significant speedup over single-core and multi-core CPU implementations.


title: EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties

authors:
Bernd Finkbeiner
Christopher Hahn
Marvin Stenger


title: Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems

authors:
Marie Fortin
Anca Muscholl
Igor Walukiewicz


title: Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis

authors:
Adrià Gascón
Ashish Tiwari
Brent Carmer
Umang Mathur


title: Verifying Equivalence of Spark Programs

authors:
Shelly Grossman
Sara Cohen
Shachar Itzhaky
Noam Rinetzky
Mooly Sagiv