title: Learning Realtime One-Counter Automata

authors:
Véronique Bruyère
Guillermo A. Pérez
Gaëtan Staquet

abstract: Abstract We present a new learning algorithm for realtime one-counter automata. Our algorithm uses membership and equivalence queries as in Angluin’s $${L}^*$$ L ∗ algorithm, as well as counter value queries and partial equivalence queries. In a partial equivalence query, we ask the teacher whether the language of a given finite-state automaton coincides with a counter-bounded subset of the target language. We evaluate an implementation of our algorithm on a number of random benchmarks and on a use case regarding efficient JSON-stream validation.


venue: tacas

title: Clausal Proofs for Pseudo-Boolean Reasoning

authors:
Randal E. Bryant
Armin Biere
Marijn J. H. Heule

abstract: Abstract When augmented with a Pseudo-Boolean (PB) solver, a Boolean satisfiability (SAT) solver can apply apply powerful reasoning methods to determine when a set of parity or cardinality constraints, extracted from the clauses of the input formula, has no solution. By converting the intermediate constraints generated by the PB solver into ordered binary decision diagrams (BDDs), a proof-generating, BDD-based SAT solver can then produce a clausal proof that the input formula is unsatisfiable. Working together, the two solvers can generate proofs of unsatisfiability for problems that are intractable for other proof-generating SAT solvers. The PB solver can, at times, detect that the proof can exploit modular arithmetic to give smaller BDD representations and therefore shorter proofs.


title: BRICK: Path Enumeration Based Bounded Reachability Checking of C Program (Competition Contribution)

authors:
Lei Bu
Zhunyi Xie
Lecheng Lyu
Yichao Li
Xiao Guo
Jianhua Zhao
Xuandong Li

abstract: Abstract BRICK is a bounded reachability checker for embedded C programs. BRICK conducts a path-oriented style checking of the bounded state space of the program, that enumerates and checks all the possible paths of the program in the threshold one by one. To alleviate the path explosion problem, BRICK locates and records unsatisfiable core path segments during the checking of each path and uses them to prune the search space. Furthermore, derivative free optimization based falsification and loop induction are introduced to handle complex program features like nonlinear path conditions and loops efficiently.


title: Practical Applications of the Alternating Cycle Decomposition

authors:
Antonio Casares
Alexandre Duret-Lutz
Klara J. Meyer
Florian Renkin
Salomon Sickert

abstract: Abstract In 2021, Casares, Colcombet, and Fijalkow introduced the Alternating Cycle Decomposition (ACD) to study properties and transformations of Muller automata. We present the first practical implementation of the ACD in two different tools, Owl and Spot, and adapt it to the framework of Emerson-Lei automata, i.e., $$\omega $$ ω -automata whose acceptance conditions are defined by Boolean formulas. The ACD provides a transformation of Emerson-Lei automata into parity automata with strong optimality guarantees: the resulting parity automaton is minimal among those automata that can be obtained by duplication of states. Our empirical results show that this transformation is usable in practice. Further, we show how the ACD can generalize many other specialized constructions such as deciding typeness of automata and degeneralization of generalized Büchi automata, providing a framework of practical algorithms for $$\omega $$ ω -automata.


title: Formal Verification of the Ethereum 2.0 Beacon Chain

authors:
Franck Cassez
Joanne Fuller
Aditya Asgaonkar

abstract: Abstract We report our experience in the formal verification of the reference implementation of the Beacon Chain. The Beacon Chain is the backbone component of the new Proof-of-Stake Ethereum 2.0 network: it is in charge of tracking information about the validators, their stakes, their attestations (votes) and if some validators are found to be dishonest, to slash them (they lose some of their stakes). The Beacon Chain is mission-critical and any bug in it could compromise the whole network. The Beacon Chain reference implementation developed by the Ethereum Foundation is written in Python, and provides a detailed operational description of the state machine each Beacon Chain’s network participant (node) must implement. We have formally specified and verified the absence of runtime errors in (a large and critical part of) the Beacon Chain reference implementation using the verification-friendly language Dafny. During the course of this work, we have uncovered several issues, proposed verified fixes. We have also synthesised functional correctness specifications that enable us to provide guarantees beyond runtime errors. Our software artefact with the code and proofs in Dafny is available at https://github.com/ConsenSys/eth2.0-dafny .


title: Better Counterexamples for Dafny

authors:
Aleksandar Chakarov
Aleksandr Fedchin
Zvonimir Rakamaric
Neha Rungta

abstract: Abstract Dafny is a verification-aware programming language used at Amazon Web Services to develop critical components of their access management, storage, and cryptography infrastructures. The Dafny toolchain provides a verifier that can prove an implementation of a method satisfies its specification. When the underlying SMT solver cannot establish a proof, it generates a counterexample. These counterexamples are hard to understand and their interpretation is often a bottleneck in the proof debugging process. In this paper, we introduce an open-source tool that transforms counterexamples generated by the SMT solver to a more user-friendly format that maps to the Dafny syntax and is suitable for further processing. This new tool allows the Dafny developers to quickly identify the root cause of a problem with their proof, thereby speeding up the development of Dafny projects.


title: Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding - (Competition Contribution)

authors:
Marek Chalupa
Vincent Mihalkovic
Anna Rechtácková
Lukás Zaoral
Jan Strejcek

abstract: Abstract The development of Symbiotic 9 focused mainly on two components. One is the symbolic executor Slowbeast, which newly supports backward symbolic execution including its extension called loop folding. This technique can infer inductive invariants from backward symbolic execution states. Thanks to these invariants, Symbiotic 9 is able to produce non-trivial correctness witnesses, which is a feature that is missing in previous versions of Symbiotic. We have also extended forward symbolic execution in Slowbeast with a basic support for parallel programs. The second component with significant improvements is the instrumentation module. In particular, we have extended the static analysis of accesses to arrays with features designed for programs that manipulate C strings. Symbiotic 9 is the Overall winner of SV-COMP 2022. Moreover, it won also the categories MemSafety and SoftwareSystems, and placed third in FalsificationOverall.


title: A Prototype for Data Race Detection in CSeq 3 - (Competition Contribution)

authors:
Alex Coto
Omar Inverso
Emerson Sales
Emilio Tuosto

abstract: Abstract We sketch a sequentialization-based technique for bounded detection of data races under sequential consistency, and summarise the major improvements to our verification framework over the last years.


title: Fast and Reliable Formal Verification of Smart Contracts with the Move Prover

authors:
David L. Dill
Wolfgang Grieskamp
Junkil Park
Shaz Qadeer
Meng Xu
Jingyi Emma Zhong

abstract: Abstract The Move Prover () is a formal verifier for smart contracts written in the Move programming language. has an expressive specification language, and is fast and reliable enough that it can be run routinely by developers and in integration testing. Besides the simplicity of smart contracts and the Move language, three implementation approaches are responsible for the practicality of : (1) an alias-free memory model, (2) fine-grained invariant checking, and (3) monomorphization. The entirety of the Move code for the Diem blockchain has been extensively specified and can be completely verified by in a few minutes. Changes in the Diem framework must be successfully verified before being integrated into the open source repository on GitHub.


title: Comparative Verification of the Digital Library of Mathematical Functions and Computer Algebra Systems

authors:
André Greiner-Petter
Howard S. Cohl
Abdou Youssef
Moritz Schubotz
Avi Trost
Rajen Dey
Akiko Aizawa
Bela Gipp

abstract: Digital mathematical libraries assemble the knowledge of years of mathematical research. Numerous disciplines (e.g., physics, engineering, pure and applied mathematics) rely heavily on compendia gathered findings. Likewise, modern research applications rely more and more on computational solutions, which are often calculated and verified by computer algebra systems. Hence, the correctness, accuracy, and reliability of both digital mathematical libraries and computer algebra systems is a crucial attribute for modern research. In this paper, we present a novel approach to verify a digital mathematical library and two computer algebra systems with one another by converting mathematical expressions from one system to the other. We use our previously eveloped conversion tool (referred to as LaCASt) to translate formulae from the NIST Digital Library of Mathematical Functions to the computer algebra systems Maple and Mathematica. The contributions of our presented work are as follows: (1) we present the most comprehensive verification of computer algebra systems and digital mathematical libraries with one another; (2) we significantly enhance the performance of the underlying translator in terms of coverage and accuracy; and (3) we provide open access to translations for Maple and Mathematica of the formulae in the NIST Digital Library of Mathematical Functions.


title: A Probabilistic Logic for Verifying Continuous-time Markov Chains

authors:
Ji Guan
Nengkun Yu

abstract: Abstract A continuous-time Markov chain (CTMC) execution is a continuous class of probability distributions over states. This paper proposes a probabilistic linear-time temporal logic, namely continuous-time linear logic (CLL), to reason about the probability distribution execution of CTMCs. We define the syntax of CLL on the space of probability distributions. The syntax of CLL includes multiphase timed until formulas, and the semantics of CLL allows time reset to study relatively temporal properties. We derive a corresponding model-checking algorithm for CLL formulas. The correctness of the model-checking algorithm depends on Schanuel’s conjecture, a central open problem in transcendental number theory. Furthermore, we provide a running example of CTMCs to illustrate our method.


title: Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time

authors:
Simon Guilloud
Viktor Kuncak

abstract: Abstract Motivated by proof checking, we consider the problem of efficiently establishing equivalence of propositional formulas by relaxing the completeness requirements while still providing certain guarantees. We present a quasilinear time algorithm to decide the word problem on a natural algebraic structures we call orthocomplemented bisemilattices, a subtheory of Boolean algebra. The starting point for our procedure is a variation of Aho, Hopcroft, Ullman algorithm for isomorphism of trees, which we generalize to directed acyclic graphs. We combine this algorithm with a term rewriting system we introduce to decide equivalence of terms. We prove that our rewriting system is terminating and confluent, implying the existence of a normal form. We then show that our algorithm computes this normal form in log linear (and thus sub-quadratic) time. We provide pseudocode and a minimal working implementation in Scala.


