title: Faster Statistical Model Checking for Unbounded Temporal Properties

authors:
Przemyslaw Daca
Thomas A. Henzinger
Jan Kretínský
Tatjana Petrov

abstract: We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


venue: tacas

title: Runtime Monitoring with Union-Find Structures

authors:
Normann Decker
Jannis Harder
Torben Scheffel
Malte Schmitz
Daniel Thoma


title: Multi-core Symbolic Bisimulation Minimisation

authors:
Tom van Dijk
Jaco van de Pol


title: Probabilistic CTL*: The Deductive Way

authors:
Rayna Dimitrova
Luis María Ferrer Fioriti
Holger Hermanns
Rupak Majumdar

abstract:
Complex probabilistic temporal behaviours need to be guaranteed in robotics and various other control domains, as well as in the context of families of randomized protocols. At its core, this entails checking infinite-state probabilistic systems with respect to quantitative properties specified in probabilistic temporal logics. Model checking methods are not directly applicable to infinite-state systems, and techniques for infinite-state probabilistic systems are limited in terms of the specifications they can handle.

This paper presents a deductive approach to the verification of countable-state systems against properties specified in probabilistic CTL$$^{*}$$, on models featuring both nondeterministic and probabilistic choices. The deductive proof system we propose lifts the classical proof system by Kesten and Pnueli to the probabilistic setting. However, the soundness arguments are completely distinct and go via the theory of martingales. Completeness results for the finite-state case and an infinite-state example illustrate the effectiveness of our approach.


title: On Atomicity in Presence of Non-atomic Writes

authors:
Constantin Enea
Azadeh Farzan


title: DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation


title: Coqoon - An IDE for Interactive Proof Development in Coq

authors:
Alexander John Faithfull
Jesper Bengtson
Enrico Tassi
Carst Tankink

abstract: International audience


title: Diagnostic Information for Control-Flow Analysis of Workflow Graphs (a.k.a. Free-Choice Workflow Nets)

authors:
Cédric Favre
Hagen Völzer
Peter Müller


title: CPA-BAM: Block-Abstraction Memoization with Value Analysis and Predicate Analysis - (Competition Contribution)


title: Interpolants in Nonlinear Theories Over the Reals

authors:
Sicun Gao
Damien Zufferey


title: An O(m\log n) Algorithm for Stuttering Equivalence and Branching Bisimulation

authors:
Jan Friso Groote
Anton Wijs

abstract: We provide a new algorithm to determine stuttering equivalence with time complexity $$Om \log n$$, where n is the number of states and m is the number of transitions of a Kripke structure. This algorithm can also be used to determine branching bisimulation in $$Om\log | Act |+\log n$$ time. Theoretically, our algorithm substantially improves upon existing algorithms which all have time complexity Omn [2, 3, 9]. Moreover, it has better or equal space complexity. Practical results confirm these findings showing that our algorithm can outperform existing algorithms with orders of magnitude, especially when the sizes of the Kripke structures are large.


title: Tactics for the Dafny Program Verifier

authors:
Gudmund Grov
Vytautas Tumas


title: Vienna Verification Tool: IC3 for Parallel Software - (Competition Contribution)

authors:
Henning Günther
Alfons Laarman
Georg Weissenbacher


title: Ultimate Automizer with Two-track Proofs - (Competition Contribution)

authors:
Matthias Heizmann
Daniel Dietsch
Marius Greitschus
Jan Leike
Betim Musa
Claus Schätzle
Andreas Podelski


title: Run Forester, Run Backwards! - (Competition Contribution)

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


title: Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems

authors:
Radu Iosif
Adam Rogalewicz
Tomás Vojnar


title: PrDK: Protocol Programming with Automata

authors:
Sung-Shik T. Q. Jongmans
Farhad Arbab


title: Safety-Constrained Reinforcement Learning for MDPs

authors:
Sebastian Junges
Nils Jansen
Christian Dehnert
Ufuk Topcu
Joost-Pieter Katoen

abstract: We consider controller synthesis for stochastic and partially unknown environments in which safety is essential. Specifically, we abstract the problem as a Markov decision process in which the expected performance is measured using a cost function that is unknown prior to run-time exploration of the state space. Standard learning approaches synthesize cost-optimal strategies without guaranteeing safety properties. To remedy this, we first compute safe, permissive strategies. Then, exploration is constrained to these strategies and thereby meets the imposed safety requirements. Exploiting an iterative learning procedure, the resulting strategy is safety-constrained and optimal. We show correctness and completeness of the method and discuss the use of several heuristics to increase its scalability. Finally, we demonstrate the applicability by means of a prototype implementation.


title: LPI: Software Verification with Local Policy Iteration - (Competition Contribution)


title: PTIME Computation of Transitive Closures of Octagonal Relations

abstract: Computing transitive closures of integer relations is the key to finding precise invariants of integer programs. In this paper, we study difference bounds and octagonal relations and prove that their transitive closure is a PTIME-computable formula in the existential fragment of Presburger arithmetic. This result marks a significant complexity improvement, as the known algorithms have EXPTIME worst case complexity.


title: Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark - (Competition Contribution)

authors:
Michal Kotoun
Petr Peringer
Veronika Soková
Tomás Vojnar


title: PRISM-Games 2.0: A Tool for Multi-objective Strategy Synthesis for Stochastic Games

authors:
Marta Kwiatkowska
David Parker
Clemens Wiltsche


title: Characteristic Formulae for Session Types

authors:
Julien Lange
Nobuko Yoshida

abstract: Subtyping is a crucial ingredient of session type theory and its applications, notably to programming language implementations. In this paper, we study effective ways to check whether a session type is a subtype of another by applying a characteristic formulae approach to the problem. Our core contribution is an algorithm to generate a modal $$\mu $$-calculus formula that characterises all the supertypes or subtypes of a given type. Subtyping checks can then be off-loaded to model checkers, thus incidentally yielding an efficient algorithm to check safety of session types, soundly and completely. We have implemented our theory and compared its cost with other classical subtyping algorithms.


title: Online and Compositional Learning of Controllers with Application to Floor Heating

authors:
Kim G. Larsen
Marius Mikucionis
Marco Muñiz
Jirí Srba
Jakob Haahr Taankvist


title: Developing and Debugging Proof Strategies by Tinkering

authors:
Yuhui Lin
Pierre Le Bras
Gudmund Grov


title: Abstract Learning Frameworks for Synthesis

authors:
Christof Löding
P. Madhusudan
Daniel Neider

abstract: We develop abstract learning frameworks for synthesis that embody the principles of the CEGIS counterexample-guided inductive synthesis algorithms in current literature. Our framework is based on iterative learning from a hypothesis space that captures synthesized objects, using counterexamples from an abstract sample space, and a concept space that abstractly defines the semantics of synthesis. We show that a variety of synthesis algorithms in current literature can be embedded in this general framework. We also exhibit three general recipes for convergent synthesis: the first two recipes based on finite spaces and Occam learners generalize all techniques of convergence used in existing engines, while the third, involving well-founded quasi-orderings, is new, and we instantiate it to concrete synthesis problems.


title: CPA-RefSel: CPAchecker with Refinement Selection - (Competition Contribution)


title: JDart: A Dynamic Symbolic Analysis Framework

authors:
Kasper Søe Luckow
Marko Dimjasevic
Dimitra Giannakopoulou
Falk Howar
Malte Isberner
Temesghen Kahsai
Zvonimir Rakamaric
Vishwanath Raman


title: Partial Order Reduction for Event-Driven Multi-threaded Programs

authors:
Pallavi Maiya
Rahul Gupta
Aditya Kanade
Rupak Majumdar


title: Robots at the Edge of the Cloud


title: v2c - A Verilog to C Translator

authors:
Rajdeep Mukherjee
Michael Tautschnig
Daniel Kroening


title: Bit-Vector Optimization

authors:
Alexander Nadel
Vadim Ryvchin


title: Parameterized Compositional Model Checking

authors:
Kedar S. Namjoshi
Richard J. Trefler


title: Synthesizing Piece-Wise Functions by Learning Classifiers

authors:
Daniel Neider
Shambwaditya Saha
P. Madhusudan


title: An Automaton Learning Approach to Solving Safety Games over Infinite Graphs

authors:
Daniel Neider
Ufuk Topcu

abstract: We propose a method to construct finite-state reactive controllers for systems whose interactions with their adversarial environment are modeled by infinite-duration two-player games over possibly infinite graphs. The method targets safety games with infinitely many states or with such a large number of states that it would be impractical--if not impossible--for conventional synthesis techniques that work on the entire state space. We resort to constructing finite-state controllers for such systems through an automata learning approach, utilizing a symbolic representation of the underlying game that is based on finite automata. Throughout the learning process, the learner maintains an approximation of the winning region represented as a finite automaton and refines it using different types of counterexamples provided by the teacher until a satisfactory controller can be derived if one exists. We present a symbolic representation of safety games inspired by regular model checking, propose implementations of the learner and teacher, and evaluate their performance on examples motivated by robotic motion planning.


title: Scalable Verification of Linear Controller Software

authors:
Junkil Park
Miroslav Pajic
Insup Lee
Oleg Sokolsky


title: Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models

authors:
Daniel Poetzl
Daniel Kroening

abstract: When optimizing a thread in a concurrent program (either done manually or by the compiler), it must be guaranteed that the resulting thread is a refinement of the original thread. Most theories of valid optimizations are formulated in terms of valid syntactic transformations on the program code, or in terms of valid transformations on thread execution traces. We present a new theory formulated instead in terms of the state of threads at synchronization operations, and show that it provides several advantages: it supports more optimizations, and leads to more efficient and simpler procedures for refinement checking. We develop the theory for the SC-for-DRF execution model (using locks for synchronization), and show that its application in a compiler testing setting leads to large performance improvements.


title: RTD-Finder: A Tool for Compositional Verification of Real-Time Component-Based Systems

authors:
Souha Ben Rayana
Marius Bozga
Saddek Bensalem
Jacques Combaz


title: Hunting Memory Bugs in C Programs with Map2Check - (Competition Contribution)

authors:
Herbert O. Rocha
Raimundo S. Barreto
Lucas C. Cordeiro


title: Hybridization Based CEGAR for Hybrid Automata with Affine Dynamics

