title: Generic Combination of Heap and Value Analyses in Abstract Interpretation


venue: vmcai

title: Modularly Combining Numeric Abstract Domains with Points-to Analysis, and a Scalable Static Numeric Analyzer for Java


title: Timing Analysis of Parallel Software Using Abstract Execution

authors:
Andreas Gustavsson
Jan Gustafsson
Björn Lisper


title: Widening for Control-Flow

authors:
Ben Hardekopf
Ben Wiedermann
Berkeley R. Churchill
Vineeth Kashyap


title: Message-Passing Algorithms for the Verification of Distributed Protocols

authors:
Loïg Jezequel
Javier Esparza


title: Probabilistic Automata for Safety LTL Specifications

authors:
Dileep Kini
Mahesh Viswanathan


title: Synthesis for Polynomial Lasso Programs

authors:
Jan Leike
Ashish Tiwari

abstract: We present a method for the synthesis of polynomial lasso programs. These programs consist of a program stem, a set of transitions, and an exit condition, all in the form of algebraic assertions conjunctions of polynomial equalities. Central to this approach is the discovery of non-linear algebraic loop invariants. We extend Sankaranarayanan, Sipma, and Manna's template-based approach and prove a completeness criterion. We perform program synthesis by generating a constraint whose solution is a synthesized program together with a loop invariant that proves the program's correctness. This constraint is non-linear and is passed to an SMT solver. Moreover, we can enforce the termination of the synthesized program with the support of test cases.


title: Weakest Precondition Synthesis for Compiler Optimizations

authors:
Nuno P. Lopes
José Monteiro


title: Policy Iteration-Based Conditional Termination and Ranking Functions


title: Relational Thread-Modular Static Value Analysis by Abstract Interpretation


title: Practical Floating-Point Tests with Integer Code


title: Precise Analysis of Value-Dependent Synchronization in Priority Scheduled Programs

authors:
Martin D. Schwarz
Helmut Seidl
Vesal Vojdani
Kalmer Apinis


title: Modular Synthesis of Sketches Using Models

authors:
Rohit Singh
Rishabh Singh
Zhilei Xu
Rebecca Krosnick
Armando Solar-Lezama

abstract:
One problem with the constraint-based approaches to synthesis that have become popular over the last few years is that they only scale to relatively small routines, on the order of a few dozen lines of code. This paper presents a mechanism for modular reasoning that allows us to break larger synthesis problems into small manageable pieces. The approach builds on previous work in the verification community of using high-level specifications and partially interpreted functions we call them models in place of more complex pieces of code in order to make the analysis modular.

The main contribution of this paper is to show how to combine these techniques with the counterexample guided synthesis approaches used to efficiently solve synthesis problems. Specifically, we show two new algorithms; one to efficiently synthesize functions that use models, and another one to synthesize functions while ensuring that the behavior of the resulting function will be in the set of behaviors allowed by the model. We have implemented our approach on top of the open-source Sketch synthesis system, and we demonstrate its effectiveness on several Sketch benchmark problems.


title: Bisimulations and Logical Characterizations on Continuous-Time Markov Decision Processes

authors:
Lei Song
Lijun Zhang
Jens Chr. Godskesen

abstract: In this paper we study strong and weak bisimulation equivalences for continuous-time Markov decision processes CTMDPs and the logical characterizations of these relations with respect to the continuous-time stochastic logic CSL. For strong bisimulation, it is well known that it is strictly finer than the CSL equivalence. In this paper we propose strong and weak bisimulations for CTMDPs and show that for a subclass of CTMDPs, strong and weak bisimulations are both sound and complete with respect to the equivalences induced by CSL and the sub-logic of CSL without next operator respectively. We then consider a standard extension of CSL, and show that it and its sub-logic without X can be fully characterized by strong and weak bisimulations respectively over arbitrary CTMDPs.


title: Cascade 2.0

authors:
Wei Wang
Clark W. Barrett
Thomas Wies


title: Precisely Deciding Control State Reachability in Concurrent Traces with Limited Observability

authors:
Chao Wang
Kevin Hoang


title: Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs

authors:
Assalé Adjé
Pierre-Loïc Garoche

abstract:
Among the various critical systems that are worth to be formally analyzed, a wide set consists of controllers for dynamical systems. Those programs typically execute an infinite loop in which simple computations update internal states and produce commands to update the system state. Those systems are yet hardly analyzable by available static analysis method, since, even if performing mainly linear computations, the computation of a safe set of reachable states often requires quadratic invariants.

In this paper we consider the general setting of a piecewise affine program; that is a program performing different affine updates on the system depending on some conditions. This typically encompasses linear controllers with saturations or controllers with different behaviors and performances activated on some safety conditions.

Our analysis is inspired by works performed a decade ago by Johansson et al, and Morari et al, in the control community. We adapted their method focused on the analysis of stability in continuous-time or discretetime settings to fit the static analysis paradigm and the computation of invariants, that is over-approximation of reachable sets using piecewise quadratic Lyapunov functions.


title: Analysis of Infinite-State Graph Transformation Systems by Cluster Abstraction

authors:
Peter Backes
Jan Reineke


title: Property Directed Polyhedral Abstraction

authors:
Nikolaj S. Bjørner
Arie Gurfinkel


title: Abstraction-Based Computation of Reward Measures for Markov Automata

authors:
Bettina Braitling
Luis María Ferrer Fioriti
Hassan Hatefi
Ralf Wimmer
Bernd Becker
Holger Hermanns


title: An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer

authors:
Maria Christakis
Peter Müller
Valentin Wüstholz


title: Proving Memory Safety of the ANI Windows Image Parser Using Compositional Exhaustive Testing

authors:
Maria Christakis
Patrice Godefroid


title: Datacentric Semantics for Verification of Privacy Policy Compliance by Mobile Applications

authors:
Agostino Cortesi
Pietro Ferrara
Marco Pistoia
Omer Tripp


title: Abstracting Induction by Extrapolation and Interpolation


title: Effective Abstractions for Verification under Relaxed Memory Models

authors:
Andrei Marian Dan
Yuri Meshman
Martin T. Vechev
Eran Yahav


title: Automatic Inference of Heap Properties Exploiting Value Domains

authors:
Pietro Ferrara
Peter Müller
Milos Novácek


title: Abstracting and Counting Synchronizing Processes

authors:
Zeinab Ganjei
Ahmed Rezine
Petru Eles
Zebo Peng


title: A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets

authors:
Khalil Ghorbal
Andrew Sogokon
André Platzer


title: From Verification to Optimizations

authors:
Rigel Gjomemo
Kedar S. Namjoshi
Phu H. Phung
V. N. Venkatakrishnan
Lenore D. Zuck


title: Tree Automata-Based Refinement with Application to Horn Clause Verification

authors:
Bishoksan Kafle
John P. Gallagher


title: Abstraction of Arrays Based on Non Contiguous Partitions

authors:
Jiangchao Liu
Xavier Rival


title: Bounded Implementations of Replicated Data Types

authors:
Madhavan Mukund
Ranjal Gautham Shenoy
S. P. Suresh


title: Path Sensitive Cache Analysis Using Cache Miss Paths

authors:
Kartik Nagar
Y. N. Srikant


title: Foundations of Quantitative Predicate Abstraction for Stability Analysis of Hybrid Systems

authors:
Pavithra Prabhakar
Miriam Garcia Soto


title: Variations on the Stochastic Shortest Path Problem

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

abstract: In this invited contribution, we revisit the stochastic shortest path problem, and show how recent results allow one to improve over the classical solutions: we present algorithms to synthesize strategies with multiple guarantees on the distribution of the length of paths reaching a given target, rather than simply minimizing its expected value. The concepts and algorithms that we propose here are applications of more general results that have been obtained recently for Markov decision processes and that are described in a series of recent papers.


title: Induction for SMT Solvers

authors:
Andrew Reynolds
Viktor Kuncak


title: Distributed Markov Chains

authors:
Ratul Saha
Javier Esparza
Sumit Kumar Jha
Madhavan Mukund
P. S. Thiagarajan

abstract:
The formal verification of large probabilistic models is challenging. Exploiting the concurrency that is often present is one way to address this problem. Here we study a class of communicating probabilistic agents in which the synchronizations determine the probability distribution for the next moves of the participating agents. The key property of this class is that the synchronizations are deterministic, in the sense that any two simultaneously enabled synchronizations involve disjoint sets of agents. As a result, such a network of agents can be viewed as a succinct and distributed presentation of a large global Markov chain. A rich class of Markov chains can be represented this way.

We use partial-order notions to define an interleaved semantics that can be used to efficiently verify properties of the global Markov chain represented by the network. To demonstrate this, we develop a statistical model checking SMC procedure and use it to verify two large networks of probabilistic agents.

We also show that our model, called distributed Markov chains DMCs, is closely related to deterministic cyclic negotiations, a recently introduced model for concurrent systems [10]. Exploiting this connection we show that the termination of a DMC that has been endowed with a global final state can be checked in polynomial time.


title: Debugging Process Algebra Specifications

authors:
Gwen Salaün
Lina Ye


title: Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation

authors:
Caterina Urban
Antoine Miné


title: A Model for Industrial Real-Time Systems

authors:
Md Tawhid Bin Waez
Andrzej Wasowski
Juergen Dingel
Karen Rudie


title: Dependent Array Type Inference from Tests

authors:
He Zhu
Aditya V. Nori
Suresh Jagannathan


title: Viper: A Verification Infrastructure for Permission-Based Reasoning

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


title: Tight Cutoffs for Guarded Protocols with Fairness

authors:
Simon Außerlechner
Swen Jacobs
Ayrat Khalimov

abstract: Guarded protocols were introduced in a seminal paper by Emerson and Kahlon 2000, and describe systems of processes whose transitions are enabled or disabled depending on the existence of other processes in certain local states. We study parameterized model checking and synthesis of guarded protocols, both aiming at formal correctness arguments for systems with any number of processes. Cutoff results reduce reasoning about systems with an arbitrary number of processes to systems of a determined, fixed size. Our work stems from the observation that existing cutoff results for guarded protocols i are restricted to closed systems, and ii are of limited use for liveness properties because reductions do not preserve fairness. We close these gaps and obtain new cutoff results for open systems with liveness properties under fairness assumptions. Furthermore, we obtain cutoffs for the detection of global and local deadlocks, which are of paramount importance in synthesis. Finally, we prove tightness or asymptotic tightness for the new cutoffs.