title: Correct Probabilistic Model Checking with Floating-Point Arithmetic

abstract: Abstract Probabilistic model checking computes probabilities and expected values related to designated behaviours of interest in Markov models. As a formal verification approach, it is applied to critical systems; thus we trust that probabilistic model checkers deliver correct results. To achieve scalability and performance, however, these tools use finite-precision floating-point numbers to represent and calculate probabilities and other values. As a consequence, their results are affected by rounding errors that may accumulate and interact in hard-to-predict ways. In this paper, we show how to implement fast and correct probabilistic model checking by exploiting the ability of current hardware to control the direction of rounding in floating-point calculations. We outline the complications in achieving correct rounding from higher-level programming languages, describe our implementation as part of the Modest Toolset’s model checker, and exemplify the tradeoffs between performance and correctness in an extensive experimental evaluation across different operating systems and CPU architectures.


title: Sky Is Not the Limit - Tighter Rank Bounds for Elevator Automata in Büchi Automata Complementation

authors:
Vojtech Havlena
Ondrej Lengál
Barbora Smahlíková

abstract: Abstract We propose several heuristics for mitigating one of the main causes of combinatorial explosion in rank-based complementation of Büchi automata (BAs): unnecessarily high bounds on the ranks of states. First, we identifyelevator automata, which is a large class of BAs (generalizing semi-deterministic BAs), occurring often in practice, where ranks of states are bounded according to the structure of strongly connected components. The bounds for elevator automata also carry over to general BAs that contain elevator automata as a sub-structure. Second, we introduce two techniques for refining bounds on the ranks of BA states using data-flow analysis of the automaton. We implement out techniques as an extension of the toolRankerfor BA complementation and show that they indeed greatly prune the generated state space, obtaining significantly better results and outperforming other state-of-the-art tools on a large set of benchmarks.


title: Deagle: An SMT-based Verifier for Multi-threaded Programs (Competition Contribution)

authors:
Fei He
Zhihang Sun
Hongyu Fan

abstract: Abstract is an SMT-based multi-threaded program verification tool. It is built on top of (front-end) and (back-end). The basic idea of is to integrate into the SMT solver an ordering consistency theory that handles ordering relations over the shared variable accesses in the program. The front-end encodes the input program into an extended propositional formula that contains ordering constraints. The back-end is reinforced with a solver for the ordering consistency theory. This paper presents the basic idea, architecture, installation, and usage of .


title: AProVE: Non-Termination Witnesses for C Programs - (Competition Contribution)

authors:
Jera Hensel
Constantin Mensendiek
Jürgen Giesl

abstract: Abstract To (dis)prove termination of programs, uses symbolic execution to transform the program’s code into an integer transition system, which is then analyzed by several backends. The transformation steps in and the tools in the backend only produce sub-proofs in their domains. Hence, we now developed new techniques to automatically combine the essence of these proofs. If non-termination is proved, then they yield an overall witness, which identifies a non-terminating path in the original program.


title: GWIT: A Witness Validator for Java based on GraalVM (Competition Contribution)

authors:
Falk Howar
Malte Mues

abstract: Abstract GWIT is a validator for violation witnesses produced by Java verifiers in the SV-COMP software verification competition. GWIT weaves assumptions documented in a witness into the source code of a program, effectively restricting the part of the program that is explored by a program analysis. It then uses the GDart tool (dynamic symbolic execution) to search for reachable errors in the modified program.


title: Kmclib: Automated Inference and Verification of Session Types from OCaml Programs

authors:
Keigo Imai
Julien Lange
Rumyana Neykova

abstract: Abstract Theories and tools based on multiparty session types offer correctness guarantees for concurrent programs that communicate using message-passing. These guarantees usually come at the cost of an intrinsically top-down approach, which requires the communication behaviour of the entire program to be specified as a global type. This paper introduces : an OCaml library that supports the development of correct message-passing programs without having to write any types. The library utilises the meta-programming facilities of OCaml to automatically infer the session types of concurrent programs and verify their compatibility (k-MC [15]). Well-typed programs, written with , do not lead to communication errors and cannot get stuck.


title: The Static Analyzer Infer in SV-COMP (Competition Contribution)

authors:
Matthias Kettl
Thomas Lemberger

abstract: Abstract We present Infer-sv, a wrapper that adapts Infer for SV-COMP. Infer is a static-analysis tool for C and other languages, developed by Facebook and used by multiple large companies. It is strongly aimed at industry and the internal use at Facebook. Despite its popularity, there are no reported numbers on its precision and efficiency. With Infer-sv, we take a first step towards an objective comparison of Infer with other SV-COMP participants from academia and industry.


title: Ultimate GemCutter and the Axes of Generalization - (Competition Contribution)

authors:
Dominik Klumpp
Daniel Dietsch
Matthias Heizmann
Frank Schüssele
Marcel Ebbinghaus
Azadeh Farzan
Andreas Podelski

abstract: Abstract Ultimate GemCutter verifies concurrent programs using the CEGAR paradigm, by generalizing from spurious counterexample traces to larger sets of correct traces. We integrate classical CEGAR generalization with orthogonal generalization across interleavings. Thereby, we are able to prove correctness of programs otherwise out-of-reach for interpolation-based verification. The competition results show significant advantages over other concurrency approaches in the Ultimate family.


title: Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion

authors:
Jason R. Koenig
Oded Padon
Sharon Shoham
Alex Aiken

abstract: Abstract We present a PDR/IC3 algorithm for finding inductive invariants with quantifier alternations. We tackle scalability issues that arise due to the large search space of quantified invariants by combining a breadth-first search strategy and a new syntactic form for quantifier-free bodies. The breadth-first strategy prevents inductive generalization from getting stuck in regions of the search space that are expensive to search and focuses instead on lemmas that are easy to discover. The new syntactic form is well-suited to lemmas with quantifier alternations by allowing both limited conjunction and disjunction in the quantifier-free body, while carefully controlling the size of the search space. Combining the breadth-first strategy with the new syntactic form results in useful inductive bias by prioritizing lemmas according to: (i) well-defined syntactic metrics for simple quantifier structures and quantifier-free bodies, and (ii) the empirically useful heuristic of preferring lemmas that are fast to discover. On a benchmark suite of primarily distributed protocols and complex Paxos variants, we demonstrate that our algorithm can solve more of the most complicated examples than state-of-the-art techniques.


title: From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques

authors:
Vasileios Koutavas
Yu-Yang Lin
Nikos Tzevelekos

abstract: Abstract We present a bounded equivalence verification technique for higher-order programs with local state. This technique combines fully abstract symbolic environmental bisimulations similar to symbolic game semantics, novel up-to techniques, and lightweight state invariant annotations. This yields an equivalence verification technique with no false positives or negatives. The technique is bounded-complete, in that all inequivalences are automatically detected given large enough bounds. Moreover, several hard equivalences are proved automatically or after being annotated with state invariants. We realise the technique in a tool prototype called Hobbit and benchmark it with an extensive set of new and existing examples. Hobbit can prove many classical equivalences including all Meyer and Sieber examples.


title: Inferring Interval-Valued Floating-Point Preconditions

authors:
Jonas Krämer
Lionel Blatter
Eva Darulova
Mattias Ulbrich

abstract: Abstract Aggregated roundoff errors caused by floating-point arithmetic can make numerical code highly unreliable. Verified postconditions for floating-point functions can guarantee the accuracy of their results under specific preconditions on the function inputs, but how to systematically find an adequate precondition for a desired error bound has not been explored so far. We present two novel techniques for automatically synthesizing preconditions for floating-point functions that guarantee that user-provided accuracy requirements are satisfied. Our evaluation on a standard benchmark set shows that our approaches are complementary and able to find accurate preconditions in reasonable time.


title: The Complexity of LTL Rational Synthesis

authors:
Orna Kupferman
Noam Shenwald

abstract: Abstract Inrational synthesis, we automatically construct a reactive system that satisfies its specification in all rational environments, namely environments that have objectives and act to fulfill them. We complete the study of the complexity of LTL rational synthesis. Our contribution is threefold. First, we tighten the known upper bounds for settings that were left open in earlier work. Second, our complexity analysis is parametric, and we describe tight upper and lower bounds in each of the problem parameters: the game graph, the objectives of the system components, and the objectives of the environment components. Third, we generalize the definition of rational synthesis, combining the cooperative and non-cooperative approaches studied in earlier work, and extend our complexity analysis to the general definition.


title: Correlated Equilibria and Fairness in Concurrent Stochastic Games

authors:
Marta Kwiatkowska
Gethin Norman
David Parker
Gabriel Santos

abstract: Abstract Game-theoretic techniques and equilibria analysis facilitate the design and verification of competitive systems. While algorithmic complexity of equilibria computation has been extensively studied, practical implementation and application of game-theoretic methods is more recent. Tools such as PRISM-games support automated verification and synthesis of zero-sum and ( $$\varepsilon $$ ε -optimal subgame-perfect) social welfare Nash equilibria properties for concurrent stochastic games. However, these methods become inefficient as the number of agents grows and may also generate equilibria that yield significant variations in the outcomes for individual agents. We extend the functionality of PRISM-games to support correlated equilibria, in which players can coordinate through public signals, and introduce a novel optimality criterion of social fairness, which can be applied to both Nash and correlated equilibria. We show that correlated equilibria are easier to compute, are more equitable, and can also improve joint outcomes. We implement algorithms for both normal form games and the more complex case of multi-player concurrent stochastic games with temporal logic specifications. On a range of case studies, we demonstrate the benefits of our methods.


title: LART: Compiled Abstract Execution - (Competition Contribution)

authors:
Henrich Lauko
Petr Rockai