authors:
Nima Roohi
Pavithra Prabhakar
Mahesh Viswanathan


title: LCTD: Tests-Guided Proofs for C Programs on LLVM - (Competition Contribution)

authors:
Olli Saarikivi
Keijo Heljanko


title: 2LS for Program Analysis - (Competition Contribution)

authors:
Peter Schrammel
Daniel Kroening


title: Safety Verification of Continuous-Space Pure Jump Markov Processes

authors:
Sadegh Esmaeil Zadeh Soudjani
Rupak Majumdar
Alessandro Abate


title: DIVINE: Explicit-State LTL Model Checker - (Competition Contribution)

authors:
Vladimír Still
Petr Rockai
Jiri Barnat


title: MU-CSeq 0.4: Individual Memory Location Unwindings - (Competition Contribution)

authors:
Ermenegildo Tomasco
Truc L. Nguyen
Omar Inverso
Bernd Fischer
Salvatore La Torre
Gennaro Parlato


title: Online Timed Pattern Matching Using Derivatives

authors:
Dogan Ulus
Thomas Ferrère
Eugene Asarin
Oded Maler


title: Synthesizing Ranking Functions from Bits and Pieces

authors:
Caterina Urban
Arie Gurfinkel
Temesghen Kahsai


title: Some Complexity Results for Stateful Network Verification

authors:
Yaron Velner
Kalev Alpernas
Aurojit Panda
Alexander Rabinovich
Mooly Sagiv
Scott Shenker
Sharon Shoham


title: Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication

authors:
Yongwang Zhao
David Sanán
Fuyuan Zhang
Yang Liu

abstract: Assurance of information flow security by formal methods is mandated in security certification of separation kernels. As an industrial standard for separation kernels, ARINC 653 has been complied with by mainstream separation kernels. Security of functionalities defined in ARINC 653 is thus very important for the development and certification of separation kernels. This paper presents the first effort to formally specify and verify separation kernels with ARINC 653 channel-based communication. We provide a reusable formal specification and security proofs for separation kernels in Isabelle/HOL. During reasoning about information flow security, we find some security flaws in the ARINC 653 standard, which can cause information leakage, and fix them in our specification. We also validate the existence of the security flaws in two open-source ARINC 653 compliant separation kernels.


title: CIVL: Applying a General Concurrency Verification Framework to C/Pthreads Programs (Competition Contribution)

authors:
Manchun Zheng
John G. Edenhofner
Ziqing Luo
Mitchell J. Gerrard
Michael S. Rogers
Matthew B. Dwyer
Stephen F. Siegel


title: Context-Bounded Analysis for POWER

authors:
Parosh Aziz Abdulla
Mohamed Faouzi Atig
Ahmed Bouajjani
Tuan Phong Ngo

abstract: We propose an under-approximate reachability analysis algorithm for programs running under the POWER memory model, in the spirit of the work on context-bounded analysis intitiated by Qadeer et al. in 2005 for detecting bugs in concurrent programs supposed to be running under the classical SC model. To that end, we first introduce a new notion of context-bounding that is suitable for reasoning about computations under POWER, which generalizes the one defined by Atig et al. in 2011 for the TSO memory model. Then, we provide a polynomial size reduction of the context-bounded state reachability problem under POWER to the same problem under SC: Given an input concurrent program $$\mathcal {P}$$, our method produces a concurrent program $$\mathcal {P}'$$ such that, for a fixed number of context switches, running $$\mathcal {P}'$$ under SC yields the same set of reachable states as running $$\mathcal {P}$$ under POWER. The generated program $$\mathcal {P}'$$ contains the same number of processes as $$\mathcal {P}$$, and operates on the same data domain. By leveraging the standard model checker CBMC, we have implemented a prototype tool and applied it on a set of benchmarks, showing the feasibility of our approach.


title: Towards Parallel Boolean Functional Synthesis

authors:
S. Akshay
Supratik Chakraborty
Ajith K. John
Shetal Shah

abstract: Given a relational specification \(\varphi (X, Y)\), where X and Y are sequences of input and output variables, we wish to synthesize each output as a function of the inputs such that the specification holds. This is called the Boolean functional synthesis problem and has applications in several areas. In this paper, we present the first parallel approach for solving this problem, using compositional and CEGAR-style reasoning as key building blocks. We show by means of extensive experiments that our approach outperforms existing tools on a large class of benchmarks.


title: HiFrog: SMT-based Function Summarization for Software Verification

authors:
Leonardo Alt
Sepideh Asadi
Hana Chockler
Karine Even-Mendoza
Grigory Fedyukovich
Antti E. J. Hyvärinen
Natasha Sharygina


title: Scaling Enumerative Program Synthesis via Divide and Conquer

authors:
Rajeev Alur
Arjun Radhakrishna
Abhishek Udupa


title: Combining String Abstract Domains for JavaScript Analysis: An Evaluation

authors:
Roberto Amadini
Alexander Jordan
Graeme Gange
François Gauthier
Peter Schachte
Harald Søndergaard
Peter J. Stuckey
Chenyi Zhang


title: CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions - (Competition Contribution)

authors:
Pavel S. Andrianov
Karlheinz Friedberger
Mikhail U. Mandrykin
Vadim S. Mutilin
Anton Volkov


title: The Automatic Detection of Token Structures and Invariants Using SAT Checking

authors:
Pedro R. G. Antonino
Thomas Gibson-Robinson
A. W. Roscoe


title: Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults

authors:
Guy Avni
Shubham Goel
Thomas A. Henzinger
Guillermo Rodríguez-Navas

abstract:
Time-triggered switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. Due to the criticality of the applications running over them, developers need to ensure that end-to-end communication is dependable and predictable. Traditional approaches assume static networks that are not flexible to changes caused by reconfigurations or, more importantly, faults, which are dealt with in the application using redundancy. We adopt the concept of handling faults in the switches from non-real-time networks while maintaining the required predictability.

We study a class of forwarding schemes that can handle various types of failures. We consider probabilistic failures. For a given network with a forwarding scheme and a constant $$\ell $$, we compute the score of the scheme, namely the probability induced by faults that at least $$\ell $$ messages arrive on time. We reduce the scoring problem to a reachability problem on a Markov chain with a "product-like" structure. Its special structure allows us to reason about it symbolically, and reduce the scoring problem to #SAT. Our solution is generic and can be adapted to different networks and other contexts. Also, we show the computational complexity of the scoring problem is #P-complete, and we study methods to estimate the score. We evaluate the effectiveness of our techniques with an implementation.


title: Maximizing the Conditional Expected Reward for Reaching the Goal

authors:
Christel Baier
Joachim Klein
Sascha Klüppelholz
Sascha Wunderlich

abstract: The paper addresses the problem of computing maximal conditional expected accumulated rewards until reaching a target state briefly called maximal conditional expectations in finite-state Markov decision processes where the condition is given as a reachability constraint. Conditional expectations of this type can, e.g., stand for the maximal expected termination time of probabilistic programs with non-determinism, under the condition that the program eventually terminates, or for the worst-case expected penalty to be paid, assuming that at least three deadlines are missed. The main results of the paper are i a polynomial-time algorithm to check the finiteness of maximal conditional expectations, ii PSPACE-completeness for the threshold problem in acyclic Markov decision processes where the task is to check whether the maximal conditional expectation exceeds a given threshold, iii a pseudo-polynomial-time algorithm for the threshold problem in the general cyclic case, and iv an exponential-time algorithm for computing the maximal conditional expectation and an optimal scheduler.


title: Rigorous Simulation-Based Analysis of Linear Hybrid Systems

authors:
Stanley Bak
Parasara Sridhar Duggirala


title: Congruence Closure with Free Variables

authors:
Haniel Barbosa
Pascal Fontaine
Andrew Reynolds


title: Almost Event-Rate Independent Monitoring of Metric Temporal Logic

authors:
David A. Basin
Bhargav Nagaraja Bhatt
Dmitriy Traytel


title: Software Verification with Validation of Results - (Report on SV-COMP 2017)


title: RPP: Automatic Proof of Relational Properties by Self-composition

authors:
Lionel Blatter
Nikolai Kosmatov
Pascale Le Gall
Virgile Prevosto


title: Counterexample-Guided Refinement of Template Polyhedra

authors:
Sergiy Bogomolov
Goran Frehse
Mirco Giacobbe
Thomas A. Henzinger


title: Up-To Techniques for Weighted Systems

authors:
Filippo Bonchi
Barbara König
Sebastian Küpper


title: Proving Termination Through Conditional Termination

authors:
Cristina Borralleras
Marc Brockschmidt
Daniel Larraz
Albert Oliveras
Enric Rodríguez-Carbonell
Albert Rubio

abstract: We present a constraint-based method for proving conditional termination of integer programs. Building on this, we construct a framework to prove (unconditional) program termination using a powerful mechanism to combine conditional termination proofs. Our key insight is that a conditional termination proof shows termination for a subset of program execution states which do not need to be considered in the remaining analysis. This facilitates more effective termination as well as non-termination analyses, and allows handling loops with different execution phases naturally. Moreover, our method can deal with sequences of loops compositionally. In an empirical evaluation, we show that our implementation VeryMax outperforms state-of-the-art tools on a range of standard benchmarks.


title: Rewriting-Based Runtime Verification for Alternation-Free HyperLTL

authors:
Noel Brett
Umair Siddique
Borzoo Bonakdarpour


title: JANI: Quantitative Model and Tool Interaction

authors:
Carlos E. Budde
Christian Dehnert
Ernst Moritz Hahn
Arnd Hartmanns
Sebastian Junges
Andrea Turrini


title: Long-Run Rewards for Markov Automata

authors:
Yuliya Butkova
Ralf Wimmer
Holger Hermanns


title: ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations

authors:
Luca Cardelli
Mirco Tribastone
Max Tschaikowski
Andrea Vandin


title: Skink: Static Analysis of Programs in LLVM Intermediate Representation - (Competition Contribution)

authors:
Franck Cassez
Anthony M. Sloane
Matthew Roberts
Matthew Pigram
Pongsak Suvanpong
Pablo González de Aledo Marugán


title: Interpolation-Based GR(1) Assumptions Refinement

authors:
Davide G. Cavezza
Dalal Alrajeh