title: Predicate Abstraction for Linked Data Structures

authors:
Alexander Bakst
Ranjit Jhala

abstract: We present Alias Refinement Types Art, a new approach that uses predicate-abstraction to automate the verification of correctness properties of linked data structures. While there are many techniques for checking that a heap-manipulating program adheres to its specification, they often require that the programmer annotate the behavior of each procedure, for example, in the form of loop invariants and pre- and post-conditions. We introduce a technique that lifts predicate abstraction to the heap by factoring the analysis of data structures into two orthogonal components: 1i¾?Alias Types, which reason about the physical shape of heap structures, and 2i¾?Refinement Types, which use simple predicates from an SMT decidable theory to capture the logical or semantic properties of the structures. We evaluate Art by implementing a tool that performs type inference for an imperative language, and empirically show, using a suite of data-structure benchmarks, that Art requires only 21i¾?% of the annotations needed by other state-of-the-art verification techniques.


title: Automatic Generation of Propagation Complete SAT Encodings

authors:
Martin Brain
Liana Hadarean
Daniel Kroening
Ruben Martins


title: Model Checking with Multi-threaded IC3 Portfolios

authors:
Sagar Chaki
Derrick Karimi


title: A General Modular Synthesis Problem for Pushdown Systems

authors:
Ilaria De Crescenzo
Salvatore La Torre


title: Abstraction-driven Concolic Testing

authors:
Przemyslaw Daca
Ashutosh Gupta
Thomas A. Henzinger

abstract: Concolic testing is a promising method for generating test suites for large programs. However, it suffers from the path-explosion problem and often fails to find tests that cover difficult-to-reach parts of programs. In contrast, model checkers based on counterexample-guided abstraction refinement explore programs exhaustively, while failing to scale on large programs with precision. In this paper, we present a novel method that iteratively combines concolic testing and model checking to find a test suite for a given coverage criterion. If concolic testing fails to cover some test goals, then the model checker refines its program abstraction to prove more paths infeasible, which reduces the search space for concolic testing. We have implemented our method on top of the concolic-testing tooli¾?Cresti¾?and the model checkeri¾?CpaChecker. We evaluated our tool on a collection of programs and a category ofi¾?SvCompi¾?benchmarks. In our experiments, we observed an improvement in branch coverage compared toi¾?Crest from $$48\,\%$$ to $$63\,\%$$ in the best case, and from $$66\,\%$$ to $$71\,\%$$ on average.


title: Parameter Synthesis for Parametric Interval Markov Chains

authors:
Benoît Delahaye
Didier Lime
Laure Petrucci


title: A Program Logic for C11 Memory Fences

authors:
Marko Doko
Viktor Vafeiadis


title: From Low-Level Pointers to High-Level Containers

authors:
Kamil Dudka
Lukás Holík
Petr Peringer
Marek Trtík
Tomás Vojnar

abstract: We propose a method that transforms a C program manipulating containers using low-level pointer statements into an equivalent program where the containers are manipulated via calls of standard high-level container operations like push_back or pop_front. The input of our method is a C program annotated by a special form of shape invariants which can be obtained from current automatic shape analysers after a slight modification. The resulting program where the low-level pointer statements are summarized into high-level container operations is more understandable and among other possible benefits better suitable for program analysis. We have implemented our approach and successfully tested it through a number of experiments with list-based containers, including experiments with simplification of program analysis by separating shape analysis from analysing data-related properties.


title: An Abstract Domain of Uninterpreted Functions

authors:
Graeme Gange
Jorge A. Navas
Peter Schachte
Harald Søndergaard
Peter J. Stuckey


title: Lazy Constrained Monotonic Abstraction

authors:
Zeinab Ganjei
Ahmed Rezine
Petru Eles
Zebo Peng


title: Reward-Bounded Reachability Probability for Uncertain Weighted MDPs

authors:
Vahid Hashemi
Holger Hermanns
Lei Song


title: Pointer Race Freedom

authors:
Frédéric Haziza
Lukás Holík
Roland Meyer
Sebastian Wolff

abstract: We propose a novel notion of pointer race for concurrent programs manipulating a shared heap. A pointer race is an access to a memory address which was freed, and it is out of the accessor's control whether or not the cell has been re-allocated. We establish two results. 1 Under the assumption of pointer race freedom, it is sound to verify a program running under explicit memory management as if it was running with garbage collection. 2 Even the requirement of pointer race freedom itself can be verified under the garbage-collected semantics. We then prove analogues of the theorems for a stronger notion of pointer race needed to cope with performance-critical code purposely using racy comparisons and even racy dereferences of pointers. As a practical contribution, we apply our results to optimize a thread-modular analysis under explicit memory management. Our experiments confirm a speed-up of upi¾?to two orders of magnitude.


title: Lipschitz Robustness of Timed I/O Systems

authors:
Thomas A. Henzinger
Jan Otop
Roopsha Samanta

abstract: We present the first study of robustness of systems that are both timed as well as reactive I/O. We study the behavior of such timed I/O systems in the presence of uncertain inputs and formalize their robustness using the analytic notion of Lipschitz continuity: a timed I/O system is K-Lipschitz robust if the perturbation in its output is at most K times the perturbation in its input. We quantify input and output perturbation using similarity functions over timed words such as the timed version of the Manhattan distance and the Skorokhod distance. We consider two models of timed I/O systems -- timed transducers and asynchronous sequential circuits. We show that K-robustness of timed transducers can be decided in polynomial space under certain conditions. For asynchronous sequential circuits, we reduce K-robustness w.r.t. timed Manhattan distances to K-robustness of discrete letter-to-letter transducers and show PSpace-completeness of the problem.


title: Exact Heap Summaries for Symbolic Execution

authors:
Benjamin Hillery
Eric Mercer
Neha Rungta
Suzette Person


title: Cloud-Based Verification of Concurrent Software


title: Program Analysis with Local Policy Iteration

authors:
Egor George Karpenkov
David Monniaux
Philipp Wendler

abstract:
We present local policy iterationi¾?LPI, a new algorithm for deriving numerical invariants that combines the precision of max-policy iteration with the flexibility and scalability of conventional Kleene iterations. It is defined in the Configurable Program Analysis CPA framework, thus allowing inter-analysis communication.

LPI uses adjustable-block encoding in order to traverse loop-free program sections, possibly containing branching, without introducing extra abstraction. Our technique operates over any template linear constraint domain, including the interval and octagon domains; templates can also be derived from the program source.

The implementation is evaluated on a set of benchmarks from the International Competition on Software Verification SV-COMP. It competes favorably with state-of-the-art analyzers.


title: Abstract Interpretation with Infinitesimals - Towards Scalability in Nonstandard Static Analysis

authors:
Kengo Kido
Swarat Chaudhuri
Ichiro Hasuo

abstract: We extend abstract interpretation for the purpose of verifying hybrid systems. Abstraction has been playing an important role in many verification methodologies for hybrid systems, but some special care is needed for abstraction of continuous dynamics defined by ODEs. We apply Cousot and Cousot's framework of abstract interpretation to hybrid systems, almost as it is, by regarding continuous dynamics as an infinite iteration of infinitesimal discrete jumps. This extension follows the recent line of work by Suenaga, Hasuo and Sekine, where deductive verification is extended for hybrid systems by 1 introducing a constant $$\mathtt {dt}$$ for an infinitesimal value; and 2 employing Robinson's nonstandard analysis NSA to define mathematically rigorous semantics. Our theoretical results include soundness and termination via uniform widening operators; and our prototype implementation successfully verifies some benchmark examples.


title: Regular Symmetry Patterns

authors:
Anthony W. Lin
Truong Khanh Nguyen
Philipp Rümmer
Jun Sun


title: Polyhedral Approximation of Multivariate Polynomials Using Handelman's Theorem

authors:
Alexandre Maréchal
Alexis Fouilhé
Tim King
David Monniaux
Michaël Périn


title: Hybrid Analysis for Partial Order Reduction of Programs with Arrays


title: D^3 : Data-Driven Disjunctive Abstraction

authors:
Hila Peleg
Sharon Shoham
Eran Yahav


title: Automating Abstract Interpretation

authors:
Thomas W. Reps
Aditya V. Thakur


title: Property Directed Abstract Interpretation

authors:
Noam Rinetzky
Sharon Shoham


title: A Method for Invariant Generation for Polynomial Continuous Systems

authors:
Andrew Sogokon
Khalil Ghorbal
Paul B. Jackson
André Platzer


title: Partitioned Memory Models for Program Analysis

authors:
Wei Wang
Clark W. Barrett
Thomas Wies


title: Effective Bug Finding in C Programs with Shape and Effect Abstractions

authors:
Iago Abal
Claus Brabrand
Andrzej Wasowski


title: Bringing LTL Model Checking to Biologists

authors:
Zara Ahmed
David Benqué
Sergey Berezin
Anna Caroline E. Dahl
Jasmin Fisher
Benjamin A. Hall
Samin Ishtiaq
Jay Nanavati
Nir Piterman
Maik Riechert
Nikita Skoblov

abstract: The BioModelAnalyzer (BMA) is a web based tool for the development of discrete models of biological systems. Through a graphical user interface, it allows rapid development of complex models of gene and protein interaction networks and stability analysis without requiring users to be proficient computer programmers. Whilst stability is a useful specification for testing many systems, testing temporal specifications in BMA presently requires the user to perform simulations. Here we describe the LTL module, which includes a graphical and natural language interfaces to testing LTL queries. The graphical interface allows for graphical construction of the queries and presents results visually in keeping with the current style of BMA. The Natural language interface complements the graphical interface by allowing a gentler introduction to formal logic and exposing educational resources.


title: Structuring Abstract Interpreters Through State and Value Abstractions

authors:
Sandrine Blazy
David Bühler
Boris Yakobowski


title: Synthesizing Non-Vacuous Systems