abstract: Abstract lart – llvm abstraction and refinement tool – originates from the divine model-checker [5, 7], in which it was employed as an abstraction toolchain for the llvm interpreter. In this contribution, we present a stand-alone tool that does not need a verification backend but performs the verification natively. The core idea is to instrument abstract semantics directly into the program and compile it into a native binary that performs program analysis. This approach provides a performance gain of native execution over the interpreted analysis and allows compiler optimizations to be employed on abstracted code, further extending the analysis efficiency. Compilation-based abstraction introduces new challenges solved by lart, like domain interaction of concrete and abstract values simulation of nondeterministic runtime or constraint propagation.


title: On-The-Fly Solving for Symbolic Parity Games

authors:
Maurice Laveaux
Wieger Wesselink
Tim A. C. Willemse

abstract: Abstract Parity games can be used to represent many different kinds of decision problems. In practice, tools that use parity games often rely on a specification in a higher-order logic from which the actual game can be obtained by means of an exploration. For many of these decision problems we are only interested in the solution for a designated vertex in the game. We formalise how to use on-the-fly solving techniques during the exploration process, and show that this can help to decide the winner of such a designated vertex in an incomplete game. Furthermore, we define partial solving techniques for incomplete parity games and show how these can be made resilient to work directly on the incomplete game, rather than on a set of safe vertices. We implement our techniques for symbolic parity games and study their effectiveness in practice, showing that speed-ups of several orders of magnitude are feasible and overhead (if unavoidable) is typically low.


title: Graves-CPA: A Graph-Attention Verifier Selector (Competition Contribution)

authors:
Will Leeson
Matthew B. Dwyer

abstract: Abstract Graves-CPA is a verification tool which uses algorithm selection to decide an ordering of underlying verifiers to most effectively verify a given program. Graves-CPA represents programs using an amalgam of traditional program graph representations and uses state-of-the-art graph neural network techniques to dynamically decide how to run a set of verification techniques. The Graves technique is implementation agnostic, but it’s competition submission, Graves-CPA, is built using several CPAchecker configurations as its underlying verifiers.


title: Dartagnan: SMT-based Violation Witness Validation (Competition Contribution)

authors:
Hernán Ponce de León
Thomas Haas
Roland Meyer

abstract: Abstract The validation of violation witnesses is an important step during software verification. It hides false alarms raised by verifiers from engineers, which in turn helps them concentrate on critical issues and improves the verification experience. Until the 2021 edition of the Competition on Software Verification (SV-COMP), CPAchecker was the only witness validator for the ConcurrencySafety category. This article describes how we extended the Dartagnan verifier to support the validation of violation witnesses. The results of the 2022 edition of the competition show that, for witnesses generated by different verifiers, Dartagnan succeeds in the validation of witnesses where CPAchecker does not. Our extension thus improves the validation possibilities for the overall competition. We discuss Dartagnan ’s strengths and weaknesses as a validation tool and describe possible ways to improve it in the future.


title: ZDD Boolean Synthesis

authors:
Yi Lin
Lucas M. Tabajara
Moshe Y. Vardi

abstract: Abstract Motivated by applications in boolean-circuit design, boolean synthesis is the process of synthesizing a boolean function with multiple outputs, given a relation between its inputs and outputs. Previous work has attempted to solve boolean functional synthesis by converting a specification formula into a Binary Decision Diagram (BDD) and quantifying existentially the output variables. We make use of the fact that the specification is usually given in the form of a Conjunctive Normal Form (CNF) formula, and we can perform resolution on a symbolic representation of a CNF formula in the form of a Zero-suppressed Binary Decision Diagram (ZDD). We adapt the realizability test to the context of CNF and ZDD, and show that theCrossoperation defined in earlier work can be used for witness construction. Experiments show that our approach is complementary to BDD-based Boolean synthesis.


title: GDart: An Ensemble of Tools for Dynamic Symbolic Execution on the Java Virtual Machine (Competition Contribution)

authors:
Malte Mues
Falk Howar

abstract: Abstract GDart is an ensemble of tools allowing dynamic symbolic execution of JVM programs. The dynamic symbolic execution engine is decomposed into three different components: a symbolic decision engine (DSE), a concolic executor (SPouT), and a SMT solver backend allowing meta-strategy solving of SMT problems (JConstraints). The symbolic decision component is loosely coupled with the executor by a newly introduced communication protocol. At SV-COMP 2022, GDart solved 471 of 586 tasks finding more correct false results (302) than correct true results (169). It scored fourth place.


title: Forest GUMP: A Tool for Explanation

authors:
Alnis Murtovi
Alexander Bainczyk
Bernhard Steffen

abstract: Abstract In this paper, we present Forest GUMP (for Generalized, Unifying Merge Process) a tool for providing tangible experience with three concepts of explanation. Besides the well-known model explanation and outcome explanation, Forest GUMP also supports class characterization, i.e., the precise characterization of all samples with the same classification. Key technology to achieve these results is algebraic aggregation, i.e., the transformation of a Random Forest into a semantically equivalent, concise white-box representation in terms of Algebraic Decision Diagrams (ADDs). The paper sketches the method and illustrates the use of Forest GUMP along an illustrative example taken from the literature. This way readers should acquire an intuition about the tool, and the way how it should be used to increase the understanding not only of the considered dataset, but also of the character of Random Forests and the ADD technology, here enriched to comprise infeasible path elimination.


title: Synthesis of Compact Strategies for Coordination Programs

authors:
Kedar S. Namjoshi
Nisarg Patel

abstract: Abstract In multi-agent settings, such as IoT and robotics, it is necessary to coordinate the actions of independent agents in order to achieve a joint behavior. While it is often easy to specify the desired joint behavior, programming the necessary coordination can be difficult. In this work, we develop theory and methods to synthesize coordination strategies that are guaranteed not to initiate unnecessary actions. We refer to such strategies as being “compact.” We formalize the intuitive notion of compactness; show that existing methods do not guarantee compactness; and propose a solution. The solution transforms a given temporal logic specification, using automata-theoretic constructions, to incorporate a notion of minimality. The central result is that the winning strategies for the transformed specification are precisely the compact strategies for the original. One can therefore apply known synthesis methods to produce compact strategies. We report on prototype implementations that synthesize compact strategies for temporal logic specifications and for specifications of multi-robot coordination.


title: LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions

authors:
Brandon Paulsen
Chao Wang

abstract: Abstract The most scalable approaches to certifying neural network robustness depend on computing sound linear lower and upper bounds for the network’s activation functions. Current approaches are limited in that the linear bounds must be handcrafted by an expert, and can be sub-optimal, especially when the network’s architecture composes operations using, for example, multiplication such as in LSTMs and the recently popularSwishactivation. The dependence on an expert prevents the application of robustness certification to developments in the state-of-the-art of activation functions, and furthermore the lack of tightness guarantees may give a false sense of insecurity about a particular model. To the best of our knowledge, we are the first to consider the problem ofautomaticallysynthesizingtightlinear bounds for arbitrary n-dimensional activation functions. We propose the first fully automated method that achieves tight linear bounds while only leveraging the mathematical definition of the activation function itself. Our method leverages an efficient heuristic technique to synthesize bounds that are tight andusually sound, and then verifies the soundness (and adjusts the bounds if necessary) using the highly optimized branch-and-bound SMT solver,dReal. Even though our method depends on an SMT solver, we show that the runtime is reasonable in practice, and, compared with state of the art, our method often achieves 2-5X tighter final output bounds and more than quadruple certified robustness.


title: Automated Translation of Natural Language Requirements to Runtime Monitors

authors:
Ivan Perez
Anastasia Mavridou
Thomas Pressburger
Alwyn Goodloe
Dimitra Giannakopoulou

abstract: Abstract Runtime verification (RV) enables monitoring systems at runtime, to detect property violations early and limit their potential consequences. This paper presents an end-to-end framework to capture requirements in structured natural language and generate monitors that capture their semantics faithfully. We leverage NASA’s Formal Requirement Elicitation Tool (fret), and the RV systemCopilot. We extendfretwith mechanisms to capture additional information needed to generate monitors, and introduceOgma, a new tool to bridge the gap betweenfretandCopilot. With this framework, users can write requirements in an intuitive format and obtain real-time C monitors suitable for use in embedded systems. Our toolchain is available as open source.


title: MaskD: A Tool for Measuring Masking Fault-Tolerance

authors:
Luciano Putruele
Ramiro Demasi
Pablo F. Castro
Pedro R. D'Argenio

abstract: Abstract We present , an automated tool designed to measure the level of fault-tolerance provided by software components. The tool focuses on measuring masking fault-tolerance, that is, the kind of fault-tolerance that allows systems to mask faults in such a way that they cannot be observed by the users. The tool takes as input a nominal model (which serves as a specification) and its fault-tolerant implementation, described by means of a guarded-command language, and automatically computes the masking distance between them. This value can be understood as the level of fault-tolerance provided by the implementation. The tool is based on a sound and complete framework we have introduced in previous work. We present the ideas behind the tool by means of a simple example and report experiments realized on more complex case studies.


title: Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic

authors:
Ritam Raha
Rajarshi Roy
Nathanaël Fijalkow
Daniel Neider

abstract: Abstract Linear temporal logic (LTL) is a specification language for finite sequences (called traces) widely used in program verification, motion planning in robotics, process mining, and many other areas. We consider the problem of learning formulas in fragments of LTL without the $$\mathbf {U}$$ U -operator for classifying traces; despite a growing interest of the research community, existing solutions suffer from two limitations: they do not scale beyond small formulas, and they may exhaust computational resources without returning any result. We introduce a new algorithm addressing both issues: our algorithm is able to construct formulas an order of magnitude larger than previous methods, and it is anytime, meaning that it in most cases successfully outputs a formula, albeit possibly not of minimal size. We evaluate the performances of our algorithm using an open source implementation against publicly available benchmarks.


title: Moving Definition Variables in Quantified Boolean Formulas

authors:
Joseph E. Reeves
Marijn J. H. Heule
Randal E. Bryant