abstract: This paper considers the problem of assumptions refinement in the context of unrealizable specifications for reactive systems. We propose a new counterstrategy-guided synthesis approach for GR(1) specifications based on Craig’s interpolants. Our interpolation-based method identifies causes for unrealizability and computes assumptions that directly target unrealizable cores, without the need for user input. Thereby, we discuss how this property reduces the maximum number of steps needed to converge to realizability compared with other techniques. We describe properties of interpolants that yield helpful GR(1) assumptions and prove the soundness of the results. Finally, we demonstrate that our approach yields weaker assumptions than baseline techniques.


title: Symbiotic 4: Beyond Reachability - (Competition Contribution)

authors:
Marek Chalupa
Martina Vitovská
Martin Jonás
Jiri Slaby
Jan Strejcek


title: Directed Automated Memory Performance Testing


title: autoCode4: Structural Controller Synthesis

authors:
Chih-Hong Cheng
Edward A. Lee
Harald Ruess


title: VeriAbs: Verification by Abstraction (Competition Contribution)

authors:
Bharti Chimdyalwar
Priyanka Darke
Avriti Chauhan
Punit Shah
Shrawan Kumar
R. Venkatesh


title: Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF

authors:
Alessandro Cimatti
Alberto Griggio
Ahmed Irfan
Marco Roveri
Roberto Sebastiani

abstract: Model checking invariant properties of designs, represented as transition systems, with non-linear real arithmetic (NRA), is an important though very hard problem. On the one hand NRA is a hard-to-solve theory; on the other hand most of the powerful model checking techniques lack support for NRA. In this paper, we present a counterexample-guided abstraction refinement (CEGAR) approach that leverages linearization techniques from differential calculus to enable the use of mature and efficient model checking algorithms for transition systems on linear real arithmetic (LRA) with uninterpreted functions (EUF). The results of an empirical evaluation confirm the validity and potential of this approach.


title: Precise Widening Operators for Proving Termination by Abstract Interpretation

authors:
Nathanaël Courant
Caterina Urban


title: Efficient Certified Resolution Proof Checking

authors:
Luís Cruz-Filipe
João Marques-Silva
Peter Schneider-Kamp

abstract: We present a novel propositional proof tracing format that eliminates complex processing, thus enabling efficient (formal) proof checking. The benefits of this format are demonstrated by implementing a proof checker in C, which outperforms a state-of-the-art checker by two orders of magnitude. We then formalize the theory underlying propositional proof checking in Coq, and extract a correct-by-construction proof checker for our format from the formalization. An empirical evaluation using 280 unsatisfiable instances from the 2015 and 2016 SAT competitions shows that this certified checker usually performs comparably to a state-of-the-art non-certified proof checker. Using this format, we formally verify the recent 200 TB proof of the Boolean Pythagorean Triples conjecture.


title: Sequential Convex Programming for the Efficient Verification of Parametric MDPs

authors:
Murat Cubuktepe
Nils Jansen
Sebastian Junges
Joost-Pieter Katoen
Ivan Papusha
Hasan A. Poonawala
Ufuk Topcu

abstract: Multi-objective verification problems of parametric Markov decision processes under optimality criteria can be naturally expressed as nonlinear programs. We observe that many of these computationally demanding problems belong to the subclass of signomial programs. This insight allows for a sequential optimization algorithm to efficiently compute sound but possibly suboptimal solutions. Each stage of this algorithm solves a geometric programming problem. These geometric programs are obtained by convexifying the nonconvex constraints of the original problem. Direct applications of the encodings as nonlinear programs are model repair and parameter synthesis. We demonstrate the scalability and quality of our approach by well-known benchmarks.


title: Forward Bisimulations for Nondeterministic Symbolic Finite Automata

authors:
Loris D'Antoni
Margus Veanes


title: ML for ML: Learning Cost Semantics by Experiment

authors:
Ankush Das
Jan Hoffmann


title: Learning Symbolic Automata

authors:
Samuel Drews
Loris D'Antoni


title: From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata

authors:
Javier Esparza
Jan Kretínský
Jean-François Raskin
Salomon Sickert

abstract: Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL objective into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size of the DPA, which often grows very fast in practice, and can reach double exponential size in the length of the LTL formula. In this paper we describe a single exponential translation from limit-deterministic Buchi automata (LDBA) to DPA, and show that it can be concatenated with a recent efficient translation from LTL to LDBA to yield a double exponential, “Safraless” LTL-to-DPA construction. We also report on an implementation, a comparison with the SPOT library, and performance on several sets of formulas, including instances from the 2016 SyntComp competition.


title: Encodings of Bounded Synthesis

authors:
Peter Faymonville
Bernd Finkbeiner
Markus N. Rabe
Leander Tentrup

abstract: The reactive synthesis problem is to compute a system satisfying a given specification in temporal logic. Bounded synthesis is the approach to bound the maximum size of the system that we accept as a solution to the reactive synthesis problem. As a result, bounded synthesis is decidable whenever the corresponding verification problem is decidable, and can be applied in settings where classic synthesis fails, such as in the synthesis of distributed systems. In this paper, we study the constraint solving problem behind bounded synthesis. We consider different reductions of the bounded synthesis problem of linear-time temporal logic (LTL) to constraint systems given as boolean formulas (SAT), quantified boolean formulas (QBF), and dependency quantified boolean formulas (DQBF). The reductions represent different trade-offs between conciseness and algorithmic efficiency. In the SAT encoding, both inputs and states of the system are represented explicitly; in QBF, inputs are symbolic and states are explicit; in DQBF, both inputs and states are symbolic. We evaluate the encodings systematically using benchmarks from the reactive synthesis competition (SYNTCOMP) and state-of-the-art solvers. Our key, and perhaps surprising, empirical finding is that QBF clearly dominates both SAT and DQBF.


title: Bounded Quantifier Instantiation for Checking Inductive Invariants

authors:
Yotam M. Y. Feldman
Oded Padon
Neil Immerman
Mooly Sagiv
Sharon Shoham


title: Lazy Automata Techniques for WS1S

authors:
Tomás Fiedor
Lukás Holík
Petr Janku
Ondrej Lengál
Tomás Vojnar

abstract: We present a new decision procedure for the logic WS1S. It originates from the classical approach, which first builds an automaton accepting all models of a formula and then tests whether its language is empty. The main novelty is to test the emptiness on the fly, while constructing a symbolic, term-based representation of the automaton, and prune the constructed state space from parts irrelevant to the test. The pruning is done by a generalization of two techniques used in antichain-based language inclusion and universality checking of finite automata: subsumption and early termination. The richer structure of the WS1S decision problem allows us, however, to elaborate on these techniques in novel ways. Our experiments show that the proposed approach can in many cases significantly outperform the classical decision procedure (implemented in the Mona tool) as well as recently proposed alternatives.


title: Ultimate Taipan: Trace Abstraction and Abstract Interpretation - (Competition Contribution)

authors:
Marius Greitschus
Daniel Dietsch
Matthias Heizmann
Alexander Nutz
Claus Schätzle
Christian Schilling
Frank Schüssele
Andreas Podelski


title: Ultimate Automizer with an On-Demand Construction of Floyd-Hoare Automata - (Competition Contribution)

authors:
Matthias Heizmann
Yu-Wen Chen
Daniel Dietsch
Marius Greitschus
Alexander Nutz
Betim Musa
Claus Schätzle
Christian Schilling
Frank Schüssele
Andreas Podelski


title: Minimization of Visibly Pushdown Automata Using Partial Max-SAT

authors:
Matthias Heizmann
Christian Schilling
Daniel Tischner

abstract: We consider the problem of state-space reduction for nondeterministic weakly-hierarchical visibly pushdown automata (Vpa). Vpa recognize a robust and algorithmically tractable fragment of context-free languages that is natural for modeling programs.


title: AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs - (Competition Contribution)

authors:
Jera Hensel
Frank Emrich
Florian Frohn
Thomas Ströder
Jürgen Giesl


title: Forester: From Heap Shapes to Automata Predicates - (Competition Contribution)

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


title: Synthesis of Recursive ADT Transformations from Reusable Templates

authors:
Jeevana Priya Inala
Nadia Polikarpova
Xiaokang Qiu
Benjamin S. Lerner
Armando Solar-Lezama

abstract: Recent work has proposed a promising approach to improving scalability of program synthesis by allowing the user to supply a syntactic template that constrains the space of potential programs. Unfortunately, creating templates often requires nontrivial effort from the user, which impedes the usability of the synthesizer. We present a solution to this problem in the context of recursive transformations on algebraic data-types. Our approach relies on polymorphic synthesis constructs: a small but powerful extension to the language of syntactic templates, which makes it possible to define a program space in a concise and highly reusable manner, while at the same time retains the scalability benefits of conventional templates. This approach enables end-users to reuse predefined templates from a library for a wide variety of problems with little effort. The paper also describes a novel optimization that further improves the performance and the scalability of the system. We evaluated the approach on a set of benchmarks that most notably includes desugaring functions for lambda calculus, which force the synthesizer to discover Church encodings for pairs and boolean operations.


title: Optimal Translation of LTL to Limit Deterministic Automata

authors:
Dileep Kini
Mahesh Viswanathan


title: Index Appearance Record for Transforming Rabin Automata into Parity Automata

authors:
Jan Kretínský
Tobias Meggendorfer
Clara Waldmann
Maximilian Weininger

abstract: Transforming deterministic \(\omega \)-automata into deterministic parity automata is traditionally done using variants of appearance records. We present a more efficient variant of this approach, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and find out that our method produces smaller automata than previous approaches. Moreover, the experiments demonstrate the potential of our method for LTL synthesis, using LTL-to-Rabin translators. It leads to significantly smaller parity automata when compared to state-of-the-art approaches on complex formulae.


title: Hierarchical Network Formation Games

authors:
Orna Kupferman
Tami Tamir


title: Validation, Synthesis and Optimization for Cyber-Physical Systems


title: FlyFast: A Mean Field Model Checker

authors:
Diego Latella
Michele Loreti
Mieke Massink


title: HipTNT+: A Termination and Non-termination Analyzer by Second-Order Abduction - (Competition Contribution)

authors:
Ton Chanh Le
Quang-Trung Ta
Wei-Ngan Chin