authors:
Roderick Bloem
Hana Chockler
Masoud Ebrahimi
Ofer Strichman


title: Static Analysis of Communicating Processes Using Symbolic Transducers

authors:
Vincent Botbol
Emmanuel Chailloux
Tristan Le Gall


title: Reduction of Workflow Nets for Generalised Soundness Verification

authors:
Hadrien Bride
Olga Kouchnarenko
Fabien Peureux


title: Matching Multiplications in Bit-Vector Formulas

authors:
Supratik Chakraborty
Ashutosh Gupta
Rahul Jain

abstract: Bit-vector formulas arising from hardware verification problems often contain word-level arithmetic operations. Empirical evidence shows that state-of-the-art SMT solvers are not very efficient at reasoning about bit-vector formulas with multiplication. This is particularly true when multiplication operators are decomposed and represented in alternative ways in the formula. We present a pre-processing heuristic that identifies certain types of decomposed multipliers, and adds special assertions to the input formula that encode the equivalence of sub-terms and word-level multiplication terms. The pre-processed formulas are then solved using an SMT solver. Our experiments with three SMT solvers show that our heuristic allows several formulas to be solved quickly, while the same formulas time out without the pre-processing step.


title: Detecting Strict Aliasing Violations in the Wild

authors:
Pascal Cuoq
Loïc Runarvot
Alexander Cherepanov


title: Independence Abstractions and Models of Concurrency

authors:
Vijay Victor D'Silva
Daniel Kroening
Marcelo Sousa


title: Complete Abstractions and Subclassical Modal Logics

authors:
Vijay Victor D'Silva
Marcelo Sousa


title: Using Abstract Interpretation to Correct Synchronization Faults

authors:
Pietro Ferrara
Omer Tripp
Peng Liu
Eric Koskinen


title: Property Directed Reachability for Proving Absence of Concurrent Modification Errors

authors:
Asya Frumkin
Yotam M. Y. Feldman
Ondrej Lhoták
Oded Padon
Mooly Sagiv
Sharon Shoham


title: Stabilizing Floating-Point Programs Using Provenance Analysis

authors:
Yijia Gu
Thomas Wahl


title: Dynamic Reductions for Model Checking Concurrent Software

authors:
Henning Günther
Alfons Laarman
Ana Sokolova
Georg Weissenbacher

abstract: Symbolic model checking of parallel programs stands and falls with effective methods of dealing with the explosion of interleavings. We propose a dynamic reduction technique to avoid unnecessary interleavings. By extending Lipton’s original work with a notion of bisimilarity, we accommodate dynamic transactions, and thereby reduce dependence on the accuracy of static analysis, which is a severe bottleneck in other reduction techniques.


title: Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games

authors:
Ernst Moritz Hahn
Sven Schewe
Andrea Turrini
Lijun Zhang

abstract: 2.5 player parity games combine the challenges posed by 2.5 player reachability games and the qualitative analysis of parity games. These two types of problems are best approached with different types of algorithms: strategy improvement algorithms for 2.5 player reachability games and recursive algorithms for the qualitative analysis of parity games. We present a method that - in contrast to existing techniques - tackles both aspects with the best suited approach and works exclusively on the 2.5 player game itself. The resulting technique is powerful enough to handle games with several million states.


title: Counterexample Validation and Interpolation-Based Refinement for Forest Automata

authors:
Lukás Holík
Martin Hruska
Ondrej Lengál
Adam Rogalewicz
Tomás Vojnar


title: Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT

authors:
Jiahong Jiang
Liqian Chen
Xueguang Wu
Ji Wang


title: Solving Nonlinear Integer Arithmetic with MCSAT


title: Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms

authors:
Igor V. Konnov
Josef Widder
Francesco Spegni
Luca Spalazzi


title: Efficient Elimination of Redundancies in Polyhedra by Raytracing

authors:
Alexandre Maréchal
Michaël Périn


title: Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions

authors:
Raphaël Monat
Antoine Miné


title: Detecting All High-Level Dataraces in an RTOS Kernel

authors:
Suvam Mukherjee
Arun Kumar
Deepak D'Souza


title: Reachability for Dynamic Parametric Processes

authors:
Anca Muscholl
Helmut Seidl
Igor Walukiewicz

abstract: In a dynamic parametric process every subprocess may spawn arbitrarily many, identical child processes, that may communicate either over global variables, or over local variables that are shared with their parent. We show that reachability for dynamic parametric processes is decidable under mild assumptions. These assumptions are e.g. met if individual processes are realized by pushdown systems, or even higher-order pushdown systems. We also provide algorithms for subclasses of pushdown dynamic parametric processes, with complexity ranging between NP and DEXPTIME.


title: Conjunctive Abstract Interpretation Using Paramodulation

authors:
Or Ozeri
Oded Padon
Noam Rinetzky
Mooly Sagiv


title: Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic

authors:
Andrew Reynolds
Radu Iosif
Cristina Serban

abstract: Separation Logic (\(\mathsf {SL}\)) is a well-known assertion language used in Hoare-style modular proof systems for programs with dynamically allocated data structures. In this paper we investigate the fragment of first-order \(\mathsf {SL}\) restricted to the Bernays-Schonfinkel-Ramsey quantifier prefix \(\exists ^*\forall ^*\), where the quantified variables range over the set of memory locations. When this set is uninterpreted (has no associated theory) the fragment is PSPACE-complete, which matches the complexity of the quantifier-free fragment [7]. However, \(\mathsf {SL}\) becomes undecidable when the quantifier prefix belongs to \(\exists ^*\forall ^*\exists ^*\) instead, or when the memory locations are interpreted as integers with linear arithmetic constraints, thus setting a sharp boundary for decidability within \(\mathsf {SL}\). We have implemented a decision procedure for the decidable fragment of \(\exists ^*\forall ^*\mathsf {SL}\) as a specialized solver inside a DPLL(T) architecture, within the CVC4 SMT solver. The evaluation of our implementation was carried out using two sets of verification conditions, produced by (i) unfolding inductive predicates, and (ii) a weakest precondition-based verification condition generator. Experimental data shows that automated quantifier instantiation has little overhead, compared to manual model-based instantiation.


title: Finding Relevant Templates via the Principal Component Analysis


title: Sound Bit-Precise Numerical Domains

authors:
Tushar Sharma
Thomas W. Reps


title: IC3 - Flipping the E in ICE

authors:
Yakir Vizel
Arie Gurfinkel
Sharon Shoham
Sharad Malik


title: Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction

authors:
Benjamin Aminof
Sasha Rubin
Ilina Stoilkovska
Josef Widder
Florian Zuleger


title: Gradual Program Verification

authors:
Johannes Bader
Jonathan Aldrich
Éric Tanter

abstract: Both static and dynamic program verification approaches have significant disadvantages when considered in isolation. Inspired by research on gradual typing, we propose gradual verification to seamlessly and flexibly combine static and dynamic verification. Drawing on general principles from abstract interpretation, and in particular on the recent Abstracting Gradual Typing methodology of Garcia et al., we systematically derive a gradual verification system from a static one. This approach yields, by construction, a gradual verification system that is compatible with the original static system, but overcomes its rigidity by resorting to dynamic verification when desired. As with gradual typing, the programmer can control the trade-off between static and dynamic checking by tuning the (im)precision of pre- and postconditions. The formal semantics of the gradual verification system and the proofs of its properties, including the gradual guarantees of Siek et al., have been fully mechanized in the Coq proof assistant.


title: Automatic Verification of RMA Programs via Abstraction Extrapolation

authors:
Cedric Baumann
Andrei Marian Dan
Yuri Meshman
Torsten Hoefler
Martin T. Vechev


title: Scalable Approximation of Quantitative Information Flow in Programs

authors:
Fabrizio Biondi
Michael A. Enescu
Annelie Heuser
Axel Legay
Kuldeep S. Meel
Jean Quilbeuf


title: Code Obfuscation Against Abstract Model Checking Attacks

authors:
Roberto Bruni
Roberto Giacobazzi
Roberta Gori


title: Abstract Code Injection - A Semantic Approach Based on Abstract Non-Interference

authors:
Samuele Buro
Isabella Mastroeni


title: A Framework for Computer-Aided Design of Educational Domain Models

authors:
Eric Butler
Emina Torlak
Zoran Popovic


title: Automatic Verification of Intermittent Systems

authors:
Manjeet Dahiya
Sorav Bansal


title: On abstraction and compositionality for weak-memory linearisability

authors:
Brijesh Dongol
Radha Jagadeesan
James Riely
Alasdair Armstrong


title: From Shapes to Amortized Complexity

authors:
Tomás Fiedor
Lukás Holík
Adam Rogalewicz
Moritz Sinn
Tomás Vojnar
Florian Zuleger


title: Invariant Generation for Multi-Path Loops with Polynomial Assignments

authors:
Andreas Humenberger
Maximilian Jaroschek
Laura Kovács

abstract: Program analysis requires the generation of program properties expressing conditions to hold at intermediate program locations. When it comes to programs with loops, these properties are typically expressed as loop invariants. In this paper we study a class of multi-path program loops with numeric variables, in particular nested loops with conditionals, where assignments to program variables are polynomial expressions over program variables. We call this class of loops extended P-solvable and introduce an algorithm for generating all polynomial invariants of such loops. By an iterative procedure employing Gr\"obner basis computation, our approach computes the polynomial ideal of the polynomial invariants of each program path and combines these ideals sequentially until a fixed point is reached. This fixed point represents the polynomial ideal of all polynomial invariants of the given extended P-solvable loop. We prove termination of our method and show that the maximal number of iterations for reaching the fixed point depends linearly on the number of program variables and the number of inner loops. In particular, for a loop with m program variables and r conditional branches we prove an upper bound of m*r iterations. We implemented our approach in the Aligator software package. Furthermore, we evaluated it on 18 programs with polynomial arithmetic and compared it to existing methods in invariant generation. The results show the efficiency of our approach.


title: Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity

authors:
Swen Jacobs
Mouhammad Sakr