abstract: Abstract Augmenting problem variables in a quantified Boolean formula with definition variables enables a compact representation in clausal form. Generally these definition variables are placed in the innermost quantifier level. To restore some structural information, we introduce a preprocessing technique that moves definition variables to the quantifier level closest to the variables that define them. We express the movement in the QRAT proof system to allow verification by independent proof checkers. We evaluated definition variable movement on the QBFEVAL’20 competition benchmarks. Movement significantly improved performance for the competition’s top solvers. Combining variable movement with the preprocessorBloqqerimproves solver performance compared to usingBloqqeralone.


title: Alpinist: An Annotation-Aware GPU Program Optimizer

authors:
Ömer Sakar
Mohsen Safari
Marieke Huisman
Anton Wijs

abstract: Abstract GPU programs are widely used in industry. To obtain the best performance, a typical development process involves the manual or semi-automatic application of optimizations prior to compiling the code. To avoid the introduction of errors, we can augment GPU programs with (pre- and postcondition-style) annotations to capture functional properties. However, keeping these annotations correct when optimizing GPU programs is labor-intensive and error-prone. This paper introduces Alpinist, an annotation-aware GPU program optimizer. It applies frequently-used GPU optimizations, but besides transforming code, it also transforms the annotations. We evaluate Alpinist, in combination with the VerCors program verifier, to automatically optimize a collection of verified programs and reverify them.


title: Automatic Repair for Network Programs

authors:
Lei Shi
Yuepeng Wang
Rajeev Alur
Boon Thau Loo

abstract: Abstract Debugging imperative network programs is a difficult task for operators as it requires understanding various network modules and complicated data structures. For this purpose, this paper presents an automated technique for repairing network programs with respect to unit tests. Given as input a faulty network program and a set of unit tests, our approach localizes the fault through symbolic reasoning, and synthesizes a patch ensuring that the repaired program passes all unit tests. It applies domain-specific abstraction to simplify network data structures and exploits function summary reuse for modular symbolic analysis. We have implemented the proposed techniques in a tool called NetRep and evaluated it on 10 benchmarks adapted from real-world software-defined network controllers. The evaluation results demonstrate the effectiveness and efficiency of NetRep for repairing network programs.


title: Adiar Binary Decision Diagrams in External Memory

authors:
Steffan Christ Sølvsten
Jaco van de Pol
Anna Blume Jakobsen
Mathias Weller Berg Thomasen

abstract: Abstract We follow up on the idea of Lars Arge to rephrase the Reduce and Apply operations of Binary Decision Diagrams (BDDs) as iterative I/O-efficient algorithms. We identify multiple avenues to simplify and improve the performance of his proposed algorithms. Furthermore, we extend the technique to other common BDD operations, many of which are not derivable using Apply operations alone. We provide asymptotic improvements to the few procedures that can be derived using Apply. Our work has culminated in a BDD package named Adiar that is able to efficiently manipulate BDDs that outgrow main memory. This makes Adiar surpass the limits of conventional BDD packages that use recursive depth-first algorithms. It is able to do so while still achieving a satisfactory performance compared to other BDD packages: Adiar, in parts using the disk, is on instances larger than 9.5 GiB only 1.47 to 3.69 times slower compared to CUDD and Sylvan, exclusively using main memory. Yet, Adiar is able to obtain this performance at a fraction of the main memory needed by conventional BDD packages to function.


title: NeuReach: Learning Reachability Functions from Simulations

authors:
Dawei Sun
Sayan Mitra

abstract: Abstract We present , a tool that uses neural networks for predicting reachable sets from executions of a dynamical system. Unlike existing reachability tools, computes areachability functionthat outputs an accurate over-approximation of the reachable set foranyinitial set in a parameterized family. Such reachability functions are useful for online monitoring, verification, and safe planning. implements empirical risk minimization for learning reachability functions. We discuss the design rationale behind the optimization problem and establish that the computed output is probably approximately correct. Our experimental evaluations over a variety of systems show promise. can learn accurate reachability functions for complex nonlinear systems, including some that are beyond existing methods. From a learned reachability function, arbitrary reachtubes can be computed in milliseconds. is available at https://github.com/sundw2014/NeuReach .


title: HOLL: Program Synthesis for Higher Order Logic Locking

authors:
Gourav Takhar
Ramesh Karri
Christian Pilato
Subhajit Roy

abstract: Abstract Logic locking “hides” the functionality of a digital circuit to protect it from counterfeiting, piracy, and malicious design modifications. The original design is transformed into a “locked” design such that the circuit reveals its correct functionality only when it is “unlocked” with a secret sequence of bits—the key bit-string. However, strong attacks, especially the SAT attack that uses a SAT solver to recover the key bit-string, have been profoundly effective at breaking the locked circuit and recovering the circuit functionality. We lift logic locking to Higher Order Logic Locking (HOLL) by hiding a higher-order relation, instead of a key of independent values, challenging the attacker to discover this key relation to recreate the circuit functionality. Our technique uses program synthesis to construct the locked design and synthesize a corresponding key relation. HOLL has low overhead and existing attacks for logic locking do not apply as the entity to be recovered is no more a value. To evaluate our proposal, we propose a new attack (SynthAttack) that uses an inductive synthesis algorithm guided by an operational circuit as an input-output oracle to recover the hidden functionality. SynthAttack is inspired by the SAT attack, and similar to the SAT attack, it is verifiably correct, i.e., if the correct functionality is revealed, a verification check guarantees the same. Our empirical analysis shows that SynthAttack can break HOLL for small circuits and small key relations, but it is ineffective for real-life designs.


title: A New Approach for Active Automata Learning Based on Apartness

authors:
Frits W. Vaandrager
Bharat Garhewal
Jurriaan Rot
Thorsten Wißmann

abstract: Abstract We present $$L^{\#}$$ L # , a new and simple approach to active automata learning. Instead of focusing on equivalence of observations, like the $$L^{*}$$ L ∗ algorithm and its descendants, $$L^{\#}$$ L # takes a different perspective: it tries to establish apartness, a constructive form of inequality. $$L^{\#}$$ L # does not require auxiliary notions such as observation tables or discrimination trees, but operates directly on tree-shaped automata. $$L^{\#}$$ L # has the same asymptotic query and symbol complexities as the best existing learning algorithms, but we show that adaptive distinguishing sequences can be naturally integrated to boost the performance of $$L^{\#}$$ L # in practice. Experiments with a prototype implementation, written in Rust, suggest that $$L^{\#}$$ L # is competitive with existing algorithms.


title: Verifying Fortran Programs with CIVL

authors:
Wenhao Wu
Jan Hückelheim
Paul D. Hovland
Stephen F. Siegel

abstract: Abstract Fortran is widely used in computational science, engineering, and high performance computing. This paper presents an extension to the CIVL verification framework to check correctness properties of Fortran programs. Unlike previous work that translates Fortran to C, LLVM IR, or other intermediate formats before verification, our work allows CIVL to directly consume Fortran source files. We extended the parsing, translation, and analysis phases to support Fortran-specific features such as array slicing and reshaping, and to find program violations that are specific to Fortran, such as argument aliasing rule violations, invalid use of variable and function attributes, or defects due to Fortran’s unspecified expression evaluation order. We demonstrate the usefulness of our tool on a verification benchmark suite and kernels extracted from a real world application.


title: Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution)

authors:
Tong Wu
Peter Schrammel
Lucas C. Cordeiro

abstract: Abstract We describe and evaluate a violation-witness validator for Java verifiers called Wit4Java. It takes a Java program with a safety property and the respective violation-witness output by a Java verifier to generate a new Java program whose execution deterministically violates the property. We extract the value of the program variables from the counterexample represented by the violation-witness and feed this information back into the original program. In addition, we have two implementations for instantiating source programs by injecting counterexamples. Experimental results show that Wit4Java can correctly validate the violation-witnesses produced by JBMC and GDart in a few seconds.


title: Efficient Neural Network Analysis with Sum-of-Infeasibilities

authors:
Haoze Wu
Aleksandar Zeljic
Guy Katz
Clark W. Barrett

abstract: Abstract Inspired by sum-of-infeasibilities methods in convex optimization, we propose a novel procedure for analyzing verification queries on neural networks with piecewise-linear activation functions. Given a convex relaxation which over-approximates the non-convex activation functions, we encode the violations of activation functions as a cost function and optimize it with respect to the convex relaxation. The cost function, referred to as the Sum-of-Infeasibilities (SoI), is designed so that its minimum is zero and achieved only if all the activation functions are satisfied. We propose a stochastic procedure, , to efficiently minimize the SoI. An extension to a canonical case-analysis-based complete search procedure can be achieved by replacing the convex procedure executed at each search state with . Extending the complete search with achieves multiple simultaneous goals: 1) it guides the search towards a counter-example; 2) it enables more informed branching decisions; and 3) it creates additional opportunities for bound derivation. An extensive evaluation across different benchmarks and solvers demonstrates the benefit of the proposed techniques. In particular, we demonstrate that SoI significantly improves the performance of an existing complete search procedure. Moreover, the SoI-based implementation outperforms other state-of-the-art complete verifiers. We also show that our technique can efficiently improve upon the perturbation bound derived by a recent adversarial attack algorithm.


title: A Theoretical Analysis of Random Regression Test Prioritization

authors:
Pu Yi
Hao Wang
Tao Xie
Darko Marinov
Wing Lam

abstract: Abstract Regression testing is an important activity to check software changes by running the tests in a test suite to inform the developers whether the changes lead to test failures. Regression test prioritization (RTP) aims to inform the developers faster by ordering the test suite so that tests likely to fail are run earlier. Many RTP techniques have been proposed and are often compared with the random RTP baseline by sampling some of the n! different test-suite orders for a test suite with n tests. However, there is no theoretical analysis of random RTP. We present such an analysis, deriving probability mass functions and expected values for metrics and scenarios commonly used in RTP research. Using our analysis, we revisit some of the most highly cited RTP papers and find that some presented results may be due to insufficient sampling. Future RTP research can leverage our analysis and need not use random sampling but can use our simple formulas or algorithms to more precisely compare with random RTP.


title: Verified First-Order Monitoring with Recursive Rules