title: Fair Termination for Parameterized Probabilistic Concurrent Systems

authors:
Ondrej Lengál
Anthony Widjaja Lin
Rupak Majumdar
Philipp Rümmer

abstract: We consider the problem of automatically verifying that a parameterized family of probabilistic concurrent systems terminates with probability one for all instances against adversarial schedulers. A parameterized family defines an infinite-state system: for each number n, the family consists of an instance with n finite-state processes. In contrast to safety, the parameterized verification of liveness is currently still considered extremely challenging especially in the presence of probabilities in the model. One major challenge is to provide a sufficiently powerful symbolic framework. One well-known symbolic framework for the parameterized verification of non-probabilistic concurrent systems is regular model checking. Although the framework was recently extended to probabilistic systems, incorporating fairness in the framework—often crucial for verifying termination—has been especially difficult due to the presence of an infinite number of fairness constraints (one for each process). Our main contribution is a systematic, regularity-preserving, encoding of finitary fairness (a realistic notion of fairness proposed by Alur and Henzinger) in the framework of regular model checking for probabilistic parameterized systems. Our encoding reduces termination with finitary fairness to verifying parameterized termination without fairness over probabilistic systems in regular model checking (for which a verification framework already exists). We show that our algorithm could verify termination for many interesting examples from distributed algorithms (Herman’s protocol) and evolutionary biology (Moran process, cell cycle switch), which do not hold under the standard notion of fairness. To the best of our knowledge, our algorithm is the first fully-automatic method that can prove termination for these examples.


title: A Novel Learning Algorithm for Büchi Automata Based on Family of DFAs and Classification Trees

authors:
Yong Li
Yu-Fang Chen
Lijun Zhang
Depeng Liu

abstract: In this paper, we propose a novel algorithm to learn a Buchi automaton from a teacher who knows an \(\omega \)-regular language. The algorithm is based on learning a formalism named family of DFAs (FDFAs) recently proposed by Angluin and Fisman [10]. The main catch is that we use a classification tree structure instead of the standard observation table structure. The worst case storage space required by our algorithm is quadratically better than the table-based algorithm proposed in [10]. We implement the first publicly available library ROLL (Regular Omega Language Learning), which consists of all \(\omega \)-regular learning algorithms available in the literature and the new algorithms proposed in this paper. Experimental results show that our tree-based algorithms have the best performance among others regarding the number of solved learning tasks.


title: ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans

authors:
Anna Lukina
Lukas Esterle
Christian Hirsch
Ezio Bartocci
Junxing Yang
Ashish Tiwari
Scott A. Smolka
Radu Grosu

abstract: We introduce ARES, an efficient approximation algorithm for generating optimal plans action sequences that take an initial state of a Markov Decision Process MDP to a state whose cost is below a specified convergence threshold. ARES uses Particle Swarm Optimization, with adaptive sizing for both the receding horizon and the particle swarm. Inspired by Importance Splitting, the length of the horizon and the number of particles are chosen such that at least one particle reaches a next-level state, that is, a state where the cost decreases by a required delta from the previous-level state. The level relation on states and the plans constructed by ARES implicitly define a Lyapunov function and an optimal policy, respectively, both of which could be explicitly generated by applying ARES to all states of the MDP, up to some topological equivalence relation. We also assess the effectiveness of ARES by statistically evaluating its rate of success in generating optimal plans. The ARES algorithm resulted from our desire to clarify if flying in V-formation is a flocking policy that optimizes energy conservation, clear view, and velocity alignment. That is, we were interested to see if one could find optimal plans that bring a flock from an arbitrary initial state to a state exhibiting a single connected V-formation. For flocks with 7 birds, ARES is able to generate a plan that leads to a V-formation in 95% of the 8,000 random initial configurations within 63i¾?s, on average. ARES can also be easily customized into a model-predictive controller MPC with an adaptive receding horizon and statistical guarantees of convergence. To the best of our knowledge, our adaptive-sizing approach is the first to provide convergence guarantees in receding-horizon techniques.


title: Optimizing and Caching SMT Queries in SymDIVINE - (Competition Contribution)

authors:
Jan Mrázek
Martin Jonás
Vladimír Still
Henrich Lauko
Jiri Barnat


title: Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation - (Competition Contribution)

authors:
Truc L. Nguyen
Omar Inverso
Bernd Fischer
Salvatore La Torre
Gennaro Parlato


title: Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation

authors:
ThanhVu Nguyen
Westley Weimer
Deepak Kapur
Stephanie Forrest

abstract: We prove that certain formulations of program synthesis and reachability are equivalent. Specifically, our constructive proof shows the reductions between the template-based synthesis problem, which generates a program in a pre-specified form, and the reachability problem, which decides the reachability of a program location. This establishes a link between the two research fields and allows for the transfer of techniques and results between them.


title: Automatic Verification of Finite Precision Implementations of Linear Controllers

authors:
Junkil Park
Miroslav Pajic
Oleg Sokolsky
Insup Lee


title: Counterexample-Guided Model Synthesis

authors:
Mathias Preiner
Aina Niemetz
Armin Biere


title: DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs - (Competition Contribution)

authors:
Williame Rocha
Herbert Rocha
Hussama Ismail
Lucas C. Cordeiro
Bernd Fischer


title: HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-linear Hybrid Automata

authors:
Nima Roohi
Pavithra Prabhakar
Mahesh Viswanathan


title: CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs

authors:
David Sanán
Yongwang Zhao
Zhe Hou
Fuyuan Zhang
Alwen Tiu
Yang Liu


title: An Abstraction Technique for Parameterized Model Checking of Leader Election Protocols: Application to FTSP

authors:
Ocan Sankur
Jean-Pierre Talpin


title: On Optimization Modulo Theories, MaxSMT and Sorting Networks

authors:
Roberto Sebastiani
Patrick Trentin

abstract:
Optimization Modulo Theories $$\text {OMT}$$ is an extension of SMT which allows for finding models that optimize given objectives. Partial weighted MaxSMT---or equivalently $$\text {OMT}$$ with Pseudo-Boolean objective functions, $$\text {OMT+PB}$$ --- is a very-relevant strict subcase of $$\text {OMT}$$. We classify existing approaches for MaxSMT or $$\text {OMT+PB}$$ in two groups: MaxSAT-based approaches exploit the efficiency of state-of-the-art MaxSAT solvers, but they are specific-purpose and not always applicable; OMT-based approaches are general-purpose, but they suffer from intrinsic inefficiencies on MaxSMT/$$\text {OMT+PB}$$ problems.

We identify a major source of such inefficiencies, and we address it by enhancing $$\text {OMT}$$ by means of bidirectional sorting networks. We implemented this idea on top of the OptiMathSAT $$\text {OMT}$$ solver. We run an extensive empirical evaluation on a variety of problems, comparing MaxSAT-based and $$\text {OMT}$$-based techniques, with and without sorting networks, implemented on top of OptiMathSAT and [InlineEquation not available: see fulltext.]. The results support the effectiveness of this idea, and provide interesting insights about the different approaches.


title: Discriminating Traces with Time

authors:
Saeid Tizpaz-Niari
Pavol Cerný
Bor-Yuh Evan Chang
Sriram Sankaranarayanan
Ashutosh Trivedi

abstract: What properties about the internals of a program explain the possible differences in its overall running time for different inputs? In this paper, we propose a formal framework for considering this question we dub trace-set discrimination. We show that even though the algorithmic problem of computing maximum likelihood discriminants is NP-hard, approaches based on integer linear programming ILP and decision tree learning can be useful in zeroing-in on the program internals. On a set of Java benchmarks, we find that compactly-represented decision trees scalably discriminate with high accuracy--more scalably than maximum likelihood discriminants and with comparable accuracy. We demonstrate on three larger case studies how decision-tree discriminants produced by our tool are useful for debugging timing side-channel vulnerabilities i.e., where a malicious observer infers secrets simply from passively watching execution times and availability vulnerabilities.


title: HQSpre - An Effective Preprocessor for QBF and DQBF

authors:
Ralf Wimmer
Sven Reimer
Paolo Marin
Bernd Becker


title: Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions

authors:
Valentin Wüstholz
Oswaldo Olivo
Marijn J. H. Heule
Isil Dillig

abstract: In an algorithmic complexity attack, a malicious party takes advantage of the worst-case behavior of an algorithm to cause denial-of-service. A prominent algorithmic complexity attack is regular expression denial-of-service (ReDoS), in which the attacker exploits a vulnerable regular expression by providing a carefully-crafted input string that triggers worst-case behavior of the matching algorithm. This paper proposes a technique for automatically finding ReDoS vulnerabilities in programs. Specifically, our approach automatically identifies vulnerable regular expressions in the program and determines whether an "evil" input string can be matched against a vulnerable regular expression. We have implemented our proposed approach in a tool called REXPLOITER and found 41 exploitable security vulnerabilities in Java web applications.


title: CPA-BAM-Slicing: Block-Abstraction Memoization and Slicing with Region-Based Dependency Analysis - (Competition Contribution)

authors:
Pavel S. Andrianov
Vadim S. Mutilin
Mikhail U. Mandrykin
Anton A. Vasilyev


title: Optimal Dynamic Partial Order Reduction with Observers

authors:
Stavros Aronis
Bengt Jonsson
Magnus Lång
Konstantinos Sagonas


title: Parameterized Verification of Synchronization in Constrained Reconfigurable Broadcast Networks

authors:
A. R. Balasubramanian
Nathalie Bertrand
Nicolas Markey

abstract:
Reconfigurable broadcast networks provide a convenient formalism for modelling and reasoning about networks of mobile agents broadcasting messages to other agents following some (evolving) communication topology. The parameterized verification of such models aims at checking whether a given property holds irrespective of the initial configuration (number of agents, initial states and initial communication topology). We focus here on the synchronization property, asking whether all agents converge to a set of target states after some execution. This problem is known to be decidable in polynomial time when no constraints are imposed on the evolution of the communication topology (while it is undecidable for static broadcast networks).
In this paper we investigate how various constraints on reconfigurations affect the decidability and complexity of the synchronization problem. In particular, we show that when bounding the number of reconfigured links between two communications steps by a constant, synchronization becomes undecidable; on the other hand, synchronization remains decidable in PTIME when the bound grows with the number of agents.