abstract: We study cutoff results for parameterized verification and synthesis of guarded protocols, as introduced by Emerson and Kahlon (2000). Guarded protocols describe systems of processes whose transitions are enabled or disabled depending on the existence of other processes in certain local states. Cutoff results reduce reasoning about systems with an arbitrary number of processes to systems of a determined, fixed size. Our work is based on the observation that existing cutoff results for guarded protocols are often impractical, since they scale linearly in the number of local states of processes in the system. We provide new cutoffs that scale not with the number of local states, but with the number of guards in the system, which is in many cases much smaller. Furthermore, we consider generalizations of the type of guards and of the specifications under consideration, and present results for problems that have not been known to admit cutoffs before.


title: Refinement Types for Ruby

authors:
Milod Kazerounian
Niki Vazou
Austin Bourgerie
Jeffrey S. Foster
Emina Torlak

abstract: Refinement types are a popular way to specify and reason about key program properties. In this paper, we introduce RTR, a new system that adds refinement types to Ruby. RTR is built on top of RDL, a Ruby type checker that provides basic type information for the verification process. RTR works by encoding its verification problems into Rosette, a solver-aided host language. RTR handles mixins through assume-guarantee reasoning and uses just-in-time verification for metaprogramming. We formalize RTR by showing a translation from a core, Ruby-like language with refinement types into Rosette. We apply RTR to check a range of functional correctness properties on six Ruby programs. We find that RTR can successfully verify key methods in these programs, taking only a few minutes to perform verification.


title: Modular Analysis of Executables Using On-Demand Heyting Completion

authors:
Julian Kranz
Axel Simon


title: Learning to Complement Büchi Automata

authors:
Yong Li
Andrea Turrini
Lijun Zhang
Sven Schewe


title: Co-Design and Verification of an Available File System

authors:
Mahsa Najafzadeh
Marc Shapiro
Patrick Eugster


title: Abstraction-Based Interaction Model for Synthesis

authors:
Hila Peleg
Shachar Itzhaky
Sharon Shoham


title: Generating Tests by Example

authors:
Hila Peleg
Dan Rasin
Eran Yahav


title: A Logical System for Modular Information Flow Verification

authors:
Adi Prabawa
Mahmudul Faisal Al Ameen
Benedict Lee
Wei-Ngan Chin


title: On Constructivity of Galois Connections


title: Revisiting MITL to Fix Decision Procedures

authors:
Nima Roohi
Mahesh Viswanathan

abstract: Metric Interval Temporal Logic ( MITL ) is a well studied real-time, temporal logic that has decidable satisfiability and model checking problems. The decision procedures for MITLrely on the automata theoretic approach, where logic formulas are translated into equivalent timed automata. Since timed automata are not closed under complementation, decision procedures for MITLfirst convert a formula into negated normal form before translating to a timed automaton. We show that, unfortunately, these 20-year-old procedures are incorrect, because they rely on an incorrect semantics of the \(\mathcal {R}\) operator. We present the right semantics of \(\mathcal {R}\) and give new, correct decision procedures for MITL. We show that both satisfiability and model checking for MITLare Open image in new window , as was previously claimed. We also identify a fragment of MITLthat we call MITL WIthat is richer than \(\texttt {MITL}_{0,\!\infty }\), for which we show that both satisfiability and model checking are Open image in new window . Many of our results have been formally proved in PVS


title: Selfless Interpolation for Infinite-State Model Checking

authors:
Tanja Schindler
Dejan Jovanovic


title: An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs

authors:
Laura Titolo
Marco A. Feliú
Mariano M. Moscato
César A. Muñoz


title: P^5 : Planner-less Proofs of Probabilistic Parameterized Protocols

authors:
Lenore D. Zuck
Kenneth L. McMillan
Jordan Torf


title: Parametric Timed Broadcast Protocols

authors:
Étienne André
Benoît Delahaye
Paulin Fournier
Didier Lime

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


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

authors:
Étienne André
Laurent Fribourg
Jean-Marc Mota
Romain Soulat

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


title: Static Analysis of Binary Code with Memory Indirections Using Polyhedra

authors:
Clément Ballabriga
Julien Forget
Laure Gonnord
Giuseppe Lipari
Jordy Ruiz


title: Exploiting Pointer Analysis in Memory Models for Deductive Verification

authors:
Quentin Bouillaguet
François Bobot
Mihaela Sighireanu
Boris Yakobowski

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


title: Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis

authors:
Rémy Boutonnet
Nicolas Halbwachs


title: euforia: Complete Software Model Checking with Uninterpreted Functions

authors:
Denis Bueno
Karem A. Sakallah


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

authors:
Normann Decker
Anton Pirogov

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


title: Lazy but Effective Functional Synthesis

authors:
Grigory Fedyukovich
Arie Gurfinkel
Aarti Gupta


title: Syntactic Partial Order Compression for Probabilistic Reachability

authors:
Gereon Fox
Daniel Stan
Holger Hermanns


title: Termination of Nondeterministic Probabilistic Programs

authors:
Hongfei Fu
Krishnendu Chatterjee


title: Demand Control-Flow Analysis

authors:
Kimball Germane
Jay McCarthy
Michael D. Adams
Matthew Might


title: Relatively Complete Pushdown Analysis of Escape Continuations

authors:
Kimball Germane
Matthew Might


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

authors:
Stefan Haar
Juraj Kolcák
Loïc Paulevé

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


title: Minimal Synthesis of String to String Functions from Examples

authors:
Jad Hamza
Viktor Kuncak

abstract:
We study the problem of synthesizing string to string transformations from a set of input/output examples. The transformations we consider are expressed using deterministic finite automata (DFA) that read pairs of letters, one letter from the input and one from the output. The DFA corresponding to these transformations have additional constraints, ensuring that each input string is mapped to exactly one output string.
We suggest that, given a set of input/output examples, the smallest DFA consistent with the examples is a good candidate for the transformation the user was expecting. We therefore study the problem of, given a set of examples, finding a minimal DFA consistent with the examples and satisfying the functionality and totality constraints mentioned above.
We prove that, in general, this problem (the corresponding decision problem) is NP-complete. This is unlike the standard DFA minimization problem which can be solved in polynomial time. We provide several NP-hardness proofs that show the hardness of multiple (independent) variants of the problem.
Finally, we propose an algorithm for finding the minimal DFA consistent with input/output examples, that uses a reduction to SMT solvers. We implemented the algorithm, and used it to evaluate the likelihood that the minimal DFA indeed corresponds to the DFA expected by the user.


title: Solving and Interpolating Constant Arrays Based on Weak Equivalences

authors:
Jochen Hoenicke
Tanja Schindler


title: A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization

authors:
Richard Huybers
Alfons Laarman


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

authors:
Anja F. Karl
Robert Schilling
Roderick Bloem
Stefan Mangard


title: Fast BGP Simulation of Large Datacenters

authors:
Nuno P. Lopes
Andrey Rybalchenko


title: Type-Directed Bounding of Collections in Reactive Programs

authors:
Tianhan Lu
Pavol Cerný
Bor-Yuh Evan Chang
Ashutosh Trivedi

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


title: A Practical Algorithm for Structure Embedding

authors:
Charlie Murphy
Zachary Kincaid


title: Automatic Program Repair Using Formal Verification and Expression Templates

authors:
Thanh-Toan Nguyen
Quang-Trung Ta
Wei-Ngan Chin


title: Effect-Driven Flow Analysis

authors:
Jens Nicolay
Quentin Stiévenart
Wolfgang De Meuter
Coen De Roover


title: Mechanically Proving Determinacy of Hierarchical Block Diagram Translations

authors:
Viorel Preoteasa
Iulia Dragomir
Stavros Tripakis


title: A Decidable Logic for Tree Data-Structures with Measurements

authors:
Xiaokang Qiu
Yanjun Wang


title: On the Semantics of Snapshot Isolation

authors:
Azalea Raad
Ori Lahav
Viktor Vafeiadis

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


title: Program Synthesis with Equivalence Reduction

authors:
Calvin Smith
Aws Albarghouthi


title: Application of Abstract Interpretation to the Automotive Electronic Control System

authors:
Tomoya Yamaguchi
Martin Brain
Chirs Ryder
Yosikazu Imai
Yoshiumi Kawamura


title: A Cooperative Parallelization Approach for Property-Directed k-Induction

authors:
Martin Blicha
Antti E. J. Hyvärinen
Matteo Marescotti
Natasha Sharygina


title: Formalizing and Checking Multilevel Consistency

authors:
Ahmed Bouajjani
Constantin Enea
Madhavan Mukund
Ranjal Gautham Shenoy
S. P. Suresh


title: Sharing Ghost Variables in a Collection of Abstract Domains

authors:
Marc Chevalier
Jérôme Feret


title: The Correctness of a Code Generator for a Functional Language

authors:
Nathanaël Courant
Antoine Séré
Natarajan Shankar


title: Language Inclusion for Finite Prime Event Structures

authors:
Andreas Fellner
Thorsten Tarrach
Georg Weissenbacher

abstract: We study the problem of language inclusion between finite, labeled prime event structures. Prime event structures are a formalism to compactly represent concurrent behavior of discrete systems. A labeled prime event structure induces a language of sequences of labels produced by the represented system. We study the problem of deciding inclusion and membership for languages encoded by finite prime event structures and provide complexity results for both problems. We provide a family of examples where prime event structures are exponentially more succinct than formalisms that do not take concurrency into account. We provide a decision algorithm for language inclusion that exploits this succinctness. Furthermore, we provide an implementation of the algorithm and an evaluation on a series of benchmarks. Finally, we demonstrate how our results can be applied to mutation-based test case generation.


title: BackFlow: Backward Context-Sensitive Flow Reconstruction of Taint Analysis Results

authors:
Pietro Ferrara
Luca Olivieri
Fausto Spoto


title: Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification

authors:
Jack J. Garzella
Marek S. Baranowski
Shaobo He
Zvonimir Rakamaric


title: Cheap CTL Compassion in NuSMV

authors:
Daniel Hausmann
Tadeusz Litak
Christoph Rauch
Matthias Zinner


title: Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation

authors:
Oren Ish-Shalom
Shachar Itzhaky
Roman Manevich
Noam Rinetzky


title: Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction

authors:
Oren Ish-Shalom
Shachar Itzhaky
Noam Rinetzky
Sharon Shoham