authors:
Sheila Zingg
Srdan Krstic
Martin Raszyk
Joshua Schneider
Dmitriy Traytel

abstract: Abstract First-order temporal logics and rule-based formalisms are two popular families of specification languages for monitoring. Each family has its advantages and only few monitoring tools support their combination. We extend metric first-order temporal logic (MFOTL) with a recursive let construct, which enables interleaving rules with temporal logic formulas. We also extend VeriMon, an MFOTL monitor whose correctness has been formally verified using the Isabelle proof assistant, to support the new construct. The extended correctness proof covers the interaction of the new construct with the existing verified algorithm, which is subtle due to the presence of the bounded future temporal operators. We demonstrate the recursive let’s usefulness on several example specifications and evaluate our verified algorithm’s performance against the DejaVu monitoring tool.


title: Maximizing Branch Coverage with Constrained Horn Clauses

authors:
Ilia Zlatkin
Grigory Fedyukovich

abstract: Abstract State-of-the-art solvers for constrained Horn clauses (CHC) are successfully used to generate reachability facts from symbolic encodings of programs. In this paper, we present a new application to test-case generation: if a block of code is provably unreachable, no test case can be generated allowing to explore other blocks of code. Our new approach uses CHC to incrementally construct different program unrollings and extract test cases from models of satisfiable formulas. At the same time, a CHC solver keeps track of CHCs that represent unreachable blocks of code which makes the unrolling process more efficient. In practice, this lets our approach to terminate early while guaranteeing maximal coverage. Our implementation called Horntinuum exhibits promising performance: it generates high coverage in the majority of cases and spends less time on average than state-of-the-art.


title: Parameterized Verification under TSO with Data Types

authors:
Parosh Aziz Abdulla
Mohamed Faouzi Atig
Florian Furbach
Adwait Amit Godbole
Yacoub G. Hendi
Shankara Narayanan Krishna
Stephan Spengler

abstract: Abstract We consider parameterized verification of systems executing according to the total store ordering (TSO) semantics. The processes manipulate abstract data types over potentially infinite domains. We present a framework that translates the reachability problem for such systems to the reachability problem for register machines enriched with the given abstract data type.


title: Optimal Stateless Model Checking for Causal Consistency

authors:
Parosh Aziz Abdulla
Mohamed Faouzi Atig
S. Krishna
Ashutosh Gupta
Omkar Tuppe

abstract: Abstract We present a framework for efficient stateless model checking (SMC) of concurrent programs under three prominent models of causal consistency, $${\texttt {CCv}}, {\texttt {CM}}, \texttt{CC}$$ CCv , CM , CC . Our approach is based on exploring traces under the program order "Image missing" and the reads from "Image missing" relations. Our SMC algorithm is provably optimal in the sense that it explores each "Image missing" and "Image missing" relation exactly once. We have implemented our framework in a tool called Conschecker . Experiments show that Conschecker performs well in detecting anomalies in classical distributed databases benchmarks.


title: A Matrix-Based Approach to Parity Games

authors:
Saksham Aggarwal
Alejandro Stuckey de la Banda
Luke Yang
Julian Gutierrez

abstract: Abstract Parity games are two-player zero-sum games of infinite duration played on finite graphs for which no solution in polynomial time is still known. Solving a parity game is an $$\text{ NP }\cap \text{ co-NP }$$ NP ∩ co-NP problem, with the best worst-case complexity algorithms available in the literature running in quasi-polynomial time. Given the importance of parity games within automated formal verification, several practical solutions have been explored showing that considerably large parity games can be solved somewhat efficiently. Here, we propose a new approach to solving parity games guided by the efficient manipulation of a suitable matrix-based representation of the games. Our results show that a sequential implementation of our approach offers very competitive performance, while a parallel implementation using GPUs outperforms the current state-of-the-art techniques. Our study considers both real-world benchmarks of structured games as well as parity games randomly generated. We also show that our matrix-based approach retains the optimal complexity bounds of the best recursive algorithm to solve large parity games in practice.


title: Inferring Needless Write Memory Accesses on Ethereum Bytecode

authors:
Elvira Albert
Jesús Correas
Pablo Gordillo
Guillermo Román-Díez
Albert Rubio

abstract: Abstract Efficiency is a fundamental property of any type of program, but it is even more so in the context of the programs executing on the blockchain (known as smart contracts ). This is because optimizing smart contracts has direct consequences on reducing the costs of deploying and executing the contracts, as there are fees to pay related to their bytes-size and to their resource consumption (called gas ). Optimizing memory usage is considered a challenging problem that, among other things, requires a precise inference of the memory locations being accessed. This is also the case for the Ethereum Virtual Machine (EVM) bytecode generated by the most-widely used compiler, , whose rather unconventional and low-level memory usage challenges automated reasoning. This paper presents a static analysis, developed at the level of the EVM bytecode generated by , that infers write memory accesses that are needless and thus can be safely removed. The application of our implementation on more than 19,000 real smart contracts has detected about 6,200 needless write accesses in less than 4 hours. Interestingly, many of these writes were involved in memory usage patterns generated by that can be greatly optimized by removing entire blocks of bytecodes. To the best of our knowledge, existing optimization tools cannot infer such needless write accesses, and hence cannot detect these inefficiencies that affect both the deployment and the execution costs of Ethereum smart contracts.


title: EBF 4.2: Black-Box Cooperative Verification for Concurrent Programs - (Competition Contribution)

authors:
Fatimah Aljaafari
Fedor Shmarov
Edoardo Manino
Rafael Menezes
Lucas C. Cordeiro

abstract: Abstract Combining different verification and testing techniques together could, at least in theory, achieve better results than each individual one on its own. The challenge in doing so is how to take advantage of the strengths of each technique while compensating for their weaknesses. EBF 4.2 addresses this challenge for concurrency vulnerabilities by creating Ensembles of Bounded model checkers and gray-box Fuzzers. In contrast with portfolios, which simply run all possible techniques in parallel, EBF strives to obtain closer cooperation between them. This goal is achieved in a black-box fashion. On the one hand, the model checkers are forced to provide seeds to the fuzzers by injecting additional vulnerabilities in the program under test. On the other hand, off-the-shelf fuzzers are forced to explore different interleavings by adding lightweight instrumentation and systematically re-seeding them.


title: Verifying Learning-Based Robotic Navigation Systems

authors:
Guy Amir
Davide Corsi
Raz Yerushalmi
Luca Marzari
David Harel
Alessandro Farinelli
Guy Katz

abstract: Abstract Deep reinforcement learning (DRL) has become a dominant deep-learning paradigm for tasks where complex policies are learned within reactive systems. Unfortunately, these policies are known to be susceptible to bugs. Despite significant progress in DNN verification, there has been little work demonstrating the use of modern verification tools on real-world, DRL-controlled systems. In this case study, we attempt to begin bridging this gap, and focus on the important task of mapless robotic navigation — a classic robotics problem, in which a robot, usually controlled by a DRL agent, needs to efficiently and safely navigate through an unknown arena towards a target. We demonstrate how modern verification engines can be used for effective model selection , i.e., selecting the best available policy for the robot in question from a pool of candidate policies. Specifically, we use verification to detect and rule out policies that may demonstrate suboptimal behavior, such as collisions and infinite loops. We also apply verification to identify models with overly conservative behavior, thus allowing users to choose superior policies, which might be better at finding shorter paths to a target. To validate our work, we conducted extensive experiments on an actual robot, and confirmed that the suboptimal policies detected by our method were indeed flawed. We also demonstrate the superiority of our verification-driven approach over state-of-the-art, gradient attacks. Our work is the first to establish the usefulness of DNN verification in identifying and filtering out suboptimal DRL policies in real-world robots, and we believe that the methods presented here are applicable to a wide range of systems that incorporate deep-learning-based agents.


title: Computing Adequately Permissive Assumptions for Synthesis

authors:
Ashwani Anand
Kaushik Mallik
Satya Prakash Nayak
Anne-Kathrin Schmuck

abstract: Abstract We automatically compute a new class of environment assumptions in two-player turn-based finite graph games which characterize an “adequate cooperation” needed from the environment to allow the system player to win. Given an $$\omega $$ -regular winning condition $$\varPhi $$ for the system player, we compute an $$\omega $$ -regular assumption $$\varPsi $$ for the environment player, such that (i) every environment strategy compliant with $$\varPsi $$ allows the system to fulfill $$\varPhi $$ (sufficiency), (ii) $$\varPsi $$ can be fulfilled by the environment for every strategy of the system (implementability), and (iii) $$\varPsi $$ does not prevent any cooperative strategy choice (permissiveness). For parity games, which are canonical representations of $$\omega $$ -regular games, we present a polynomial-time algorithm for the symbolic computation of adequately permissive assumptions and show that our algorithm runs faster and produces better assumptions than existing approaches—both theoretically and empirically. To the best of our knowledge, for $$\omega $$ -regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive.


title: Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format

authors:
Bruno Andreotti
Hanna Lachnitt
Haniel Barbosa

abstract: Abstract Proofs from SMT solvers ensure correctness independently from implementation, which is often a requirement when solvers are used in safety-critical applications or proof assistants. Alethe is an established SMT proof format generated by the solvers veriT and cvc5, with reconstruction support in the proof assistants Isabelle/HOL and Coq. The format is close to SMT-LIB and allows both coarse- and fine-grained steps, facilitating proof production. However, it lacks a stand-alone checker, which harms its usability and hinders its adoption. Moreover, the coarse-grained steps can be too expensive to check and lead to verification failures. We present Carcara , an independent proof checker and elaborator for Alethe, implemented in Rust. It aims to increase the adoption of the format by providing push-button proof-checking for Alethe proofs, focusing on efficiency and usability; and by providing elaboration for coarse-grained steps into fine-grained ones, increasing the potential success rate of checking Alethe proofs in performance-critical validators, such as proof assistants. We evaluate Carcara over a large set of Alethe proofs generated from SMT-LIB problems and show that it has good performance and its elaboration techniques can make proofs easier to check.