title: Automatic Generation of Precise and Useful Commutativity Conditions

authors:
Kshitij Bansal
Eric Koskinen
Omer Tripp

abstract:
Reasoning about commutativity between data-structure operations is an important problem with applications including parallelizing compilers, optimistic parallelization and, more recently, Ethereum smart contracts. There have been research results on automatic generation of commutativity conditions, yet we are unaware of any fully automated technique to generate conditions that are both sound and effective.
We have designed such a technique, driven by an algorithm that iteratively refines a conservative approximation of the commutativity (and non-commutativity) condition for a pair of methods into an increasingly precise version. The algorithm terminates if/when the entire state space has been considered, and can be aborted at any time to obtain a partial yet sound commutativity condition. We have generalized our work to left-/right-movers and proved relative completeness. We describe aspects of our technique that lead to useful commutativity conditions, including how predicates are selected during refinement and heuristics that impact the output shape of the condition.
We have implemented our technique in a prototype open-source tool Servois. Our algorithm produces quantifier-free queries that are dispatched to a back-end SMT solver. We evaluate Servois through two case studies: (i) We synthesize commutativity conditions for a range of data structures including Set, HashTable, Accumulator, Counter, and Stack. (ii) We consider an Ethereum smart contract called BlockKing, and show that Servois can detect serious concurrency-related vulnerabilities and guide developers to construct robust and efficient implementations.


title: Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models

authors:
Luca Bortolussi
Simone Silvetti

abstract: Parameterized verification of temporal properties is an active research area, being extremely relevant for model-based design of complex systems. In this paper, we focus on parameter synthesis for stochastic models, looking for regions of the parameter space where the model satisfies a linear time specification with probability greater (or less) than a given threshold. We propose a statistical approach relying on simulation and leveraging a machine learning method based on Gaussian Processes for statistical parametric verification, namely Smoothed Model Checking. By injecting active learning ideas, we obtain an efficient synthesis routine which is able to identify the target regions with statistical guarantees. Our approach, which is implemented in Python, scales better than existing ones with respect to state space of the model and number of parameters. It is applicable to linear time specifications with time constraints and to more complex stochastic models than Markov Chains.


title: Strategy Representation by Decision Trees in Reactive Synthesis

authors:
Tomás Brázdil
Krishnendu Chatterjee
Jan Kretínský
Viktor Toman

abstract: Graph games played by two players over finite-state graphs are central in many problems in computer science. In particular, graph games with \omega-regular winning conditions, specified as parity objectives, which can express properties such as safety, liveness, fairness, are the basic framework for verification and synthesis of reactive systems. The decisions for a player at various states of the graph game are represented as strategies. While the algorithmic problem for solving graph games with parity objectives has been widely studied, the most prominent data-structure for strategy representation in graph games has been binary decision diagrams (BDDs). However, due to the bit-level representation, BDDs do not retain the inherent flavor of the decisions of strategies, and are notoriously hard to minimize to obtain succinct representation. In this work we propose decision trees for strategy representation in graph games. Decision trees retain the flavor of decisions of strategies and allow entropy-based minimization to obtain succinct trees. However, decision trees work in settings (e.g., probabilistic models) where errors are allowed, and overfitting of data is typically avoided. In contrast, for strategies in graph games no error is allowed, and the decision tree must represent the entire strategy. We develop new techniques to extend decision trees to overcome the above obstacles, while retaining the entropy-based techniques to obtain succinct trees. We have implemented our techniques to extend the existing decision tree solvers. We present experimental results for problems in reactive synthesis to show that decision trees provide a much more efficient data-structure for strategy representation as compared to BDDs.


title: Chain Reduction for Binary and Zero-Suppressed Decision Diagrams


title: A Statistical Model Checker for Nondeterminism and Rare Events

authors:
Carlos E. Budde
Pedro R. D'Argenio
Arnd Hartmanns
Sean Sedwards


title: A Verified Implementation of the Bounded List Container

authors:
Raphaël Cauderlier
Mihaela Sighireanu

abstract: This paper contributes to the trend of providing fully verified container libraries. We consider an implementation of the bounded doubly linked list container which manages the list in a fixed size, heap allocated array. The container provides constant time methods to update the list by adding, deleting, and changing elements, as well as cursors for list traversal and access to elements. The library is implemented in C, but we wrote the code and its specification by imitating the ones provided by GNAT for the standard library of Ada 2012. The proof of functional correctness is done using VeriFast, which provides an auto-active verification environment for Separation Logic extended with algebraic data types. The specifications proved entail the contracts of the Ada library and include new features. The verification method we used employs a precise algebraic model of the data structure and we show that it facilitates the verification and captures entirely the library contracts. This case study may be of interest for other verification platforms, thus we highlight the intricate points of its proof.


title: Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection

authors:
Milan Ceska
Vojtech Havlena
Lukás Holík
Ondrej Lengál
Tomás Vojnar


title: SYMBIOTIC 5: Boosted Instrumentation - (Competition Contribution)

authors:
Marek Chalupa
Martina Vitovská
Jan Strejcek


title: ICE-Based Refinement Type Discovery for Higher-Order Functional Programs

authors:
Adrien Champion
Tomoya Chiba
Naoki Kobayashi
Ryosuke Sato

abstract: We propose a method for automatically finding refinement types of higher-order function programs. Our method is an extension of the Ice framework of Garg et al. for finding invariants. In addition to the usual positive and negative samples in machine learning, their Ice framework uses implication constraints, which consist of pairs (x, y) such that if x satisfies an invariant, so does y. From these constraints, Ice infers inductive invariants effectively. We observe that the implication constraints in the original Ice framework are not suitable for finding invariants of recursive functions with multiple function calls. We thus generalize the implication constraints to those of the form $$(\{x_1,\dots ,x_k\}, y)$$ , which means that if all of $$x_1,\dots ,x_k$$ satisfy an invariant, so does y. We extend their algorithms for inferring likely invariants from samples, verifying the inferred invariants, and generating new samples. We have implemented our method and confirmed its effectiveness through experiments.


title: Fine-Grained Complexity of Safety Verification

authors:
Peter Chini
Roland Meyer
Prakash Saivasan


title: From Natural Projection to Partial Model Checking and Back

authors:
Gabriele Costa
David A. Basin
Chiara Bodei
Pierpaolo Degano
Letterio Galletta

abstract: Specification decomposition is a theoretically interesting and practically relevant problem for which two approaches were independently developed by the control theory and verification communities: natural projection and partial model checking. In this paper we show that, under reasonable assumptions, natural projection reduces to partial model checking and, when cast in a common setting, the two are equivalent. Aside from their theoretical interest, our results build a bridge whereby the control theory community can reuse algorithms and results developed by the verification community. In addition, we present an algorithm and a tool for the partial model checking of finite-state automata that can be used as an alternative to natural projection.


title: VeriAbs: Verification by Abstraction and Test Generation - (Competition Contribution)

authors:
Priyanka Darke
Sumanth Prabhu
Bharti Chimdyalwar
Avriti Chauhan
Shrawan Kumar
Animesh Basak Chowdhury
R. Venkatesh
Advaita Datar
Raveendra Kumar Medicherla


title: Daisy - Framework for Analysis and Optimization of Numerical Programs (Tool Paper)

authors:
Eva Darulova
Anastasiia Izycheva
Fariha Nasir
Fabian Ritter
Heiko Becker
Robert Bastian


title: Ultimate Taipan with Dynamic Block Encoding - (Competition Contribution)

authors:
Daniel Dietsch
Marius Greitschus
Matthias Heizmann
Jochen Hoenicke
Alexander Nutz
Andreas Podelski
Christian Schilling
Tanja Schindler

abstract: Ultimate Taipan is a software model checker that uses trace abstraction and abstract interpretation to prove correctness of programs. In contrast to previous versions, Ultimate Taipan now uses dynamic block encoding to obtain the best precision possible when evaluating transition formulas of large block encoded programs.


title: Oink: An Implementation and Evaluation of Modern Parity Game Solvers

abstract: Parity games have important practical applications in formal verification and synthesis, especially to solve the model-checking problem of the modal mu-calculus. They are also interesting from the theory perspective, as they are widely believed to admit a polynomial solution, but so far no such algorithm is known. In recent years, a number of new algorithms and improvements to existing algorithms have been proposed. We implement a new and easy to extend tool Oink, which is a high-performance implementation of modern parity game algorithms. We further present a comprehensive empirical evaluation of modern parity game algorithms and solvers, both on real world benchmarks and randomly generated games. Our experiments show that our new tool Oink outperforms the current state-of-the art.


title: The Refinement Calculus of Reactive Systems Toolset

authors:
Iulia Dragomir
Viorel Preoteasa
Stavros Tripakis


title: InterpChecker: Reducing State Space via Interpolations - (Competition Contribution)

authors:
Zhao Duan
Cong Tian
Zhenhua Duan
C.-H. Luke Ong


title: More Scalable LTL Model Checking via Discovering Design-Space Dependencies ( D^3 D 3 )

authors:
Rohit Dureja
Kristin Yvonne Rozier

abstract: Modern system design often requires comparing several models over a large design space. Different models arise out of a need to weigh different design choices, to check core capabilities of versions with varying features, or to analyze a future version against previous ones. Model checking can compare different models; however, applying model checking off-the-shelf may not scale due to the large size of the design space for today’s complex systems. We exploit relationships between different models of the same (or related) systems to optimize the model-checking search. Our algorithm, \(D^{3}\), preprocesses the design space and checks fewer model-checking instances, e.g., using nuXmv. It automatically prunes the search space by reducing both the number of models to check, and the number of LTL properties that need to be checked for each model in order to provide the complete model-checking verdict for every individual model-property pair. We formalize heuristics that improve the performance of \(D^{3}\). We demonstrate the scalability of \(D^{3}\) by extensive experimental evaluation, e.g., by checking 1,620 real-life models for NASA’s NextGen air traffic control system. Compared to checking each model-property pair individually, \(D^{3}\) is up to 9.4\(\times \) faster.


title: Accelerating Syntax-Guided Invariant Synthesis

authors:
Grigory Fedyukovich
Rastislav Bodík