abstract: Automatic verification of array manipulating programs is a challenging problem because it often amounts to the inference of inductive quantified loop invariants which, in some cases, may not even be first-order expressible. In this paper, we suggest a novel verification technique that is based on induction on user-defined rank of program states as an alternative to loop-invariants. Our technique, dubbed inductive rank reduction, works in two steps. Firstly, we simplify the verification problem and prove that the program is correct when the input state contains an input array of length \(\ell _\textsf {B}\) or less, using the length of the array as the rank of the state. Secondly, we employ a squeezing function \(\curlyvee \) which converts a program state \(\sigma \) with an array of length \(\ell > \ell _\textsf {B}\) to a state Open image in new window containing an array of length \(\ell -1\) or less. We prove that when \(\curlyvee \) satisfies certain natural conditions then if the program violates its specification on \(\sigma \) then it does so also on Open image in new window. The correctness of the program on inputs with arrays of arbitrary lengths follows by induction.


title: Promptness and Bounded Fairness in Concurrent and Parameterized Systems

authors:
Swen Jacobs
Mouhammad Sakr
Martin Zimmermann

abstract: We investigate the satisfaction of specifications in Prompt Linear Temporal Logic (Prompt-LTL) by concurrent systems. Prompt-LTL is an extension of LTL that allows to specify parametric bounds on the satisfaction of eventualities, thus adding a quantitative aspect to the specification language. We establish a connection between bounded fairness, bounded stutter equivalence, and the satisfaction of Prompt-LTL\X formulas. Based on this connection, we prove the first cutoff results for different classes of systems with a parametric number of components and quantitative specifications, thereby identifying previously unknown decidable fragments of the parameterized model checking problem.


title: A Systematic Approach to Abstract Interpretation of Program Transformations

authors:
Sven Keidel
Sebastian Erdweg


title: Improving Parity Game Solvers with Justifications

authors:
Ruben Lapauw
Maurice Bruynooghe
Marc Denecker


title: Solving $\mathrm {LIA} ^\star $ Using Approximations

authors:
Maxwell Levatich
Nikolaj S. Bjørner
Ruzica Piskac
Sharon Shoham


title: Systematic Classification of Attackers via Bounded Model Checking

authors:
Eric Rothstein Morris
Jun Sun
Sudipta Chattopadhyay

abstract: In this work, we study the problem of verification of systems in the presence of attackers using bounded model checking. Given a system and a set of security requirements, we present a methodology to generate and classify attackers, mapping them to the set of requirements that they can break. A naive approach suffers from the same shortcomings of any large model checking problem, i.e., memory shortage and exponential time. To cope with these shortcomings, we describe two sound heuristics based on cone-of-influence reduction and on learning, which we demonstrate empirically by applying our methodology to a set of hardware benchmark systems.


title: Witnessing Secure Compilation

authors:
Kedar S. Namjoshi
Lucas M. Tabajara

abstract: Compiler optimizations are designed to improve run-time performance while preserving input-output behavior. Correctness in this sense does not necessarily preserve security: it is known that standard optimizations may break or weaken security properties that hold of the source program. This work develops a translation validation method for secure compilation. Security (hyper-)properties are expressed using automata operating over a bundle of program traces. A flexible, automaton-based refinement scheme, generalizing existing refinement methods, guarantees that the associated security property is preserved by a program transformation. In practice, the refinement relations ("security witnesses") can be generated during compilation and validated independently with a refinement checker. This process is illustrated for common optimizations. Crucially, it is not necessary to verify the compiler implementation itself, which is infeasible in practice for production compilers.


title: Practical Abstractions for Automated Verification of Shared-Memory Concurrency

authors:
Wytse Oortwijn
Dilian Gurov
Marieke Huisman


title: Fixing Code that Explodes Under Symbolic Evaluation

authors:
Sorawee Porncharoenwase
James Bornholt
Emina Torlak


title: How to Win First-Order Safety Games

authors:
Helmut Seidl
Christian Müller
Bernd Finkbeiner

abstract:
First-order (FO) transition systems have recently attracted attention for the verification of parametric systems such as network protocols, software-defined networks or multi-agent workflows like conference management systems. Functional correctness or noninterference of these systems have conveniently been formulated as safety properties. In order to automatically synthesize predicates to enforce safety or noninterference, we generalize FO transition systems to FO safety games. For the important case of FO games with monadic predicates only, we provide a complete classification into decidable and undecidable cases.
For games with non-monadic predicates, we concentrate on universal first-order invariants, since these are sufficient to express a large class of noninterference properties. Based on general techniques for second-order quantifier elimination, we provide abstraction and refinement techniques to synthesize FO-expressible strategies that enforce safety.
We demonstrate the usefulness of our approach by automatically inferring nontrivial FO specifications for message passing in a leader election protocol as well as for a conference management system to exclude unappreciated disclosure of reports.


title: Generalized Property-Directed Reachability for Hybrid Systems

authors:
Kohei Suenaga
Takuya Ishizawa

abstract: Generalized property-directed reachability (GPDR) belongs to the family of the model-checking techniques called IC3/PDR. It has been successfully applied to software verification; for example, it is the core of Spacer, a state-of-the-art Horn-clause solver bundled with Z3. However, it has yet to be applied to hybrid systems, which involve a continuous evolution of values over time. As the first step towards GPDR- based model checking for hybrid systems, this paper formalizes HGPDR, an adaptation of GPDR to hybrid systems, and proves its soundness. We also implemented a semi-automated proof-of-concept verifier, which allows a user to provide hints to guide verification steps.


title: Synthesizing Environment Invariants for Modular Hardware Verification

authors:
Hongce Zhang
Weikun Yang
Grigory Fedyukovich
Aarti Gupta
Sharad Malik


title: Formal Semantics and Verification of Network-Based Biocomputation Circuits

authors:
Michelle Aluf-Medina
Till Korten
Avraham Raviv
Dan V. Nicolau Jr.
Hillel Kugler

abstract: Abstract Network-Based Biocomputation Circuits (NBCs) offer a new paradigm for solving complex computational problems by utilizing biological agents that operate in parallel to explore manufactured planar devices. The approach can also have future applications in diagnostics and medicine by combining NBCs computational power with the ability to interface with biological material. To realize this potential, devices should be designed in a way that ensures their correctness and robust operation. For this purpose, formal methods and tools can offer significant advantages by allowing investigation of design limitations and detection of errors before manufacturing and experimentation. Here we define a computational model for NBCs by providing formal semantics to NBC circuits. We present a formal verification-based approach and prototype tool that can assist in the design of NBCs by enabling verification of a given design’s correctness. Our tool allows verification of the correctness of NBC designs for several NP-Complete problems, including the Subset Sum, Exact Cover and Satisfiability problems and can be extended to other NBC implementations. Our approach is based on defining transition systems for NBCs and using temporal logic for specifying and proving properties of the design using model checking. Our formal model can also serve as a starting point for computational complexity studies of the power and limitations of NBC systems.


title: A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries

authors:
Nathalie Bertrand
Marijana Lazic
Josef Widder


title: Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories

authors:
Martin Bromberger
Alberto Fiori
Christoph Weidenbach


title: Proving the Existence of Fair Paths in Infinite-State Systems

authors:
Alessandro Cimatti
Alberto Griggio
Enrico Magnago


title: Verification of Concurrent Programs Using Petri Net Unfoldings

authors:
Daniel Dietsch
Matthias Heizmann
Dominik Klumpp
Mehdi Naouar
Andreas Podelski
Claus Schätzle


title: Model Checking Algorithms for Hyperproperties (Invited Paper)

abstract: Hyperproperties generalize trace properties by expressing relations between multiple computations. Hyperpropertes include policies from information-flow security, like observational determinism or non-interference, and many other system properties including promptness and knowledge. In this paper, we give an overview on the model checking problem for temporal hyperlogics. Our starting point is the model checking algorithm for HyperLTL, a reduction to B\"uchi automata emptiness. This basic construction can be extended with propositional quantification, resulting in an algorithm for HyperQPTL. It can also be extended with branching time, resulting in an algorithm for HyperCTL*. However, it is not possible to have both extensions at the same time: the model checking problem of HyperQCTL* is undecidable. An attractive compromise is offered by MPL[E], i.e., monadic path logic extended with the equal-level predicate. The expressiveness of MPL[E] falls strictly between that of HyperCTL* and HyperQCTL*. MPL[E] subsumes both HyperCTL* and HyperKCTL*, the extension of HyperCTL* with the knowledge operator. We show that the model checking problem for MPL[E] is still decidable.


title: Compositional Model Checking for Multi-properties

authors:
Ohad Goudsmid
Orna Grumberg
Sarai Sheinvald


title: Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching

authors:
Jochen Hoenicke
Tanja Schindler


title: Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper)

authors:
Andreas Humenberger
Laura Kovács

abstract: Provably correct software is one of the key challenges in our softwaredriven society. While formal verification establishes the correctness of a given program, the result of program synthesis is a program which is correct by construction. In this paper we overview some of our results for both of these scenarios when analysing programs with loops. The class of loops we consider can be modelled by a system of linear recurrence equations with constant coefficients, called C-finite recurrences. We first describe an algorithmic approach for synthesising all polynomial equality invariants of such non-deterministic numeric single-path loops. By reverse engineering invariant synthesis, we then describe an automated method for synthesising program loops satisfying a given set of polynomial loop invariants. Our results have applications towards proving partial correctness of programs, compiler optimisation and generating number sequences from algebraic relations. This is a preprint that was invited for publication at VMCAI 2021.


title: GPURepair: Automated Repair of GPU Kernels

authors:
Saurabh Joshi
Gautam Muduganti

abstract: This paper presents a tool for repairing errors in GPU kernels written in CUDA or OpenCL due to data races and barrier divergence. Our novel extension to prior work can also remove barriers that are deemed unnecessary for correctness. We implement these ideas in our tool called GPURepair, which uses GPUVerify as the verification oracle for GPU kernels. We also extend GPUVerify to support CUDA Cooperative Groups, allowing GPURepair to perform inter-block synchronization for CUDA kernels. To the best of our knowledge, GPURepair is the only tool that can propose a fix for intra-block data races and barrier divergence errors for both CUDA and OpenCL kernels and the only tool that fixes inter-block data races for CUDA kernels. We perform extensive experiments on about 750 kernels and provide a comparison with prior work. We demonstrate the superiority of GPURepair through its capability to fix more kernels and its unique ability to remove redundant barriers and handle inter-block data races.