title: Context-Sensitive Meta-Constraint Systems for Explainable Program Analysis

authors:
Kalmer Apinis
Vesal Vojdani

abstract: Abstract We show how to generate a constraint system of symbolic expressions as part of an inter-procedural constraint-system–based program analysis such that any chosen slice of the intended analysis may be computed through the evaluation of the symbolic constraints. Thus, our method ensures that the computed expressions provide genuine explanations for the chosen analysis slice. The resulting system is then annotated with program location information, translated into closed-form expressions, and simplified to yield a human-readable justification for the analyzer’s verdict. Justifications are given using program locations, constants from the program, abstract lattice operations, loops in the analysis, and computed results.


title: Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation - (Competition Contribution)

authors:
Paulína Ayaziová
Jan Strejcek

abstract: Abstract The new version of the witness validator Symbiotic-Witch follows more precisely the (fixed version of the) semantics of verification witnesses. This makes the tool more efficient as it can benefit from sink nodes. Further, the tool can now refute a witness. To sum up, Symbiotic-Witch 2 can confirm or refute violation witnesses of reachability safety, memory safety, memory cleanup, and overflow properties of sequential C programs.


title: Stack-Aware Hyperproperties

authors:
Ali Bajwa
Minjian Zhang
Rohit Chadha
Mahesh Viswanathan

abstract: Abstract A hyperproperty relates executions of a program and is used to formalize security objectives such as confidentiality, non-interference, privacy, and anonymity. Formally, a hyperproperty is a collection of allowable sets of executions. A program violates a hyperproperty if the set of its executions is not in the collection specified by the hyperproperty. The logic HyperCTL* has been proposed in the literature to formally specify and verify hyperproperties. The problem of checking whether a finite-state program satisfies a HyperCTL* formula is known to be decidable. However, the problem turns out to be undecidable for procedural (recursive) programs. Surprisingly, we show that decidability can be restored if we consider restricted classes of hyperproperties, namely those that relate only those executions of a program which have the same call-stack access pattern. We call such hyperproperties, stack-aware hyperproperties. Our decision procedure can be used as a proof method for establishing security objectives such as noninference for recursive programs, and also for refuting security objectives such as observational determinism. Further, if the call stack size is observable to the attacker, the decision procedure provides exact verification.


title: LTL Reactive Synthesis with a Few Hints

authors:
Mrudula Balachander
Emmanuel Filiot
Jean-François Raskin

abstract: Abstract We study a variant of the problem of synthesizing Mealy machines that enforce LTL specifications against all possible behaviours of the environment, including hostile ones. In the variant studied here, the user provides the high level LTL specification $$\varphi $$ of the system to design, and a setEof examples of executions that the solution must produce. Our synthesis algorithm first generalizes the user-provided examples inEusing tailored extensions of automata learning algorithms, while preserving realizability of $$\varphi $$ . Second, it turns the (usually) incomplete Mealy machine obtained by the learning phase into a complete Mealy machine realizing $$\varphi $$ . The examples are used to guide the synthesis procedure. We prove learnability guarantees of our algorithm and prove that our problem, while generalizing the classical LTL synthesis problem, matches its worst-case complexity. The additional cost of learning fromEis even polynomial in the size ofEand in the size of a symbolic representation of solutions that realize $$\varphi $$ , computed by the synthesis toolAcacia-Bonzai. We illustrate the practical interest of our approach on a set of examples.


title: Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks

authors:
Shahaf Bassan
Guy Katz

abstract: Abstract With the rapid growth of machine learning, deep neural networks (DNNs) are now being used in numerous domains. Unfortunately, DNNs are “black-boxes”, and cannot be interpreted by humans, which is a substantial concern in safety-critical systems. To mitigate this issue, researchers have begun working on explainable AI (XAI) methods, which can identify a subset of input features that are the cause of a DNN’s decision for a given input. Most existing techniques are heuristic, and cannot guarantee the correctness of the explanation provided. In contrast, recent and exciting attempts have shown that formal methods can be used to generate provably correct explanations. Although these methods are sound, the computational complexity of the underlying verification problem limits their scalability; and the explanations they produce might sometimes be overly complex. Here, we propose a novel approach to tackle these limitations. We (i) suggest an efficient, verification-based method for finding minimal explanations , which constitute a provable approximation of the global, minimum explanation; (ii) show how DNN verification can assist in calculating lower and upper bounds on the optimal explanation; (iii) propose heuristics that significantly improve the scalability of the verification process; and (iv) suggest the use of bundles , which allows us to arrive at more succinct and interpretable explanations. Our evaluation shows that our approach significantly outperforms state-of-the-art techniques, and produces explanations that are more useful to humans. We thus regard this work as a step toward leveraging verification technology in producing DNNs that are more reliable and comprehensible.


title: Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants

authors:
Kevin Batz
Mingshuai Chen
Sebastian Junges
Benjamin Lucien Kaminski
Joost-Pieter Katoen
Christoph Matheja

abstract: Abstract Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite expected runtime. We contribute a simple yet effective inductive synthesis approach for proving such quantitative reachability properties by generating inductive invariants on source-code level . Our implementation shows promise: It finds invariants for (in)finite-state programs, can beat state-of-the-art probabilistic model checkers, and is competitive with modern tools dedicated to invariant synthesis and expected runtime reasoning.


title: Verified reductions for optimization

authors:
Alexander Bentkamp
Ramon Fernández Mir
Jeremy Avigad

abstract: Abstract Numerical and symbolic methods for optimization are used extensively in engineering, industry, and finance. Various methods are used to reduce problems of interest to ones that are amenable to solution by these methods. We develop a framework for designing and applying such reductions, using the Lean programming language and interactive proof assistant. Formal verification makes the process more reliable, and the availability of an interactive framework and ambient mathematical library provides a robust environment for constructing the reductions and reasoning about them.


title: AutoHyper: Explicit-State Model Checking for HyperLTL

authors:
Raven Beutner
Bernd Finkbeiner

abstract: Abstract HyperLTL is a temporal logic that can express hyperproperties, i.e., properties that relate multiple execution traces of a system. Such properties are becoming increasingly important and naturally occur, e.g., in information-flow control, robustness, mutation testing, path planning, and causality checking. Thus far, complete model checking tools for HyperLTL have been limited to alternation-free formulas, i.e., formulas that use only universal or only existential trace quantification. Properties involving quantifier alternations could only be handled in an incomplete way, i.e., the verification might fail even though the property holds. In this paper, we present , an explicit-state automata-based model checker that supports full HyperLTL and is complete for properties with arbitrary quantifier alternations. We show that language inclusion checks can be integrated into HyperLTL verification, which allows to benefit from a range of existing inclusion-checking tools. We evaluate on a broad set of benchmarks drawn from different areas in the literature and compare it with existing (incomplete) methods for HyperLTL verification.


title: Competition on Software Verification and Witness Validation: SV-COMP 2023

abstract: Abstract The 12th edition of the Competition on Software Verification (SV-COMP 2023) is again the largest overview of tools for software verification, evaluating 52 verification systems from 34 teams from 10 countries. Besides providing an overview of the state of the art in automatic software verification, the goal of the competition is to establish standards, provide a platform for exchange to developers of such tools, educate PhD students on reproducibility approaches and benchmarking, and provide computing resources to developers that do not have access to compute clusters. The competition consisted of 23 805 verification tasks for C programs and 586 verification tasks for Java programs. The specifications include reachability, memory safety, overflows, and termination. This year, the competition introduced a new competition track on witness validation, where validators for verification witnesses are evaluated with respect to their quality.


title: Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Translator

authors:
Dirk Beyer
Po-Chun Chien
Nian-Ze Lee

abstract: Abstract Across the broad research field concerned with the analysis of computational systems, research endeavors are often categorized by the respective models under investigation. Algorithms and tools are usually developed for a specific model, hindering their applications to similar problems originating from other computational systems. A prominent example of such a situation is the area of formal verification and testing for hardware and software systems. The two research communities share common theoretical foundations and solving methods, including satisfiability, interpolation, and abstraction refinement. Nevertheless, it is often demanding for one community to benefit from the advancements of the other, as analyzers typically assume a particular input format. To bridge the gap between the hardware and software analysis, we propose Btor2C, a translator from word-level sequential circuits to C programs. We choose the Btor2 language as the input format for its simplicity and bit-precise semantics. It can be deemed as an intermediate representation tailored for analysis. Given a Btor2 circuit, Btor2C generates a behaviorally equivalent program in the language C, supported by many static program analyzers. We demonstrate the use cases of Btor2C by translating the benchmark set from the Hardware Model Checking Competitions into C programs and analyze them by tools from the Intl. Competitions on Software Verification and Testing. Our results show that software analyzers can complement hardware verifiers for enhanced quality assurance: For example, the software verifier VeriAbs with Btor2C as preprocessor found more bugs than the best hardware verifiers ABC and AVR in our experiment.


title: Multiparty Session Typing in Java, Deductively

authors:
Jelle Bouma
Stijn de Gouw
Sung-Shik Jongmans

abstract: Abstract Multiparty session typing (MPST) is a method to automatically prove safety and liveness of protocol implementations relative to specifications. We present BGJ: a new tool to apply the MPST method in combination with Java. The checks performed using our tool are purely static (all errors are reported early at compile-time) and resource-efficient (near-zero cost abstractions at run-time), thereby addressing two issues of existing tools. BGJ is built using VerCors, but our approach is general.


title: Validating Streaming JSON Documents with Learned VPAs

authors:
Véronique Bruyère
Guillermo A. Pérez
Gaëtan Staquet