abstract: We present a fast algorithm for syntax-guided synthesis of inductive invariants which combines enumerative learning with inductive-subset extraction, leverages counterexamples-to-induction and interpolation-based bounded proofs. It is a variant of a recently proposed probabilistic method, called FreqHorn, which is however less dependent on heuristics than its predecessor. We present an evaluation of the new algorithm on a large set of benchmarks and show that it exhibits a more predictable behavior than its predecessor, and it is competitive to the state-of-the-art invariant synthesizers based on Property Directed Reachability.


title: RVHyper: A Runtime Verification Tool for Temporal Hyperproperties

authors:
Bernd Finkbeiner
Christopher Hahn
Marvin Stenger
Leander Tentrup

abstract: We present \(\text {RVHyper}\), a runtime verification tool for hyperproperties. Hyperproperties, such as non-interference and observational determinism, relate multiple computation traces with each other. Specifications are given as formulas in the temporal logic \(\text {HyperLTL}\), which extends linear-time temporal logic (LTL) with trace quantifiers and trace variables. \(\text {RVHyper}\) processes execution traces sequentially until a violation of the specification is detected. In this case, a counter example, in the form of a set of traces, is returned. As an example application, we show how \(\text {RVHyper}\) can be used to detect spurious dependencies in hardware designs.


title: Multi-cost Bounded Reachability in MDP

authors:
Arnd Hartmanns
Sebastian Junges
Joost-Pieter Katoen
Tim Quatmann


title: Hoare Logics for Time Bounds - A Study in Meta Theory

authors:
Maximilian P. L. Haslbeck
Tobias Nipkow

abstract: We study three different Hoare logics for reasoning about time bounds of imperative programs and formalize them in Isabelle/HOL: a classical Hoare like logic due to Nielson, a logic with potentials due to Carbonneaux et al. and a separation logic following work by Atkey, Chaguerand and Pottier. These logics are formally shown to be sound and complete. Verification condition generators are developed and are shown sound and complete too. We also consider variants of the systems where we abstract from multiplicative constants in the running time bounds, thus supporting a big-O style of reasoning. Finally we compare the expressive power of the three systems.


title: Permutation Games for the Weakly Aconjunctive \mu μ -Calculus

authors:
Daniel Hausmann
Lutz Schröder
Hans-Peter Deifel

abstract: We introduce a natural notion of limit-deterministic parity automata and present a method that uses such automata to construct satisfiability games for the weakly aconjunctive fragment of the $$\mu $$ -calculus. To this end we devise a method that determinizes limit-deterministic parity automata of size n with k priorities through limit-deterministic Büchi automata to deterministic parity automata of size $$\mathcal {O}((nk)!)$$ and with $$\mathcal {O}(nk)$$ priorities. The construction relies on limit-determinism to avoid the full complexity of the Safra/Piterman-construction by using partial permutations of states in place of Safra-Trees. By showing that limit-deterministic parity automata can be used to recognize unsuccessful branches in pre-tableaux for the weakly aconjunctive $$\mu $$ -calculus, we obtain satisfiability games of size $$\mathcal {O}((nk)!)$$ with $$\mathcal {O}(nk)$$ priorities for weakly aconjunctive input formulas of size n and alternation-depth k. A prototypical implementation that employs a tableau-based global caching algorithm to solve these games on-the-fly shows promising initial results.


title: Ultimate Automizer and the Search for Perfect Interpolants - (Competition Contribution)

authors:
Matthias Heizmann
Yu-Fang Chen
Daniel Dietsch
Marius Greitschus
Jochen Hoenicke
Yong Li
Alexander Nutz
Betim Musa
Christian Schilling
Tanja Schindler
Andreas Podelski

abstract: Ultimate Automizer is a software verifier that generalizes proofs for traces to proofs for larger parts for the program. In recent years the portfolio of proof producers that are available to Ultimate has grown continuously. This is not only because more trace analysis algorithms have been implemented in Ultimate but also due to the continuous progress in the SMT community. In this paper we explain how Ultimate Automizer dynamically selects trace analysis algorithms and how the tool decides when proofs for traces are “good” enough for using them in the abstraction refinement.


title: What a Difference a Variable Makes

authors:
Marijn J. H. Heule
Armin Biere


title: Abstraction Refinement for Emptiness Checking of Alternating Data Automata

authors:
Radu Iosif
Xiao Xu


title: Generation of Minimum Tree-Like Witnesses for Existential CTL

authors:
Chuan Jiang
Gianfranco Ciardo

abstract: An advantage of model checking is its ability to generate witnesses or counterexamples. Approaches exist to generate small or minimum witnesses for simple unnested formulas, but no existing method guarantees minimality for general nested ones. Here, we give a definition of witness size, use edge-valued decision diagrams to recursively compute the minimum witness size for each subformula, and describe a general approach to build minimum tree-like witnesses for existential CTL. Experimental results show that for some models, our approach is able to generate minimum witnesses while the traditional approach is not.


title: Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts

authors:
Andreas Katis
Grigory Fedyukovich
Huajun Guo
Andrew Gacek
John Backes
Arie Gurfinkel
Michael W. Whalen

abstract: Automated synthesis of reactive systems from specifications has been a topic of research for decades. Recently, a variety of approaches have been proposed to extend synthesis of reactive systems from proposi- tional specifications towards specifications over rich theories. We propose a novel, completely automated approach to program synthesis which reduces the problem to deciding the validity of a set of forall-exists formulas. In spirit of IC3 / PDR, our problem space is recursively refined by blocking out regions of unsafe states, aiming to discover a fixpoint that describes safe reactions. If such a fixpoint is found, we construct a witness that is directly translated into an implementation. We implemented the algorithm on top of the JKind model checker, and exercised it against contracts written using the Lustre specification language. Experimental results show how the new algorithm outperforms JKinds already existing synthesis procedure based on k-induction and addresses soundness issues in the k-inductive approach with respect to unrealizable results.


title: Bit-Vector Model Counting Using Statistical Estimation

authors:
Seonmo Kim
Stephen McCamant