title: Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible

authors:
Marius Kamp
Michael Philippsen


title: Decomposing Data Structure Commutativity Proofs with $m\!n$-Differencing

authors:
Eric Koskinen
Kshitij Bansal


title: A Design of GPU-Based Quantitative Model Checking

authors:
YoungMin Kwon
Eunhee Kim


title: Compositional Satisfiability Solving in Separation Logic


title: A Self-certifying Compilation Framework for WebAssembly

authors:
Kedar S. Namjoshi
Anton Xue


title: Twinning Automata and Regular Expressions for String Static Analysis

authors:
Luca Negrini
Vincenzo Arceri
Pietro Ferrara
Agostino Cortesi


title: Automated Repair of Heap-Manipulating Programs Using Deductive Synthesis

authors:
Thanh-Toan Nguyen
Quang-Trung Ta
Ilya Sergey
Wei-Ngan Chin


title: On Preprocessing for Weighted MaxSAT

authors:
Tobias Paxian
Pascal Raiola
Bernd Becker


title: Concurrent Correctness in Vector Space

authors:
Christina L. Peterson
Victor Cook
Damian Dechev


title: Unbounded Procedure Summaries from Bounded Environments

authors:
Lauren Pick
Grigory Fedyukovich
Aarti Gupta


title: A Synchronous Effects Logic for Temporal Verification of Pure Esterel

authors:
Yahui Song
Wei-Ngan Chin


title: Generative Program Analysis and Beyond: The Power of Domain-Specific Languages (Invited Paper)

authors:
Bernhard Steffen
Alnis Murtovi


title: Eliminating Message Counters in Synchronous Threshold Automata

authors:
Ilina Stoilkovska
Igor Konnov
Josef Widder
Florian Zuleger


title: Runtime Abstract Interpretation for Numerical Accuracy and Robustness

authors:
Franck Védrine
Maxime Jacquemin
Nikolai Kosmatov
Julien Signoles


title: Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking

authors:
Hongce Zhang
Aarti Gupta
Sharad Malik


title: Netter: Probabilistic, Stateful Network Models

authors:
Han Zhang
Chi Zhang
Arthur Azevedo de Amorim
Yuvraj Agarwal
Matt Fredrikson
Limin Jia


title: Relational String Abstract Domains

authors:
Vincenzo Arceri
Martina Olliaro
Agostino Cortesi
Pietro Ferrara


title: Flavors of Sequential Information Flow

authors:
Ezio Bartocci
Thomas Ferrère
Thomas A. Henzinger
Dejan Nickovic
Ana Oliveira da Costa


title: Fanoos: Multi-resolution, Multi-strength, Interactive Explanations for Learned Systems

authors:
David Bayani
Stefan Mitsch

abstract: Machine learning becomes increasingly important to tune or even synthesize the behavior of safety-critical components in highly non-trivial environments, where the inability to understand learned components in general, and neural nets in particular, poses serious obstacles to their adoption. Explainability and interpretability methods for learned systems have gained considerable academic attention, but the focus of current approaches on only one aspect of explanation, at a fixed level of abstraction, and limited if any formal guarantees, prevents those explanations from being digestible by the relevant stakeholders (e.g., end users, certification authorities, engineers) with their diverse backgrounds and situation-specific needs. We introduce Fanoos, a flexible framework for combining formal verification techniques, heuristic search, and user interaction to explore explanations at the desired level of granularity and fidelity. We demonstrate the ability of Fanoos to produce and adjust the abstractness of explanations in response to user requests on a learned controller for an inverted double pendulum and on a learned CPU usage model.


title: Loop Verification with Invariants and Contracts


title: EPMC Gets Knowledge in Multi-agent Systems

authors:
Chen Fu
Ernst Moritz Hahn
Yong Li
Sven Schewe
Meng Sun
Andrea Turrini
Lijun Zhang


title: High Assurance Software for Financial Regulation and Business Platforms

authors:
Stephen Goldbaum
Attila Mihály
Tosha Ellison
Earl T. Barr
Mark Marron


title: Gradient-Descent for Randomized Controllers Under Partial Observability

authors:
Linus Heck
Jip Spel
Sebastian Junges
Joshua Moerman
Joost-Pieter Katoen

abstract: Randomization is a powerful technique to create robust controllers, in particular in partially observable settings. The degrees of randomization have a significant impact on the system performance, yet they are intricate to get right. The use of synthesis algorithms for parametric Markov chains (pMCs) is a promising direction to support the design process of such controllers. This paper shows how to define and evaluate gradients of pMCs. Furthermore, it investigates varieties of gradient descent techniques from the machine learning community to synthesize the probabilities in a pMC. The resulting method scales to significantly larger pMCs than before and empirically outperforms the state-of-the-art, often by at least one order of magnitude.


title: Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking

authors:
Peter Gjøl Jensen
Jirí Srba
Nikolaj Jensen Ulrik
Simon Mejlby Virenfeldt


title: Verifying Pufferfish Privacy in Hidden Markov Models

authors:
Depeng Liu
Bow-Yaw Wang
Lijun Zhang

abstract: Pufferfish is a Bayesian privacy framework for designing and analyzing privacy mechanisms. It refines differential privacy, the current gold standard in data privacy, by allowing explicit prior knowledge in privacy analysis. Through these privacy frameworks, a number of privacy mechanisms have been developed in literature. In practice, privacy mechanisms often need be modified or adjusted to specific applications. Their privacy risks have to be re-evaluated for different circumstances. Moreover, computing devices only approximate continuous noises through floating-point computation, which is discrete in nature. Privacy proofs can thus be complicated and prone to errors. Such tedious tasks can be burdensome to average data curators. In this paper, we propose an automatic verification technique for Pufferfish privacy. We use hidden Markov models to specify and analyze discretized Pufferfish privacy mechanisms. We show that the Pufferfish verification problem in hidden Markov models is NP-hard. Using Satisfiability Modulo Theories solvers, we propose an algorithm to analyze privacy requirements. We implement our algorithm in a prototypical tool called FAIER, and present several case studies. Surprisingly, our case studies show that naive discretization of well-established privacy mechanisms often fail, witnessed by counterexamples generated by FAIER. In discretized \emph{Above Threshold}, we show that it results in absolutely no privacy. Finally, we compare our approach with testing based approach on several case studies, and show that our verification technique can be combined with testing based approach for the purpose of (i) efficiently certifying counterexamples and (ii) obtaining a better lower bound for the privacy budget $\epsilon$.


title: A Flow-Insensitive-Complete Program Representation

authors:
Solène Mirliaz
David Pichardie

abstract: International audience


title: Lightweight Shape Analysis Based on Physical Types

authors:
Olivier Nicole
Matthieu Lemerre
Xavier Rival


title: Fast Three-Valued Abstract Bit-Vector Arithmetic

authors:
Jan Onderka
Stefan Ratschan


title: Satisfiability and Synthesis Modulo Oracles

authors:
Elizabeth Polgreen
Andrew Reynolds
Sanjit A. Seshia

abstract: In classic program synthesis algorithms, such as counterexample-guided inductive synthesis (CEGIS), the algorithms alternate between a synthesis phase and an oracle (verification) phase. Many synthesis algorithms use a white-box oracle based on satisfiability modulo theory (SMT) solvers to provide counterexamples. But what if a white-box oracle is either not available or not easy to work with? We present a framework for solving a general class of oracle-guided synthesis problems which we term synthesis modulo oracles. In this setting, oracles may be black boxes with a query-response interface defined by the synthesis problem. As a necessary component of this framework, we also formalize the problem of satisfiability modulo theories and oracles, and present an algorithm for solving this problem. We implement a prototype solver for satisfiability and synthesis modulo oracles and demonstrate that, by using oracles that execute functions not easily modeled in SMT-constraints, such as recursive functions or oracles that incorporate compilation and execution of code, SMTO and SyMO are able to solve problems beyond the abilities of standard SMT and synthesis solvers.


title: Bisimulations for Neural Network Reduction

abstract: We present a notion of bisimulation that induces a reduced network which is semantically equivalent to the given neural network. We provide a minimization algorithm to construct the smallest bisimulation equivalent network. Reductions that construct bisimulation equivalent neural networks are limited in the scale of reduction. We present an approximate notion of bisimulation that provides semantic closeness, rather than, semantic equivalence, and quantify semantic deviation between the neural networks that are approximately bisimilar. The latter provides a trade-off between the amount of reduction and deviations in the semantics.


title: NP Satisfiability for Arrays as Powers

authors:
Rodrigo Raya
Viktor Kuncak

abstract: We show that the satisfiability problem for the quantifier-free theory of product structures with the equicardinality relation is in NP. As an application, we extend the combinatory array logic fragment to handle cardinality constraints. The resulting fragment is independent of the base element and index set theories.


title: STAMINA 2.0: Improving Scalability of Infinite-State Stochastic Model Checking

authors:
Riley Roberts
Thakur Neupane
Lukas Buecherl
Chris J. Myers
Zhen Zhang


title: Generalized Arrays for Stainless Frames

authors:
Georg Stefan Schmid
Viktor Kuncak

abstract: . We present an approach for veriﬁcation of programs with shared mutable references against speciﬁcations such as assertions, pre-conditions, postconditions, and read/write eﬀects. We implement our tool in the Stainless veriﬁcation system for Scala. A novelty of our approach is to translate imperative function contracts (including frame conditions) using quantiﬁer-free formulas in ﬁrst-order logic, instead of quantiﬁers or separation logic. Our quantiﬁer-free encoding enables SMT solvers to both prove safety and to report counterex-amples relative to the semantics of procedure contracts. Our encoding is possible thanks to the expressive power of the extended array theory of de Moura and Bjørner, implemented in the SMT solver Z3, whose map operators allow us to project heaps before and after the call onto the declared reads and modiﬁes clauses. To support inductive proofs about the preservation of invariants, our approach permits capturing a projection of heap state as a history variable and evaluating imperative ghost code in the speciﬁed captured heap. We also retain the eﬃciency of reasoning about purely functional layers of data structures, which need not be represented using heap references but often map directly to SMT-LIB algebraic data types and arrays. We thus obtain a combination of expressiveness for shared mutable data where needed, while retaining automation for purely functional program aspects. We illustrate our approach by proving detailed correctness properties of examples manipulating mutable linked structures.