abstract: Abstract We present a new streaming algorithm to validate JSON documents against a set of constraints given as a JSON schema. Among the possible values a JSON document can hold, objects are unordered collections of key-value pairs while arrays are ordered collections of values. We prove that there always exists a visibly pushdown automaton (VPA) that accepts the same set of JSON documents as a JSON schema. Leveraging this result, our approach relies on learning a VPA for the provided schema. As the learned VPA assumes a fixed order on the key-value pairs of the objects, we abstract its transitions in a special kind of graph, and propose an efficient streaming algorithm using the VPA and its graph to decide whether a JSON document is valid for the schema. We evaluate the implementation of our algorithm on a number of random JSON documents, and compare it to the classical validation algorithm.


title: Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability

authors:
Michaël Cadilhac
Guillermo A. Pérez

abstract: Abstract We describe our implementation of downset-manipulating algorithms used to solve the realizability problem for linear temporal logic (LTL). These algorithms were introduced by Filiot et al. in the 2010s and implemented in the tools Acacia and Acacia+ in C and Python. We identify degrees of freedom in the original algorithms and provide a complete rewriting of Acacia in C++20 articulated around genericity and leveraging modern techniques for better performance. These techniques include compile-time specialization of the algorithms, the use of SIMD registers to store vectors, and several preprocessing steps, some relying on efficient Binary Decision Diagram (BDD) libraries. We also explore different data structures to store downsets. The resulting tool is competitive against comparable modern tools.


title: Bubaak: Runtime Monitoring of Program Verifiers - (Competition Contribution)

authors:
Marek Chalupa
Thomas A. Henzinger

abstract: Abstract The main idea behind Bubaak is to run multiple program analyses in parallel and use runtime monitoring and enforcement to observe and control their progress in real time. The analyses send information about (un)explored states of the program and discovered invariants to a monitor. The monitor processes the received data and can force an analysis to stop the search of certain program parts (which have already been analyzed by other analyses), or to make it utilize a program invariant found by another analysis. At SV-COMP 2023, the implementation of data exchange between the monitor and the analyses was not yet completed, which is why Bubaak only ran several analyses in parallel, without any coordination. Still, Bubaak won the meta-category FalsificationOverall and placed very well in several other (sub)-categories of the competition.


title: A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems

authors:
Krishnendu Chatterjee
Thomas A. Henzinger
Mathias Lechner
Dorde Zikelic

abstract: Abstract Reinforcement learning has received much attention for learning controllers of deterministic systems. We consider a learner-verifier framework for stochastic control systems and survey recent methods that formally guarantee a conjunction of reachability and safety properties. Given a property and a lower bound on the probability of the property being satisfied, our framework jointly learns a control policy and a formal certificate to ensure the satisfaction of the property with a desired probability threshold. Both the control policy and the formal certificate are continuous functions from states to reals, which are learned as parameterized neural networks. While in the deterministic case, the certificates are invariant and barrier functions for safety, or Lyapunov and ranking functions for liveness, in the stochastic case the certificates are supermartingales. For certificate verification, we use interval arithmetic abstract interpretation to bound the expected values of neural network functions.


title: EVA: a Tool for the Compositional Verification of AUTOSAR Models

authors:
Alessandro Cimatti
Luca Cristoforetti
Alberto Griggio
Stefano Tonetta
Sara Corfini
Marco Di Natale
Florian Barrau

abstract: Abstract We present , a framework for the integration of modern verification tools in the context of AUTOSAR, a widely-used open standard for the development of automotive software systems. Our framework enables the automatic end-to-end verification of system-level properties using a compositional approach. It combines software model checking techniques for the verification of software components at the code level with a contract-based analysis for verifying their correct composition. In this paper, we present the tool through its application on a representative automotive case study, discussing the main functionalities provided and the results obtained.


title: New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization

authors:
João Cortes
Inês Lynce
Vasco Manquinho

abstract: Abstract In the last decade, numerous algorithms for single-objective Boolean optimization have been proposed that rely on the iterative usage of a highly effective Propositional Satisfiability (SAT) solver. But the use of SAT solvers in Multi-Objective Combinatorial Optimization (MOCO) algorithms is still scarce. Due to this shortage of efficient tools for MOCO, many real-world applications formulated as multi-objective are simplified to single-objective, using either a linear combination or a lexicographic ordering of the objective functions to optimize. In this paper, we extend the state of the art of MOCO solvers with two novel unsatisfiability-based algorithms. The first is a core-guided MOCO solver. The second is a hitting set-based MOCO solver. Experimental results in several sets of benchmark instances show that our new unsatisfiability-based algorithms can outperform state-of-the-art SAT-based algorithms for MOCO.


title: VeriAbsL: Scalable Verification by Abstraction and Strategy Prediction (Competition Contribution)

authors:
Priyanka Darke
Bharti Chimdyalwar
Sakshi Agrawal
Shrawan Kumar
R. Venkatesh
Supratik Chakraborty

abstract: Abstract We present VeriAbsL, a reachability verifier that performs verification in three stages. First, it slices the input code using a combination of two slicers, then it verifies the slices using predicted strategies, and at last, it composes the result of verifying the individual slices. We introduce a novel shallow slicing technique that uses variable reference information of the program, and data and control dependencies of the entry function to generate slices. We also introduce a novel strategy prediction technique that uses machine learning to predict a strategy. It uses boolean features to describe a program to a neural network that predicts a strategy. We use the portfolio of VeriAbs, a reachabiltiy verifier with manually defined strategies. In sv-comp 2023, VeriAbsL verified 227 (Without witness validation.) more programs than VeriAbs, and 475 (Without witness validation.) programs that VeriAbs could not verify.


title: Industrial-Strength Controlled Concurrency Testing for sc C tt # Programs with sc Coyote

authors:
Pantazis Deligiannis
Aditya Senthilnathan
Fahad Nayyar
Chris Lovett
Akash Lal