abstract: Approximate model counting for bit-vector SMT formulas (generalizing \#SAT) has many applications such as probabilistic inference and quantitative information-flow security, but it is computationally difficult. Adding random parity constraints (XOR streamlining) and then checking satisfiability is an effective approximation technique, but it requires a prior hypothesis about the model count to produce useful results. We propose an approach inspired by statistical estimation to continually refine a probabilistic estimate of the model count for a formula, so that each XOR-streamlined query yields as much information as possible. We implement this approach, with an approximate probability model, as a wrapper around an off-the-shelf SMT solver or SAT solver. Experimental results show that the implementation is faster than the most similar previous approaches which used simpler refinement strategies. The technique also lets us model count formulas over floating-point constraints, which we demonstrate with an application to a vulnerability in differential privacy mechanisms.


title: Property Checking Array Programs Using Loop Shrinking

authors:
Shrawan Kumar
Amitabha Sanyal
R. Venkatesh
Punit Shah

abstract: Most verification tools find it difficult to prove properties of programs containing loops that process arrays of large or unknown size. These methods either fail to abstract the array at the right granularity and are therefore limited in precision or scalability, or they attempt to synthesize an appropriate invariant that is quantified over the elements of the array, a task known to be difficult. In this paper, we present a different approach based on a notion called loop shrinkability, in which an array processing loop is transformed to a loop of much smaller bound that processes only a few non-deterministically chosen elements of the array. The result is a finite state program with a drastically reduced state space that can be analyzed by bounded model checkers. We show that the proposed transformation is an over-approximation, i.e. if the transformed program is correct, so is the original. In addition, when applicable, the method is impervious to the size or existence of the bound of the array. As an assessment of usefulness, we tested a tool based on our method on the ArraysReach category of SV-COMP 2017 benchmarks. After excluding programs with feature not handled by our tool, we could successfully verify 87 of the 93 remaining programs.


title: Frame Inference for Inductive Entailment Proofs in Separation Logic

authors:
Quang Loc Le
Jun Sun
Shengchao Qin


title: Geometric Nontermination Arguments

authors:
Jan Leike
Matthias Heizmann

abstract: We present a new kind of nontermination argument, called geometric nontermination argument. The geometric nontermination argument is a finite representation of an infinite execution that has the form of a sum of several geometric series. For so-called linear lasso programs we can decide the existence of a geometric nontermination argument using a nonlinear algebraic $\exists$-constraint. We show that a deterministic conjunctive loop program with nonnegative eigenvalues is nonterminating if an only if there exists a geometric nontermination argument. Furthermore, we present an evaluation that demonstrates that our method is feasible in practice.


title: 2LS: Memory Safety and Non-termination - (Competition Contribution)

authors:
Viktor Malík
Stefan Marticek
Peter Schrammel
Mandayam K. Srivas
Tomás Vojnar
Johanan Wahlang

abstract: 2LS is a C program analyser built upon the CPROVER infrastructure. 2LS is bit-precise and it can verify and refute program assertions and termination. 2LS implements template-based synthesis techniques, e.g. to find invariants and ranking functions, and incremental loop unwinding techniques to find counterexamples and k-induction proofs. New features in this year’s version are improved handling of heap-allocated data structures using a template domain for shape analysis and two approaches to prove program non-termination.


title: TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation

authors:
Lina Marsso
Radu Mateescu
Wendelin Serwe


title: EMME: A Formal Tool for ECMAScript Memory Model Evaluation

authors:
Cristian Mattarei
Clark W. Barrett
Shu-yu Guo
Bradley Nelson
Ben Smith

abstract: Nearly all web-based interfaces are written in JavaScript. Given its prevalence, the support for high performance JavaScript code is crucial. The ECMA Technical Committee 39 (TC39) has recently extended the ECMAScript language (i.e., JavaScript) to support shared memory accesses between different threads. The extension is given in terms of a natural language memory model specification. In this paper we describe a formal approach for validating both the memory model and its implementations in various JavaScript engines. We first introduce a formal version of the memory model and report results on checking the model for consistency and other properties. We then introduce our tool, EMME, built on top of the Alloy analyzer, which leverages the model to generate all possible valid executions of a given JavaScript program. Finally, we report results using EMME together with small test programs to analyze industrial JavaScript engines. We show that EMME can find bugs as well as missed opportunities for optimization.


title: Map2Check Using LLVM and KLEE - (Competition Contribution)

authors:
Rafael Menezes
Herbert Rocha
Lucas C. Cordeiro
Raimundo S. Barreto

abstract: Map2Check is a bug hunting tool that automatically checks safety properties in C programs. It tracks memory pointers and variable assignments to check user-specified assertions, overflow, and pointer safety. Here, we extend Map2Check to: (i) simplify the program using Clang/LLVM; (ii) perform a path-based symbolic execution using the KLEE tool; and (iii) transform and instrument the code using the LLVM dynamic information flow. The SVCOMP’18 results show that Map2Check can be effective in generating and checking test cases related to memory management of C programs.


title: CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving

authors:
Hakan Metin
Souheib Baarir
Maximilien Colange
Fabrice Kordon

abstract: SAT solvers are now widely used to solve a large variety of problems, including formal verification of systems. SAT problems derived from such applications often exhibit symmetry properties that could be exploited to speed up their solving. Static symmetry breaking is so far the most popular approach to take advantage of symmetries. It relies on a symmetry preprocessor which augments the initial problem with constraints that force the solver to consider only a few configurations among the many symmetric ones.


title: Computing the Concurrency Threshold of Sound Free-Choice Workflow Nets

authors:
Philipp J. Meyer
Javier Esparza
Hagen Völzer

abstract:
Workflow graphs extend classical flow charts with concurrent fork and join nodes. They constitute the core of business processing languages such as BPMN or UML Activity Diagrams. The activities of a workflow graph are executed by humans or machines, generically called resources. If concurrent activities cannot be executed in parallel by lack of resources, the time needed to execute the workflow increases. We study the problem of computing the minimal number of resources necessary to fully exploit the concurrency of a given workflow, and execute it as fast as possible (i.e., as fast as with unlimited resources).
We model this problem using free-choice Petri nets, which are known to be equivalent to workflow graphs. We analyze the computational complexity of two versions of the problem: computing the resource and concurrency thresholds. We use the results to design an algorithm to approximate the concurrency threshold, and evaluate it on a benchmark suite of 642 industrial examples. We show that it performs very well in practice: It always provides the exact value, and never takes more than 30 milliseconds for any workflow, even for those with a huge number of reachable markings.


title: Symmetry Reduction for the Local Mu-Calculus

authors:
Kedar S. Namjoshi
Richard J. Trefler

abstract: Model checking large networks of processes is challenging due to state explosion. In many cases, individual processes are isomorphic, but there is insufficient global symmetry to simplify model checking. This work considers the verification of local properties, those defined over the neighborhood of a process. Considerably generalizing earlier results on invariance, it is shown that all local mu-calculus properties, including safety and liveness properties, are preserved by neighborhood symmetries. Hence, it suffices to check them locally over a set of representative process neighborhoods. In general, local verification approximates verification over the global state space; however, if process interactions are outward-facing, the relationship is shown to be exact. For many network topologies, even those with little global symmetry, analysis with representatives provides a significant, even exponential, reduction in the cost of verification. Moreover, it is shown that for network families generated from building-block patterns, neighborhood symmetries are easily determined, and verification over the entire family reduces to verification over a finite set of representative process neighborhoods.


title: Invariant Synthesis for Incomplete Verification Engines

authors:
Daniel Neider
Pranav Garg
P. Madhusudan
Shambwaditya Saha
Daejun Park

abstract: We propose a framework for synthesizing inductive invariants for incomplete verification engines, which soundly reduce logical problems in undecidable theories to decidable theories. Our framework is based on the counter-example guided inductive synthesis principle (CEGIS) and allows verification engines to communicate non-provability information to guide invariant synthesis. We show precisely how the verification engine can compute such non-provability information and how to build effective learning algorithms when invariants are expressed as Boolean combinations of a fixed set of predicates. Moreover, we evaluate our framework in two verification settings, one in which verification engines need to handle quantified formulas and one in which verification engines have to reason about heap properties expressed in an expressive but undecidable separation logic. Our experiments show that our invariant synthesis framework based on non-provability information can both effectively synthesize inductive invariants and adequately strengthen contracts across a large suite of programs.


title: AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic

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


title: Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning

authors:
Giles Reger
Martin Suda
Andrei Voronkov


title: Revisiting Enumerative Instantiation

authors:
Andrew Reynolds
Haniel Barbosa
Pascal Fontaine


title: A Non-linear Arithmetic Procedure for Control-Command Software Verification

authors:
Pierre Roux
Mohamed Iguernlala
Sylvain Conchon


title: Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis

authors:
Stefan Schupp
Erika Ábrahám

abstract: To decide whether a set of states is reachable in a hybrid system, over-approximative symbolic successor computations can be used, where the symbolic representation of state sets as well as the successor computations have several parameters which determine the efficiency and the precision of the computations. Naturally, faster computations come with less precision and more spurious counterexamples. To remove a spurious counterexample, the only possibility offered by current tools is to reduce the error by re-starting the complete search with different parameters. In this paper we propose a CEGAR approach that takes as input a user-defined ordered list of search configurations, which are used to dynamically refine the search tree along potentially spurious counterexamples. Dedicated datastructures allow to extract as much useful information as possible from previous computations in order to reduce the refinement overhead.


title: Structurally Defined Conditional Data-Flow Static Analysis

authors:
Elena Sherman
Matthew B. Dwyer

abstract: Data flow analysis (DFA) is an important verification technique that computes the effect of data values propagating over program paths. While more precise than flow-insensitive analyses, such an analysis is time-consuming.


title: Automating Deductive Verification for Weak-Memory Programs

authors:
Alexander J. Summers
Peter Müller


title: Feature-Guided Black-Box Safety Testing of Deep Neural Networks

authors:
Matthew Wicker
Xiaowei Huang
Marta Kwiatkowska

abstract: Despite the improved accuracy of deep neural networks, the discovery of adversarial examples has raised serious safety concerns. Most existing approaches for crafting adversarial examples necessitate some knowledge (architecture, parameters, etc.) of the network at hand. In this paper, we focus on image classifiers and propose a feature-guided black-box approach to test the safety of deep neural networks that requires no such knowledge. Our algorithm employs object detection techniques such as SIFT (Scale Invariant Feature Transform) to extract features from an image. These features are converted into a mutable saliency distribution, where high probability is assigned to pixels that affect the composition of the image with respect to the human visual system. We formulate the crafting of adversarial examples as a two-player turn-based stochastic game, where the first player's objective is to minimise the distance to an adversarial example by manipulating the features, and the second player can be cooperative, adversarial, or random. We show that, theoretically, the two-player game can con- verge to the optimal strategy, and that the optimal strategy represents a globally minimal adversarial image. For Lipschitz networks, we also identify conditions that provide safety guarantees that no adversarial examples exist. Using Monte Carlo tree search we gradually explore the game state space to search for adversarial examples. Our experiments show that, despite the black-box setting, manipulations guided by a perception-based saliency distribution are competitive with state-of-the-art methods that rely on white-box saliency matrices or sophisticated optimization procedures. Finally, we show how our method can be used to evaluate robustness of neural networks in safety-critical applications such as traffic sign recognition in self-driving cars.


title: Verified Model Checking of Timed Automata

authors:
Simon Wimmer
Peter Lammich

abstract: We have constructed a mechanically verified prototype implementation of a model checker for timed automata, a popular formalism for modeling real-time systems. Our goal is two-fold: first, we want to provide a reference implementation that is fast enough to check other model checkers against it on reasonably sized benchmarks; second, we strive for maximal feature compatibility with the state-of-the-art tool Uppaal. The starting point of our work is an existing highly abstract formalization of reachability checking of timed automata. We reduce checking of Uppaal-style models to the problem of model checking a single automaton in this abstract formalization, while retaining the ability to perform on the fly model-checking. Using the Isabelle Refinement Framework, the abstract specification of the model checker is refined, via multiple intermediate steps, to an actual imperative implementation in Standard ML. The resulting tool is evaluated on a set of standard benchmarks to demonstrate its practical usability.


title: YOGAR-CBMC: CBMC with Scheduling Constraint Based Abstraction Refinement - (Competition Contribution)

authors:
Liangze Yin
Wei Dong
Wanwei Liu
Yunchou Li
Ji Wang

abstract: This paper presents the Y ogar - CBMC tool for verification of multi-threaded C programs. It employs a scheduling constraint based abstraction refinement method for bounded model checking of concurrent programs. To obtain effective refinement constraints, we have proposed the notion of Event Order Graph (EOG) , and have devised two graph-based algorithms over EOG for counterexample validation and refinement generation. The experiments in SV-COMP 2017 show the promising results of our tool.


title: Efficient Verification of Imperative Programs Using Auto2

abstract: Auto2 is a recently introduced prover for the proof assistant Isabelle. It is designed to be both highly customizable from within Isabelle, and also have a powerful proof search mechanism. In this paper, we apply auto2 to the verification of imperative programs. We describe the setup of auto2 for both stages of the proof process: verification of a functional version of the program, and refining to the imperative version using separation logic. As examples, we verify several data structures, including red-black trees, interval trees, priority queues, and union-find. We also verify several algorithms making use of these data structures. These examples show that our framework is able to verify complex algorithms efficiently and in a modular manner.


title: Presentation of the 9th Edition of the Model Checking Contest

authors:
Elvio Gilberto Amparore
Bernard Berthomieu
Gianfranco Ciardo
Silvano Dal-Zilio
Francesco Gallà
Lom-Messan Hillah
Francis Hulin-Hubard
Peter Gjøl Jensen
Loïg Jezequel
Fabrice Kordon
Didier Le Botlan
Torsten Liebke
Jeroen Meijer
Andrew S. Miner
Emmanuel Paviot-Adet
Jirí Srba
Yann Thierry-Mieg
Tom van Dijk
Karsten Wolf

abstract: The Model Checking Contest (MCC) is an annual competition of software tools for model checking. Tools must process an increasing benchmark gathered from the whole community and may participate in various examinations: state space generation, computation of global properties, computation of some upper bounds in the model, evaluation of reachability formulas, evaluation of CTL formulas, and evaluation of LTL formulas. For each examination and each model instance, participating tools are provided with up to 3600 s and 16 gigabyte of memory. Then, tool answers are analyzed and confronted to the results produced by other competing tools to detect diverging answers (which are quite rare at this stage of the competition, and lead to penalties). For each examination, golden, silver, and bronze medals are attributed to the three best tools. CPU usage and memory consumption are reported, which is also valuable information for tool developers.


title: i _\mathrm Rank : A Variable Order Metric for DEDS Subject to Linear Invariants

authors:
Elvio Gilberto Amparore
Gianfranco Ciardo
Susanna Donatelli
Andrew S. Miner

abstract: Finding good variable orders for decision diagrams is essential for their effective use. We consider Multiway Decision Diagrams (MDDs) encoding a set of fixed-size vectors satisfying a set of linear invariants. Two critical applications of this problem are encoding the state space of a discrete-event discrete state system (DEDS) and encoding all solutions to a set of integer constraints. After studying the relations between the MDD structure and the constraints imposed by the linear invariants, we define i $$_\mathrm {Rank}$$ , a new variable order metric that exploits the knowledge embedded in these invariants. We evaluate i $$_\mathrm {Rank}$$ against other previously proposed metrics on a benchmark of 40 different DEDS and show that it is a better predictor of the MDD size and it is better at driving heuristics for the generation of good variable orders.


title: Minimal-Time Synthesis for Parametric Timed Automata

authors:
Étienne André
Vincent Bloemen
Laure Petrucci
Jaco van de Pol

abstract: Parametric timed automata (PTA) extend timed automata by allowing parameters in clock constraints. Such a formalism is for instance useful when reasoning about unknown delays in a timed system. Using existing techniques, a user can synthesize the parameter constraints that allow the system to reach a specified goal location, regardless of how much time has passed for the internal clocks. We focus on synthesizing parameters such that not only the goal location is reached, but we also address the following questions: what is the minimal time to reach the goal location? and for which parameter values can we achieve this? We analyse the problem and present a semi-algorithm to solve it. We also discuss and provide solutions for minimizing a specific parameter value to still reach the goal. We empirically study the performance of these algorithms on a benchmark set for PTAs and show that minimal-time reachability synthesis is more efficient to compute than the standard synthesis algorithm for reachability. Data or code related to this paper is available at: [ 26 ].


title: Java Pathfinder at SV-COMP 2019 (Competition Contribution)

authors:
Cyrille Artho
Willem Visser

abstract: This paper gives a brief overview of Java Pathfinder, or jpf-core. We describe the architecture of JPF, its strengths, and how it was set up for SV-COMP 2019.


title: Binary Decision Diagrams with Edge-Specified Reductions

authors:
Junaid Babar
Chuan Jiang
Gianfranco Ciardo
Andrew S. Miner

abstract: Various versions of binary decision diagrams (BDDs) have been proposed in the past, differing in the reduction rule needed to give meaning to edges skipping levels. The most widely adopted, fully-reduced BDDs and zero-suppressed BDDs, excel at encoding different types of boolean functions (if the function contains subfunctions independent of one or more underlying variables, or it tends to have value zero when one of its arguments is nonzero, respectively). Recently, new classes of BDDs have been proposed that, at the cost of some additional complexity and larger memory requirements per node, exploit both cases. We introduce a new type of BDD that we believe is conceptually simpler, has small memory requirements in terms of node size, tends to result in fewer nodes, and can easily be further extended with additional reduction rules. We present a formal definition, prove canonicity, and provide experimental results to support our efficiency claims.


title: Specification and Efficient Monitoring Beyond STL

authors:
Alexey Bakhirkin
Nicolas Basset

abstract: An appealing feature of Signal Temporal Logic (STL) is the existence of efficient monitoring algorithms both for Boolean and real-valued robustness semantics, which are based on computing an aggregate function (conjunction, disjunction, min, or max) over a sliding window. On the other hand, there are properties that can be monitored with the same algorithms, but that cannot be directly expressed in STL due to syntactic restrictions. In this paper, we define a new specification language that extends STL with the ability to produce and manipulate real-valued output signals and with a new form of until operator. The new language still admits efficient offline monitoring, but also allows to express some properties that in the past motivated researchers to extend STL with existential quantification, freeze quantification, and other features that increase the complexity of monitoring.


title: Debugging of Behavioural Models with CLEAR

authors:
Gianluca Barbon
Vincent Leroy
Gwen Salaün

abstract: This paper presents a tool for debugging behavioural models being analysed using model checking techniques. It consists of three parts: (i) one for annotating a behavioural model given a temporal formula, (ii) one for visualizing the erroneous part of the model with a specific focus on decision points that make the model to be correct or incorrect, and (iii) one for abstracting counterexamples thus providing an explanation of the source of the bug.


title: TOOLympics 2019: An Overview of Competitions in Formal Methods

authors:
Ezio Bartocci
Dirk Beyer
Paul E. Black
Grigory Fedyukovich
Hubert Garavel
Arnd Hartmanns
Marieke Huisman
Fabrice Kordon
Julian Nagele
Mihaela Sighireanu
Bernhard Steffen
Martin Suda
Geoff Sutcliffe
Tjark Weber
Akihisa Yamada

abstract: Evaluation of scientific contributions can be done in many different ways. For the various research communities working on the verification of systems (software, hardware, or the underlying involved mechanisms), it is important to bring together the community and to compare the state of the art, in order to identify progress of and new challenges in the research area. Competitions are a suitable way to do that. The first verification competition was created in 1992 (SAT competition), shortly followed by the CASC competition in 1996. Since the year 2000, the number of dedicated verification competitions is steadily increasing. Many of these events now happen regularly, gathering researchers that would like to understand how well their research prototypes work in practice. Scientific results have to be reproducible, and powerful computers are becoming cheaper and cheaper, thus, these competitions are becoming an important means for advancing research in verification technology. TOOLympics 2019 is an event to celebrate the achievements of the various competitions, and to understand their commonalities and differences. This volume is dedicated to the presentation of the 16 competitions that joined TOOLympics as part of the celebration of the $$25^{ th }$$ anniversary of the TACAS conference.


title: International Competition on Runtime Verification (CRV)

authors:
Ezio Bartocci
Yliès Falcone
Giles Reger

abstract: We review the first five years of the international Competition on Runtime Verification (CRV), which began in 2014. Runtime verification focuses on verifying system executions directly and is a useful lightweight technique to complement static verification techniques. The competition has gone through a number of changes since its introduction, which we highlight in this paper.


title: The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations

authors:
Nils Becker
Peter Müller
Alexander J. Summers

abstract: SMT solvers typically reason about universal quantifiers via E-matching: syntactic matching patterns for each quantifier prescribe shapes of ground terms whose presence in the SMT run will trigger quantifier instantiations. The effectiveness and performance of the SMT solver depend crucially on well-chosen patterns. Overly restrictive patterns cause relevant quantifier instantiations to be missed, while overly permissive patterns can cause performance degradation including non-termination if the solver gets stuck in a matching loop. Understanding and debugging such instantiation problems is an overwhelming task, due to the typically large number of quantifier instantiations and their non-trivial interactions with each other and other solver aspects. In this paper, we present the Axiom Profiler, a tool that enables users to analyse instantiation problems effectively, by filtering and visualising rich logging information from SMT runs. Our tool implements novel techniques for automatically detecting matching loops and explaining why they repeat indefinitely. We evaluated the tool on the full test suites of five existing program verifiers, where it discovered and explained multiple previously-unknown matching loops.


title: VoxLogicA: A Spatial Model Checker for Declarative Image Analysis

authors:
Gina Belmonte
Vincenzo Ciancia
Diego Latella
Mieke Massink

abstract: Spatial and spatio-temporal model checking techniques have a wide range of application domains, among which large scale distributed systems and signal and image analysis. We explore a new domain, namely (semi-)automatic contouring in Medical Imaging, introducing the tool VoxLogicA which merges the state-of-the-art library of computational imaging algorithms ITK with the unique combination of declarative specification and optimised execution provided by spatial logic model checking. The result is a rapid , logic based analysis development methodology. The analysis of an existing benchmark of medical images for segmentation of brain tumours shows that simple VoxLogicA analysis can reach state-of-the-art accuracy, competing with best-in-class algorithms, with the advantage of explainability and easy replicability . Furthermore, due to a two-orders-of-magnitude speedup compared to the existing general-purpose spatio-temporal model checker topochecker , VoxLogicA enables interactive development of analysis of 3D medical images, which can greatly facilitate the work of professionals in this domain.


title: Digital Bifurcation Analysis of TCP Dynamics

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

abstract: Digital bifurcation analysis is a new algorithmic method for exploring how the behaviour of a parameter-dependent computer system varies with a change in its parameters and, in particular, for identification of bifurcation points where such variation becomes dramatic. We have developed the method in an analogy with the traditional bifurcation theory and have it successfully applied to models taken from systems biology. In this case study paper, we demonstrate the appropriateness and usefulness of the digital bifurcation analysis as a push-button alternative to the classical approaches as traditionally used for analysing the stability of TCP/IP protocols. We consider two typical examples (congestion control and buffer sizes throughput influence) and show that the method provides the same results as obtained with classical non-automatic analytical and numerical methods.


title: Automatic Verification of C and Java Programs: SV-COMP 2019

abstract: This report describes the 2019 Competition on Software Verification (SV-COMP), the 8 \(^{\text {th}}\) edition of a series of comparative evaluations of fully automatic software verifiers for C programs, and now also for Java programs. The competition provides a snapshot of the current state of the art in the area, and has a strong focus on replicability of its results. The repository of benchmark verification tasks now supports a new, more flexible format for task definitions (based on YAML), which was a precondition for conveniently benchmarking Java programs in the same controlled competition setting that was successfully applied in the previous years. The competition was based on 10 522 verification tasks for C programs and 368 verification tasks for Java programs. Each verification task consisted of a program and a property (reachability, memory safety, overflows, termination). SV-COMP 2019 had 31 participating verification systems from 14 countries.


abstract: Tool competitions are a special form of comparative evaluation, where each tool has a team of developers or supporters associated that makes sure the tool is properly configured to show its best possible performance. Tool competitions have been a driving force for the development of mature tools that represent the state of the art in several research areas. This paper describes the International Competition on Software Testing (Test-Comp), a comparative evaluation of automatic tools for software test generation. Test-Comp 2019 is presented as part of TOOLympics 2019, a satellite event of the conference TACAS.