title: Making PROGRESS in Property Directed Reachability

authors:
Tobias Seufert
Christoph Scholl
Arun Chandrasekharan
Sven Reimer
Tobias Welp


title: Scaling Up Livelock Verification for Network-on-Chip Routing Algorithms

authors:
Landon Taylor
Zhen Zhang


title: Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applications that Do Not Terminate

authors:
Rahmadi Trimananda
Weiyu Luo
Brian Demsky
Guoqing Harry Xu

abstract: Event-driven architectures are broadly used for systems that must respond to events in the real world. Event-driven applications are prone to concurrency bugs that involve subtle errors in reasoning about the ordering of events. Unfortunately, there are several challenges in using existing model-checking techniques on these systems. Event-driven applications often loop indefinitely and thus pose a challenge for stateless model checking techniques. On the other hand, deploying purely stateful model checking can explore large sets of equivalent executions. In this work, we explore a new technique that combines dynamic partial order reduction with stateful model checking to support non-terminating applications. Our work is (1) the first dynamic partial order reduction algorithm for stateful model checking that is sound for non-terminating applications and (2) the first dynamic partial reduction algorithm for stateful model checking of event-driven applications. We experimented with the IoTCheck dataset: a study of interactions in smart home app pairs. This dataset consists of app pairs originated from 198 real-world smart home apps. Overall, our DPOR algorithm successfully reduced the search space for the app pairs, enabling 69 pairs of apps that did not finish without DPOR to finish and providing a 7X average speedup.


title: Verifying Solidity Smart Contracts via Communication Abstraction in SmartACE

authors:
Scott Wesley
Maria Christakis
Jorge A. Navas
Richard J. Trefler
Valentin Wüstholz
Arie Gurfinkel


title: Out of Control: Reducing Probabilistic Models by Control-State Elimination

authors:
Tobias Winkler
Johannes Lehmann
Joost-Pieter Katoen

abstract: State-of-the-art probabilistic model checkers perform verification on explicit-state Markov models defined in a high-level programming formalism like the PRISM modeling language. Typically, the low-level models resulting from such program-like specifications exhibit lots of structure such as repeating subpatterns. Established techniques like probabilistic bisimulation minimization are able to exploit these structures; however, they operate directly on the explicit-state model. On the other hand, methods for reducing structured state spaces by reasoning about the high-level program have not been investigated that much. In this paper, we present a new, simple, and fully automatic program-level technique to reduce the underlying Markov model. Our approach aims at computing the summary behavior of adjacent locations in the program's control-flow graph, thereby obtaining a program with fewer"control states". This reduction is immediately reflected in the program's operational semantics, enabling more efficient model checking. A key insight is that in principle, each (combination of) program variable(s) with finite domain can play the role of the program counter that defines the flow structure. Unlike most other reduction techniques, our approach is property-directed and naturally supports unspecified model parameters. Experiments demonstrate that our simple method yields state-space reductions of up to 80% on practically relevant benchmarks.


title: Mixed Semantics Guided Layered Bounded Reachability Analysis of Compositional Linear Hybrid Automata

authors:
Yuming Wu
Lei Bu
Jiawan Wang
Xinyue Ren
Wen Xiong
Xuandong Li


title: Bit-Precise Reasoning via Int-Blasting

authors:
Yoni Zohar
Ahmed Irfan
Makai Mann
Aina Niemetz
Andres Nötzli
Mathias Preiner
Andrew Reynolds
Clark W. Barrett
Cesare Tinelli


title: Distributing and Parallelizing Non-canonical Loops

authors:
Clément Aubert
Thomas Rubiano
Neea Rusch
Thomas Seiller


title: SMT-Based Modeling and Verification of Spiking Neural Networks: A Case Study

authors:
Soham Banerjee
Sumana Ghosh
Ansuman Banerjee
Swarup Kumar Mohalik


title: StaticPersist: Compiler Support for PMEM Programming


title: Symbolic Abstract Heaps for Polymorphic Information-Flow Guard Inference

authors:
Nicolas Berthier
Narges Khakpour


title: Satisfiability Modulo Custom Theories in Z3

authors:
Nikolaj S. Bjørner
Clemens Eisenhofer
Laura Kovács


title: Bayesian Parameter Estimation with Guarantees via Interval Analysis and Simulation

authors:
Michele Boreale
Luisa Collodi


title: A Pragmatic Approach to Stateful Partial Order Reduction

authors:
Berk Çirisci
Constantin Enea
Azadeh Farzan
Suha Orhun Mutluergil


title: A Generic Framework to Coarse-Grain Stochastic Reaction Networks by Abstract Interpretation

authors:
Jérôme Feret
Albin Salazar

abstract: . In the last decades, logical or discrete models have emerged as a successful paradigm for capturing and predicting the behaviors of systems of molecular interactions. Intuitively, they consist in sampling the abundance of each kind of biochemical entity within finite sets of intervals and deriving transitions accordingly. On one hand, formally-proven sound derivation from more precise descriptions (such as from reaction networks) may include many fictitious behaviors. On the other hand, direct modeling usually favors dominant interactions with no guarantee on the behaviors that are neglected. In this paper, we formalize a sound coarse-graining approach for stochastic reaction networks. Its originality relies on two main ingredients. Firstly, we abstract values by intervals that overlap in order to introduce a minimal effort for the system to go back to the previous interval, hence limiting fictitious oscillations in the coarse-grained models. Sec-ondly, we compute for pairs of transitions (in the coarse-grained model) bounds on the probabilities on which one will occur first. We illustrate our ideas on two case studies and demonstrate how techniques from Abstract Interpretation can be used to design more precise discretization methods, while providing a framework to further investigate the underlying structure of logical and discrete models.


title: Efficient Interprocedural Data-Flow Analysis Using Treedepth and Treewidth

authors:
Amir Kafshdar Goharshady
Ahmed Khaled Zaher


title: Maximal Robust Neural Network Specifications via Oracle-Guided Numerical Optimization

authors:
Anan Kabaha
Dana Drachsler-Cohen


title: Result Invalidation for Incremental Modular Analyses

authors:
Jens Van der Plas
Quentin Stiévenart
Coen De Roover


title: CosySEL: Improving SAT Solving Using Local Symmetries

authors:
Sabrine Saouli
Souheib Baarir
Claude Dutheillet
Jo Devriendt


title: Compositional Verification of Stigmergic Collective Systems

authors:
Luca Di Stefano
Frédéric Lang


title: Sound Symbolic Execution via Abstract Interpretation and Its Application to Security

authors:
Ignacio Tiraboschi
Tamara Rezk
Xavier Rival

abstract: Symbolic execution is a program analysis technique commonly utilized to determine whether programs violate properties and, in case violations are found, to generate inputs that can trigger them. Used in the context of security properties such as noninterference, symbolic execution is precise when looking for counterexample pairs of traces when insecure information flows are found, however it is sound only up to a bound thus it does not allow to prove the correctness of programs with executions beyond the given bound. By contrast, abstract interpretation-based static analysis guarantees soundness but generally lacks the ability to provide counterexample pairs of traces. In this paper, we propose to weave both to obtain the best of two worlds. We demonstrate this with a series of static analyses, including a static analysis called RedSoundRSE aimed at verifying noninterference. RedSoundRSE provides both semantically sound results and the ability to derive counterexample pairs of traces up to a bound. It relies on a combination of symbolic execution and abstract domains inspired by the well known notion of reduced product. We formalize RedSoundRSE and prove its soundness as well as its relative precision up to a bound. We also provide a prototype implementation of RedSoundRSE and evaluate it on a sample of challenging examples.


title: Synthesizing History and Prophecy Variables for Symbolic Model Checking

authors:
Cole Vick
Kenneth L. McMillan


title: Solving Constrained Horn Clauses over Algebraic Data Types

authors:
Lucas Zavalía
Lidiia Chernigovskaia
Grigory Fedyukovich


title: ARENA: Enhancing Abstract Refinement for Neural Network Verification

authors:
Yuyi Zhong
Quang-Trung Ta
Siau-Cheng Khoo


title: Boosting Constrained Horn Solving by Unsat Core Learning

authors:
Parosh Aziz Abdulla
Chencheng Liang
Philipp Rümmer


title: Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability

authors:
Nicolas Amat
Silvano Dal-Zilio
Didier Le Botlan

abstract: We propose a method for checking generalized reachability properties in Petri nets that takes advantage of structural reductions and that can be used, transparently, as a pre-processing step of existing model-checkers. Our approach is based on a new procedure that can project a property, about an initial Petri net, into an equivalent formula that only refers to the reduced version of this net. Our projection is defined as a variable elimination procedure for linear integer arithmetic tailored to the specific kind of constraints we handle. It has linear complexity, is guaranteed to return a sound property, and makes use of a simple condition to detect when the result is exact. Experimental results show that our approach works well in practice and that it can be useful even when there is only a limited amount of reductions.


title: Parameterized Verification of Disjunctive Timed Networks

authors:
Étienne André
Paul Eichler
Swen Jacobs
Shyam Lal Karra

abstract: We introduce new techniques for the parameterized verification of disjunctive timed networks (DTNs), i.e., networks of timed automata (TAs) that communicate via location guards that enable a transition only if there is another process in a given location. This computational model has been considered in the literature before, example applications are gossiping clock synchronization protocols or planning problems. We address the minimum-time reachability problem (Minreach) in DTNs, and show how to efficiently solve it based on a novel zone graph algorithm. We further show that solving Minreach allows us to construct a summary TA capturing exactly the possible behaviors of a single TA within a DTN of arbitrary size. The combination of these two results enables the parameterized verification of DTNs, while avoiding the construction of an exponential-size cutoff system required by existing results. Additionally, we develop sufficient conditions for solving Minreach and parameterized verification problems even in certain cases where locations that appear in location guards can have clock invariants, a case that has usually been excluded in the literature. Our techniques are also implemented, and experiments show their practicality.