abstract: Abstract This paper describes the design and implementation of the open-source tool $$\textsc {Coyote} $$ for testing concurrent programs written in the $$\textsc {C}{} \texttt {\#} $$ language. $$\textsc {Coyote} $$ provides algorithmic capabilities to explore the state-space of interleavings of a concurrent program, with deterministic repro for any bug that it finds. $$\textsc {Coyote} $$ encapsulates multiple ideas from the research community to offer state-of-the-art testing for $$\textsc {C}{} \texttt {\#} $$ programs, as well as an efficiently engineered implementation that has been shown robust enough to support industrial use.


title: Specifying and Verifying Higher-order Rust Iterators

authors:
Xavier Denis
Jacques-Henri Jourdan

abstract: Abstract In Rust, programs are often written using iterators, but these pose problems for verification: they are non-deterministic, infinite, and often higher-order, effectful and built using adapters. We present a general framework for specifying and reasoning with Rust iterators in first-order logic. Our approach is capable of addressing the challenges set out above, which we demonstrate by verifying real Rust iterators, including a higher-order, effectful . Using the Creusot verification platform, we evaluate our framework on clients of iterators, showing it leads to efficient verification of complex functional properties.


title: Ultimate Taipan and Race Detection in Ultimate - (Competition Contribution)

authors:
Daniel Dietsch
Matthias Heizmann
Dominik Klumpp
Frank Schüssele
Andreas Podelski

abstract: Abstract Ultimate Taipan integrates trace abstraction with algebraic program analysis on path programs. Taipan supports data race checking in concurrent programs through a reduction to reachability checking. Though the subsequent verification is not tuned for data race checking, the results are encouraging.


title: Antichains Algorithms for the Inclusion Problem Between ømega-VPL

authors:
Kyveli Doveri
Pierre Ganty
Luka Hadzi-Dokic

abstract: Abstract We define novel algorithms for the inclusion problem between two visibly pushdown languages of infinite words, an EXPTime -complete problem. Our algorithms search for counterexamples to inclusion in the form of ultimately periodic words i.e. words of the form $$uv^{\omega }$$ u v ω where $$u$$ u and $$v$$ v are finite words. They are parameterized by a pair of quasiorders telling which ultimately periodic words need not be tested as counterexamples to inclusion without compromising completeness. The pair of quasiorders enables distinct reasoning for prefixes and periods of ultimately periodic words thereby allowing to discard even more words compared to using the same quasiorder for both. We put forward two families of quasiorders: the state-based quasiorders based on automata and the syntactic quasiorders based on languages. We also implemented our algorithm and conducted an empirical evaluation on benchmarks from software verification.


title: Korn - Software Verification with Horn Clauses (Competition Contribution)

abstract: Abstract Korn is a software verifier that infers correctness certificates and violation witnesses sutomatically using state-of-the-art Horn-clause solvers, such as Z3 and Eldarica. The solvers are used in a portfolio together with cheap random sampling where the latter can be very effective at finding counterexamples. Korn perfomend best in the sub-category of SV-COMP 2023.


title: WASIM: A Word-level Abstract Symbolic Simulation Framework for Hardware Formal Verification

authors:
Wenji Fang
Hongce Zhang

abstract: Abstract This paper demonstrates the design and usage of WASIM, a word-level abstract symbolic simulation framework with pluggable abstraction/refinement functions. WASIM is useful in the formal verification of functional properties on register-transfer level (RTL) hardware designs. Users can control the symbolic simulation process and tune the level of abstraction by interacting with WASIM through its Python API. WASIM can be used to directly check formal properties on symbolic traces or to extract useful fragments from symbolic representations to construct safe inductive invariants as a correctness certificate. We demonstrate the utility of WASIM on the verification of two pipelined hardware designs. WASIM and the case studies are available under open-source license at: [9].


title: Eclipse ESCET™: The Eclipse Supervisory Control Engineering Toolkit

authors:
Wan J. Fokkink
Martijn A. Goorden
Dennis Hendriks
D. A. van Beek
Albert T. Hofkamp
Ferdie F. H. Reijnen
L. F. P. Etman
Lars Moormann
Joanna M. van de Mortel-Fronczak
Michel A. Reniers
Jacobus E. Rooda
Bram van der Sanden
Ramon R. H. Schiffelers
Sander Thuijsman
J. J. Verbakel
J. A. Vogel

abstract: Abstract The Eclipse Supervisory Control Engineering Toolkit (ESCET™) is an open-source project to provide a model-based approach and toolkit for developing supervisory controllers, targeting their entire engineering process. It supports synthesis-based engineering of supervisory controllers for discrete-event systems, combining model-based engineering with computer-aided design to automatically generate correct-by-construction controllers. At its heart is supervisory controller synthesis, a formal technique for the automatic derivation of supervisory controllers from the unrestricted system behavior and system requirements. Vital for the future development of these techniques and tools is the ESCET project’s open environment, allowing industry and academia to collaborate on creating an industrial-strength toolkit. We report on some crucial developments of the toolkit in the context of research projects with Rijkswaterstaat and ASML that have considerably improved its capability to deal with the complexity of real-life systems as well as its usability.


title: Active Learning for SAT Solver Benchmarking

authors:
Tobias Fuchs
Jakob Bach
Ashlin Iser

abstract: Abstract Benchmarking is a crucial phase when developing algorithms. This also applies to solvers for the SAT (propositional satisfiability) problem. Benchmark selection is about choosing representative problem instances that reliably discriminate solvers based on their runtime. In this paper, we present a dynamic benchmark selection approach based on active learning. Our approach predicts the rank of a new solver among its competitors with minimum runtime and maximum rank prediction accuracy. We evaluated this approach on the Anniversary Track dataset from the 2022 SAT Competition. Our selection approach can predict the rank of a new solver after about 10 % of the time it would take to run the solver on all instances of this dataset, with a prediction accuracy of about 92 %. We also discuss the importance of instance families in the selection process. Overall, our tool provides a reliable way for solver engineers to determine a new solver’s performance efficiently.


title: OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural Networks

authors:
Xingwu Guo
Ziwei Zhou
Yueling Zhang
Guy Katz
Min Zhang

abstract: Abstract Occlusion is a prevalent and easily realizable semantic perturbation to deep neural networks (DNNs). It can fool a DNN into misclassifying an input image by occluding some segments, possibly resulting in severe errors. Therefore, DNNs planted in safety-critical systems should be verified to be robust against occlusions prior to deployment. However, most existing robustness verification approaches for DNNs are focused on non-semantic perturbations and are not suited to the occlusion case. In this paper, we propose the first efficient, SMT-based approach for formally verifying the occlusion robustness of DNNs. We formulate the occlusion robustness verification problem and prove it is NP-complete. Then, we devise a novel approach for encoding occlusions as a part of neural networks and introduce two acceleration techniques so that the extended neural networks can be efficiently verified using off-the-shelf, SMT-based neural network verification tools. We implement our approach in a prototype called OccRob and extensively evaluate its performance on benchmark datasets with various occlusion variants. The experimental results demonstrate our approach’s effectiveness and efficiency in verifying DNNs’ robustness against various occlusions, and its ability to generate counterexamples when these DNNs are not robust.


title: Mungojerrie: Linear-Time Objectives in Model-Free Reinforcement Learning

authors:
Ernst Moritz Hahn
Mateo Perez
Sven Schewe
Fabio Somenzi
Ashutosh Trivedi
Dominik Wojtczak

abstract: Abstract Mungojerrie is an extensible tool that provides a framework to translate linear-time objectives into reward for reinforcement learning (RL). The tool provides convergent RL algorithms for stochastic games, reference implementations of existing reward translations for $$\omega $$ ω -regular objectives, and an internal probabilistic model checker for $$\omega $$ ω -regular objectives. This functionality is modular and operates on shared data structures, which enables fast development of new translation techniques. Mungojerrie supports finite models specified in PRISM and $$\omega $$ ω -automata specified in the HOA format, with an integrated command line interface to external linear temporal logic translators. Mungojerrie is distributed with a set of benchmarks for $$\omega $$ ω -regular objectives in RL.


title: Lockstep Composition for Unbalanced Loops

authors:
Ameer Hamza
Grigory Fedyukovich

abstract: Abstract Equivalence checking of two programs is often reduced to the safety verification of a so-called product program that aligns the programs in lockstep. However, this strategy is not applicable when programs have arbitrary loop structures, e.g., the numbers of loops vary. We introduce an automatic iterative abstraction-refinement-based technique for checking equivalence of a single-loop program and a program which has a series of consecutive loops. Our approach decomposes the single loop into a sequence of separate loops thus reducing the main problem to a series of equivalence-checking problems for pairs of loops. Since due to the decomposition, these problems become abstract, our approach iteratively refines the decomposed loops and lifts useful information across them. Our second contribution is a procedure for the alignment of loops with counters and explicit bounds that cannot be composed in lockstep. We have implemented the approach and successfully evaluated it on two suites, one with benchmarks containing different numbers of loops and the other containing benchmarks that need alignment.


title: A Practitioner's Guide to MDP Model Checking Algorithms

authors:
Arnd Hartmanns
Sebastian Junges
Tim Quatmann
Maximilian Weininger

abstract: Abstract Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) is key for the verification of systems that act under uncertainty. Popular algorithms are policy iteration and variants of value iteration; in tool competitions, most participants rely on the latter. These algorithms generally need worst-case exponential time. However, the problem can equally be formulated as a linear program, solvable in polynomial time. In this paper, we give a detailed overview of today’s state-of-the-art algorithms for MDP model checking with a focus on performance and correctness. We highlight their fundamental differences, and describe various optimizations and implementation variants. We experimentally compare floating-point and exact-arithmetic implementations of all algorithms on three benchmark sets using two probabilistic model checkers. Our results show that (optimistic) value iteration is a sensible default, but other algorithms are preferable in specific settings. This paper thereby provides a guide for MDP verification practitioners—tool builders and users alike.


title: Modular Mix-and-Match Complementation of Büchi Automata

authors:
Vojtech Havlena
Ondrej Lengál
Yong Li
Barbora Smahlíková
Andrea Turrini

abstract: Abstract Complementation of nondeterministic Büchi automata (BAs) is an important problem in automata theory with numerous applications in formal verification, such as termination analysis of programs, model checking, or in decision procedures of some logics. We build on ideas from a recent work on BA determinization by Li et al. and propose a new modular algorithm for BA complementation. Our algorithm allows to combine several BA complementation procedures together, with one procedure for a subset of the BA’s strongly connected components (SCCs). In this way, one can exploit the structure of particular SCCs (such as when they are inherently weak or deterministic) and use more efficient specialized algorithms, regardless of the structure of the whole BA. We give a general framework into which partial complementation procedures can be plugged in, and its instantiation with several algorithms. The framework can, in general, produce a complement with an Emerson-Lei acceptance condition, which can often be more compact. Using the algorithm, we were able to establish an exponentially better new upper bound of $$\mathcal {O}(4^n)$$ O ( 4 n ) for complementation of the recently introduced class of elevator automata. We implemented the algorithm in a prototype and performed a comprehensive set of experiments on a large set of benchmarks, showing that our framework complements well the state of the art and that it can serve as a basis for future efficient BA complementation and inclusion checking algorithms.


title: Taming Large Bounds in Synthesis from Bounded-Liveness Specifications

authors:
Philippe Heim
Rayna Dimitrova

abstract: Abstract Automatic synthesis from temporal logic specifications is an attractive alternative to manual system design, due to its ability to generate correct-by-construction implementations from high-level specifications. Due to the high complexity of the synthesis problem, significant research efforts have been directed at developing practically efficient approaches for restricted specification language fragments. In this paper we focus on the fragment of Linear Temporal Logic (LTL) syntactically extended with bounded temporal operators. We propose a new synthesis approach with the primary motivation to solve efficiently the synthesis problem for specifications with bounded temporal operators, in particular those with large bounds. The experimental evaluation of our method shows that for this type of specifications it outperforms state-of-art synthesis tools, demonstrating that it is a promising approach to efficiently treating quantitative timing constraints in safety specifications.


title: ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving

authors:
Maximilian Heisinger
Martina Seidl
Armin Biere

abstract: Abstract Over the last years, innovative parallel and distributed SAT solving techniques were presented that could impressively exploit the power of modern hardware and cloud systems. Two approaches were particularly successful: (1) search-space splitting in a Divide-and-Conquer (D &C) manner and (2) portfolio-based solving. The latter executes different solvers or configurations of solvers in parallel. For quantified Boolean formulas (QBFs), the extension of propositional logic with quantifiers, there is surprisingly little recent work in this direction compared to SAT. In this paper, we present ParaQooba , a novel framework for parallel and distributed QBF solving which combines D &C parallelization and distribution with portfolio-based solving. Our framework is designed in such a way that it can be easily extended and arbitrary sequential QBF solvers can be integrated out of the box, without any programming effort. We show how ParaQooba orchestrates the collaboration of different solvers for joint problem solving by performing an extensive evaluation on benchmarks from QBFEval’22, the most recent QBF competition.


title: Ultimate Automizer and the CommuHash Normal Form - (Competition Contribution)

authors:
Matthias Heizmann
Max Barth
Daniel Dietsch
Leonard Fichtner
Jochen Hoenicke
Dominik Klumpp
Mehdi Naouar
Tanja Schindler
Frank Schüssele
Andreas Podelski

abstract: Abstract The verification approach of Ultimate Automizer utilizes SMT formulas. This paper presents techniques to keep the size of the formulas small. We focus especially on a normal form, called CommuHash normal form that was easy to implement and had a significant impact on the runtime of our tool.


title: Bounded Model Checking for Asynchronous Hyperproperties

authors:
Tzu-Han Hsu
Borzoo Bonakdarpour
Bernd Finkbeiner
César Sánchez

abstract: Abstract Many types of attacks on confidentiality stem from the nondeterministic nature of the environment that computer programs operate in. We focus on verification of confidentiality in nondeterministic environments by reasoning about asynchronous hyperproperties . We generalize the temporal logic to allow nested trajectory quantification, where a trajectory determines how different execution traces may advance and stutter. We propose a bounded model checking algorithm for based on QBF-solving for a fragment of and evaluate it by various case studies on concurrent programs, scheduling attacks, compiler optimization, speculative execution, and cache timing attacks. We also rigorously analyze the complexity of model checking .