title: Automatic and Incremental Repair for Speculative Information Leaks

authors:
Joachim Bard
Swen Jacobs
Yakir Vizel


title: A Fully Verified Persistency Library

authors:
Stefan Bodenmüller
John Derrick
Brijesh Dongol
Gerhard Schellhorn
Heike Wehrheim

abstract: . Non-volatile memory (NVM) technologies offer DRAM-like speeds with the added benefit of failure resilience. However, developing concurrent programs for NVM can be challenging since programmers must consider both inter-thread synchronisation and durability aspects at the same time. To alleviate this, libraries such as FliT have been developed to manage transformations to durability , allowing a linearizable concurrent object to be converted into a durably linearizable one by replacing the reads/writes to memory by calls to corresponding operations of the FliT library. However, a formal proof of correctness for FliT is missing, and standard proof techniques for durable linearizability are challenging to apply, since FliT itself is not durably linearizable. In this paper, we study the problem of proving correctness of transformations to durability. First, we develop an abstract persistency library (called PLib ) that operationally characterises transformations to durability. We prove soundness of PLib via a forward simulation coupled with a prophecy variable used as an oracle about future behaviour. Second, we show correctness of the library FliT by proving that FliT refines PLib under the realistic PTSO memory model, i.e., the persistent version of TSO memory model implemented by Intel architectures. The proof of refinement between FliT and PLib has been mechanised within the theorem prover KIV. Taken together, these proofs guarantee that FliT is also sound wrt transformations to durability.


title: On the Verification of the Correctness of a Subgraph Construction Algorithm

authors:
Lucas Böltz
Viorica Sofronie-Stokkermans
Hannes Frey


title: Guaranteed Inference for Probabilistic Programs: A Parallelisable, Small-Step Operational Approach

authors:
Michele Boreale
Luisa Collodi


title: Automatically Enforcing Rust Trait Properties

authors:
Twain Byrnes
Yoshiki Takashima
Limin Jia


title: Local Reasoning About Probabilistic Behaviour for Classical-Quantum Programs

authors:
Yuxin Deng
Huiling Wu
Ming Xu


title: AGNES: Abstraction-Guided Framework for Deep Neural Networks Security

authors:
Akshay Dhonthi
Marcello Eiermann
Ernst Moritz Hahn
Vahid Hashemi

abstract: Deep Neural Networks (DNNs) are becoming widespread, particularly in safety-critical areas. One prominent application is image recognition in autonomous driving, where the correct classification of objects, such as traffic signs, is essential for safe driving. Unfortunately, DNNs are prone to backdoors, meaning that they concentrate on attributes of the image that should be irrelevant for their correct classification. Backdoors are integrated into a DNN during training, either with malicious intent (such as a manipulated training process, because of which a yellow sticker always leads to a traffic sign being recognised as a stop sign) or unintentional (such as a rural background leading to any traffic sign being recognised as animal crossing, because of biased training data). In this paper, we introduce AGNES, a tool to detect backdoors in DNNs for image recognition. We discuss the principle approach on which AGNES is based. Afterwards, we show that our tool performs better than many state-of-the-art methods for multiple relevant case studies.


title: Resilience and Home-Space for WSTS

authors:
Alain Finkel
Mathieu Hilaire


title: Interpolation and Quantifiers in Ortholattices

authors:
Simon Guilloud
Sankalp Gambhir
Viktor Kuncak

abstract: We study quantifiers and interpolation properties in \emph{orthologic}, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based proof system for quantified orthologic, which we prove sound and complete for the class of all complete ortholattices. We show that orthologic does not admit quantifier elimination in general. Despite that, we show that interpolants always exist in orthologic. We give an algorithm to compute interpolants efficiently. We expect our result to be useful to quickly establish unreachability as a component of verification algorithms.


title: Generic Model Checking for Modal Fixpoint Logics in COOL-MC

authors:
Daniel Hausmann
Merlin Humml
Simon Prucker
Lutz Schröder
Aaron Strahlberger


title: TP-DejaVu: Combining Operational and Declarative Runtime Verification

authors:
Klaus Havelund
Panagiotis Katsaros
Moran Omer
Doron Peled
Anastasios Temperekidis


title: Formal Runtime Error Detection During Development in the Automotive Industry

authors:
Jesko Hecking-Harbusch
Jochen Quante
Maximilian Schlund


title: Petrification: Software Model Checking for Programs with Dynamic Thread Management

authors:
Matthias Heizmann
Dominik Klumpp
Lars Nitzke
Frank Schüssele


title: A Navigation Logic for Recursive Programs with Dynamic Thread Creation

authors:
Roman Lakenbrink
Markus Müller-Olm
Christoph Ohrem
Jens Oliver Gutsfeld


title: Generation of Violation Witnesses by Under-Approximating Abstract Interpretation

authors:
Marco Milanese
Antoine Miné


title: Borrowable Fractional Ownership Types for Verification

authors:
Takashi Nakayama
Yusuke Matsushita
Ken Sakayori
Ryosuke Sato
Naoki Kobayashi


title: Abstract Interpretation-Based Feature Importance for Support Vector Machines

authors:
Abhinandan Pal
Francesco Ranzato
Caterina Urban
Marco Zanella


title: Sound Abstract Nonexploitability Analysis

authors:
Francesco Parolini
Antoine Miné


title: Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic

authors:
Ritam Raha
Rajarshi Roy
Nathanaël Fijalkow
Daniel Neider
Guillermo A. Pérez


title: Verification of Neural Networks' Local Differential Classification Privacy

authors:
Roie Reshef
Anan Kabaha
Olga Seleznova
Dana Drachsler-Cohen


title: Correctness Witness Validation by Abstract Interpretation

authors:
Simmo Saan
Michael Schwarz
Julian Erhard
Helmut Seidl
Sarah Tilscher
Vesal Vojdani

abstract: Witnesses record automated program analysis results and make them exchangeable. To validate correctness witnesses through abstract interpretation, we introduce a novel abstract operation unassume. This operator incorporates witness invariants into the abstract program state. Given suitable invariants, the unassume operation can accelerate fixpoint convergence and yield more precise results. We demonstrate the feasibility of this approach by augmenting an abstract interpreter with unassume operators and evaluating the impact of incorporating witnesses on performance and precision. Using manually crafted witnesses, we can confirm verification results for multi-threaded programs with a reduction in effort ranging from 7% to 47% in CPU time. More intriguingly, we discover that using witnesses from model checkers can guide our analyzer to verify program properties that it could not verify on its own.


title: Solving Two-Player Games Under Progress Assumptions

authors:
Anne-Kathrin Schmuck
K. S. Thejaswini
Irmak Saglam
Satya Prakash Nayak

abstract: This paper considers the problem of solving infinite two-player games over finite graphs under various classes of progress assumptions motivated by applications in cyber-physical system (CPS) design. Formally, we consider a game graph G, a temporal specification $\Phi$ and a temporal assumption $\psi$, where both are given as linear temporal logic (LTL) formulas over the vertex set of G. We call the tuple $(G,\Phi,\psi)$ an 'augmented game' and interpret it in the classical way, i.e., winning the augmented game $(G,\Phi,\psi)$ is equivalent to winning the (standard) game $(G,\psi \implies \Phi)$. Given a reachability or parity game $(G,\Phi)$ and some progress assumption $\psi$, this paper establishes whether solving the augmented game $(G,\Phi,\psi)$ lies in the same complexity class as solving $(G,\Phi)$. While the answer to this question is negative for arbitrary combinations of $\Phi$ and $\psi$, a positive answer results in more efficient algorithms, in particular for large game graphs. We therefore restrict our attention to particular classes of CPS-motivated progress assumptions and establish the worst-case time complexity of the resulting augmented games. Thereby, we pave the way towards a better understanding of assumption classes that can enable the development of efficient solution algorithms in augmented two-player games.


title: Deductive Verification of Parameterized Embedded Systems Modeled in SystemC

authors:
Philip Tasche
Raúl E. Monti
Stefanie Eva Drerup
Pauline Blohm
Paula Herber
Marieke Huisman


title: Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training

authors:
Jiaxu Tian
Dapeng Zhi
Si Liu
Peixin Wang
Guy Katz
Min Zhang

abstract: The intrinsic complexity of deep neural networks (DNNs) makes it challenging to verify not only the networks themselves but also the hosting DNN-controlled systems. Reachability analysis of these systems faces the same challenge. Existing approaches rely on over-approximating DNNs using simpler polynomial models. However, they suffer from low efficiency and large overestimation, and are restricted to specific types of DNNs. This paper presents a novel abstraction-based approach to bypass the crux of over-approximating DNNs in reachability analysis. Specifically, we extend conventional DNNs by inserting an additional abstraction layer, which abstracts a real number to an interval for training. The inserted abstraction layer ensures that the values represented by an interval are indistinguishable to the network for both training and decision-making. Leveraging this, we devise the first black-box reachability analysis approach for DNN-controlled systems, where trained DNNs are only queried as black-box oracles for the actions on abstract states. Our approach is sound, tight, efficient, and agnostic to any DNN type and size. The experimental results on a wide range of benchmarks show that the DNNs trained by using our approach exhibit comparable performance, while the reachability analysis of the corresponding systems becomes more amenable with significant tightness and efficiency improvement over the state-of-the-art white-box approaches.


title: Function Synthesis for Maximizing Model Counting

authors:
Thomas Vigouroux
Marius Bozga
Cristian Ene
Laurent Mounier


title: Efficient Local Search for Nonlinear Real Arithmetic

authors:
Zhonghan Wang
Bohua Zhan
Bohan Li
Shaowei Cai


title: Model-Guided Synthesis for LTL over Finite Traces

authors:
Shengping Xiao
Yongkang Li
Xinyue Huang
Yicong Xu
Jianwen Li
Geguang Pu
Ofer Strichman
Moshe Y. Vardi


title: A Static Analysis of Entanglement

authors:
Nicola Assolini
Alessandra Di Pierro
Isabella Mastroeni