title: Efficient Loop Conditions for Bounded Model Checking Hyperproperties

authors:
Tzu-Han Hsu
César Sánchez
Sarai Sheinvald
Borzoo Bonakdarpour

abstract: Abstract Bounded model checking (BMC) is an effective technique for hunting bugs by incrementally exploring the state space of a system. To reason about infinite traces through a finite structure and to ultimately obtain completeness, BMC incorporates loop conditions that revisit previously observed states. This paper focuses on developing loop conditions for BMC of – a temporal logic for hyperproperties that allows expressing important policies for security and consistency in concurrent systems, etc. Loop conditions for are more complicated than for , as different traces may loop inconsistently in unrelated moments. Existing BMC approaches for only considered linear unrollings without any looping capability, which precludes both finding small infinite traces and obtaining a complete technique. We investigate loop conditions for BMC, for formulas that contain up to one quantifier alternation. We first present a general complete automata-based technique which is based on bounds of maximum unrollings. Then, we introduce alternative simulation-based algorithms that allow exploiting short loops effectively, generating SAT queries whose satisfiability guarantees the outcome of the original model checking problem. We also report empirical evaluation of the prototype implementation of our BMC techniques using .


venue: tacas

title: Feature Necessity & Relevancy in ML Classifier Explanations

authors:
Xuanxiang Huang
Martin C. Cooper
António Morgado
Jordi Planes
João Marques-Silva

abstract: Abstract Given a machine learning (ML) model and a prediction, explanations can be defined as sets of features which are sufficient for the prediction. In some applications, and besides asking for an explanation, it is also critical to understand whether sensitive features can occur in some explanation, or whether a non-interesting feature must occur in all explanations. This paper starts by relating such queries respectively with the problems of relevancy and necessity in logic-based abduction. The paper then proves membership and hardness results for several families of ML classifiers. Afterwards the paper proposes concrete algorithms for two classes of classifiers. The experimental results confirm the scalability of the proposed algorithms.


title: Java Ranger: Supporting String and Array Operations in Java Ranger (Competition Contribution)

authors:
Soha Hussein
Qiuchen Yan
Stephen McCamant
Vaibhav Sharma
Michael W. Whalen

abstract: Abstract Java Ranger is a path-merging tool for Java Programs. It identifies branching regions of code and summarizes them by generating a disjunctive logical constraint that describes the behavior of the code region. Previously, Java Ranger showed that a reduction of 70% of execution paths is possible when used to merge branching regions of code that support numeric constraints. In this paper, we describe the support of two additional features since participation in SV-COMP 2020: symbolic array and symbolic string operations. Finally, we present a preliminary evaluation of the effect of the structure of the disjunctive constraint on the solver’s performance. Results suggest that certain constraint structures can speed up the performance of Java Ranger.


title: Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification

authors:
Nouraldin Jaber
Christopher Wagner
Swen Jacobs
Milind Kulkarni
Roopsha Samanta

abstract: Abstract Distributed agreement-based (DAB) systems use common distributed agreement protocols such as leader election and consensus as building blocks for their target functionality. While automated verification for DAB systems is undecidable in general, recent work identifies a large class of DAB systems for which verification is efficiently-decidable. Unfortunately, the conditions characterizing such a class can be opaque and non-intuitive, and can pose a significant challenge to system designers trying to model their systems in this class. In this paper, we present a synthesis-driven tool, Cinnabar, to help system designers building DAB systems ensure that their intended designs belong to an efficiently-decidable class. In particular, starting from an initial sketch provided by the designer, Cinnabar generates sketch completions using a counterexample-guided procedure. The core technique relies on compactly encoding root-causes of counterexamples to varied properties such as efficient-decidability and safety. We demonstrate Cinnabar ’s effectiveness by successfully and efficiently synthesizing completions for a variety of interesting DAB systems including a distributed key-value store and a distributed consortium system.


title: Neural Network-Guided Synthesis of Recursive List Functions

authors:
Naoki Kobayashi
Minchao Wu

abstract: Abstract Kobayashi et al. have recently proposed NeuGuS , a framework of neural-network-guided synthesis of logical formulas or simple program fragments, where a neural network is first trained based on data, and then a logical formula over integers is constructed by using the weights and biases of the trained network as hints. The previous method was, however, restricted the class of formulas of quantifier-free linear integer arithmetic. In this paper, we propose a NeuGuS method for the synthesis of recursive predicates over lists definable by using the left fold function. To this end, we design and train a special-purpose recurrent neural network (RNN), and use the weights of the trained RNN to synthesize a recursive predicate. We have implemented the proposed method and conducted preliminary experiments to confirm the effectiveness of the method.


title: ALASCA: Reasoning in Quantified Linear Arithmetic

authors:
Konstantin Korovin
Laura Kovács
Giles Reger
Johannes Schoisswohl
Andrei Voronkov

abstract: Abstract Automated reasoning is routinely used in the rigorous construction and analysis of complex systems. Among different theories, arithmetic stands out as one of the most frequently used and at the same time one of the most challenging in the presence of quantifiers and uninterpreted function symbols. First-order theorem provers perform very well on quantified problems due to the efficient superposition calculus, but support for arithmetic reasoning is limited to heuristic axioms. In this paper, we introduce the $$\textsc {Alasca}$$ A L A S C A calculus that lifts superposition reasoning to the linear arithmetic domain. We show that $$\textsc {Alasca}$$ A L A S C A is both sound and complete with respect to an axiomatisation of linear arithmetic. We implemented and evaluated $$\textsc {Alasca}$$ A L A S C A using the Vampire theorem prover, solving many more challenging problems compared to state-of-the-art reasoners.


title: Transforming Quantified Boolean Formulas Using Biclique Covers

authors:
Oliver Kullmann
Ankit Shukla

abstract: Abstract We introduce the global conflict graph of DQCNFs (dependency quantified conjunctive normal forms), recording clashes between clauses on such universal variables on which all existential variables depend (called “global variables”). The biclique covers of this graph correspond to the eligible clause-slices of the DQCNF which consider only the global variables. We show that all such slices yield satisfiability-equivalent variations. This opens the possibility to realise this slice using as few global variables as possible. We give basic theoretical results and first supporting experimental data.


title: A Truly Symbolic Linear-Time Algorithm for SCC Decomposition

authors:
Casper Abild Larsen
Simon Meldahl Schmidt
Jesper Steensgaard
Anna Blume Jakobsen
Jaco van de Pol
Andreas Pavlogiannis

abstract: Abstract Decomposing a directed graph to its strongly connected components (SCCs) is a fundamental task in model checking. To deal with the state-space explosion problem, graphs are often represented symbolically using binary decision diagrams (BDDs), which have exponential compression capabilities. The theoretically-best symbolic algorithm for SCC decomposition is Gentilini et al’s $$\textsc {Skeleton}$$ algorithm, that uses O(n) symbolic steps on a graph of n nodes. However, $$\textsc {Skeleton}$$ uses $$\Theta (n)$$ symbolic objects, as opposed to (poly-)logarithmically many, which is the norm for symbolic algorithms, thereby relinquishing its symbolic nature. Here we present $$\textsc {Chain}$$ , a new symbolic algorithm for SCC decomposition that also makes O(n) symbolic steps, but further uses logarithmic space, and is thus truly symbolic. We then extend $$\textsc {Chain}$$ to $$\textsc {ColoredChain}$$ , an algorithm for SCC decomposition on edge-colored graphs, which arise naturally in model-checking a family of systems. Finally, we perform an experimental evaluation of $$\textsc {Chain}$$ among other standard symbolic SCC algorithms in the literature. The results show that $$\textsc {Chain}$$ is competitive on almost all benchmarks, and often faster, while it clearly outperforms all other algorithms on challenging inputs.


title: Model Checking Linear Dynamical Systems under Floating-point Rounding

authors:
Engel Lefaucheux
Joël Ouaknine
David Purser
Mohammadamin Sharifi

abstract: Abstract We consider linear dynamical systems under floating-point rounding. In these systems, a matrix is repeatedly applied to a vector, but the numbers are rounded into floating-point representation after each step (i.e., stored as a fixed-precision mantissa and an exponent). The approach more faithfully models realistic implementations of linear loops, compared to the exact arbitrary-precision setting often employed in the study of linear dynamical systems. Our results are twofold: We show that for non-negative matrices there is a special structure to the sequence of vectors generated by the system: the mantissas are periodic and the exponents grow linearly. We leverage this to show decidability of $$\omega $$ ω -regular temporal model checking against semialgebraic predicates. This contrasts with the unrounded setting, where even the non-negative case encompasses the long-standing open Skolem and Positivity problems. On the other hand, when negative numbers are allowed in the matrix, we show that the reachability problem is undecidable by encoding a two-counter machine. Again, this is in contrast with the unrounded setting where point-to-point reachability is known to be decidable in polynomial time.


title: CoPTIC: Constraint Programming Translated Into C

abstract: Abstract Constraint programming systems allow a diverse range of problems to be modelled and solved. Most systems require the user to learn a new constraint programming language, which presents a barrier to novice and casual users. To address this problem, we present the CoPTIC constraint programming system, which allows the user to write a model in the well-known programming language C, augmented with a simple API to support using a guess-and-check paradigm. The resulting model is at most as complex as an ordinary C program that uses naive brute force to solve the same problem. CoPTIC uses the bounded model checker CBMC to translate the model into a SAT instance, which is solved using the SAT solver CaDiCaL. We show that, while this is less efficient than a direct translation from a dedicated constraint language into SAT, performance remains adequate for casual users. CoPTIC supports constraint satisfaction and optimisation problems, as well as enumeration of multiple solutions. After a solution has been found, CoPTIC allows the model to be run with the solution; this makes it easy to debug a model, or to print the solution in any desired format.


title: Explainable Online Monitoring of Metric Temporal Logic

authors:
Leonardo Lima
Andrei Herasimau
Martin Raszyk
Dmitriy Traytel
Simon Yuan

abstract: Abstract Runtime monitors analyze system execution traces for policy compliance. Monitors for propositional specification languages, such as metric temporal logic (MTL), produce Boolean verdicts denoting whether the policy is satisfied or violated at a given point in the trace. Given a sufficiently complex policy, it can be difficult for the monitor’s user to understand how the monitor arrived at its verdict. We develop an MTL monitor that outputs verdicts capturing why the policy was satisfied or violated. Our verdicts are proof trees in a sound and complete proof system that we design. We demonstrate that such verdicts can serve as explanations for end users by augmenting our monitor with a graphical interface for the interactive exploration of proof trees. As a second application, our verdicts serve as certificates in a formally verified checker we develop using the Isabelle proof assistant.


title: 2LS: Arrays and Loop Unwinding - (Competition Contribution)

authors:
Viktor Malík
Frantisek Necas
Peter Schrammel
Tomás Vojnar

abstract: Abstract 2LS is a C program analyser built upon the CPROVER infrastructure that can verify and refute program assertions, memory safety, and termination. Until now, one of the main drawbacks of 2LS was its inability to verify most programs with arrays. This paper introduces a new abstract domain in 2LS for reasoning about the contents of arrays. In addition, we introduce an improved approach to loop unwinding, a crucial component of the 2LS’ verification algorithm, which particularly enables finding proofs and counterexamples for programs working with dynamic memory.


title: Reconciling Preemption Bounding with DPOR

authors:
Iason Marmanis
Michalis Kokologiannakis
Viktor Vafeiadis

abstract: Abstract There are two major techniques for scaling up stateless model checking: dynamic partial order reduction (DPOR), which only explores executions that differ in the ordering of racy accesses, and preemption bounding , which only explores executions containing up to k preemptions (preemptive context-switches). Combining these two techniques is challenging because DPOR-equivalent executions often contain a different number of preemptions, making it incorrect to cut explorations that exceed the preemption bound. To restore completeness, prior work has weakened the DPOR algorithm, which often results in the exploration of many redundant executions. We propose an alternative approach. Starting from an optimal DPOR algorithm, we achieve completeness by allowing some slack on the preemption-bound of the explored executions. We prove that the required slack does not exceed the number of threads of the program (minus two), and that this upper limit is tight.


title: Correct Approximation of Stationary Distributions

abstract: Abstract A classical problem for Markov chains is determining their stationary (or steady-state) distribution. This problem has an equally classical solution based on eigenvectors and linear equation systems. However, this approach does not scale to large instances, and iterative solutions are desirable. It turns out that a naive approach, as used by current model checkers, may yield completely wrong results. We present a new approach, which utilizes recent advances in partial exploration and mean payoff computation to obtain a correct, converging approximation.


title: VeriFuzz 1.4: Checking for (Non-)termination (Competition Contribution)

authors:
Ravindra Metta
Prasanth Yeduru
Hrishikesh Karmarkar
Raveendra Kumar Medicherla

abstract: Abstract In VeriFuzz 1.4, we implemented two new techniques for checking Non-termination and Termination. VeriFuzz 1.4 won the Termination category of SV-COMP 2023.


title: Make Flows Small Again: Revisiting the Flow Framework

authors:
Roland Meyer
Thomas Wies
Sebastian Wolff

abstract: Abstract We present a new flow framework for separation logic reasoning about programs that manipulate general graphs. The framework overcomes problems in earlier developments: it is based on standard fixed point theory, guarantees least flows, rules out vanishing flows, and has an easy to understand notion of footprint as needed for soundness of the frame rule. In addition, we present algorithms for automating the frame rule, which we evaluate on graph updates extracted from linearizability proofs for concurrent data structures. The evaluation demonstrates that our algorithms help to automate key aspects of these proofs that have previously relied on user guidance or heuristics.


title: Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers

authors:
Dawn Michaelson
Dominik Schreiber
Marijn J. H. Heule
Benjamin Kiesl-Reiter
Michael W. Whalen

abstract: Abstract Distributed clause-sharing SAT solvers can solve problems up to one hundred times faster than sequential SAT solvers by sharing derived information among multiple sequential solvers working on the same problem. Unlike sequential solvers, however, distributed solvers have not been able to produce proofs of unsatisfiability in a scalable manner, which has limited their use in critical applications. In this paper, we present a method to produce unsatisfiability proofs for distributed SAT solvers by combining the partial proofs produced by each sequential solver into a single, linear proof. Our approach is more scalable and general than previous explorations for parallel clause-sharing solvers, allowing use on distributed solvers without shared memory. We propose a simple sequential algorithm as well as a fully distributed algorithm for proof composition. Our empirical evaluation shows that for large-scale distributed solvers (100 nodes of 16 cores each), our distributed approach allows reliable proof composition and checking with reasonable overhead. We analyze the overhead and discuss how and where future efforts may further improve performance.


title: Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution)

authors:
Raphaël Monat
Abdelraouf Ouadjaout
Antoine Miné

abstract: Abstract Mopsa is a multilanguage static analysis platform relying on abstract interpretation. It is able to analyze C, Python, and programs mixing these two languages; we focus on the C analysis here. It provides a novel way to combine abstract domains, in order to offer extensibility and cooperation between them, which is especially beneficial when relational numerical domains are used. The analyses are currently flow-sensitive and fully context-sensitive. We focus only on proving programs to be correct, as our analyses are designed to be sound and terminating but not complete. We present our first participation to SV-Comp, where Mopsa earned a bronze medal in the SoftwareSystems category.


title: The WhyRel Prototype for Modular Relational Verification of Pointer Programs

authors:
Ramana Nagasamudram
Anindya Banerjee
David A. Naumann

abstract: Abstract Verifying relations between programs arises as a task in various verification contexts such as optimizing transformations, relating new versions of programs with older versions (regression verification), and noninterference. However, relational verification for programs acting on dynamically allocated mutable state is not well supported by existing tools, which provide a high level of automation at the cost of restricting the programs considered. Auto-active tools, on the other hand, require more user interaction but enable verification of a broader class of programs. This article presents WhyRel, a tool for the auto-active verification of relational properties of pointer programs based on relational region logic. WhyRel is evaluated through verification case studies, relying on SMT solvers orchestrated by the Why3 platform on which it builds. Case studies include establishing representation independence of ADTs, showing noninterference, and challenge problems from recent literature.


title: Symbolic Model Checking for TLA+ Made Faster

authors:
Rodrigo Otoni
Igor Konnov
Jure Kukovec
Patrick Eugster
Natasha Sharygina

abstract: Abstract The need to provide formal guarantees about the behaviour of the algorithms underpinning modern distributed systems became evident in recent years. This interest made apparent the complexities involved in applying verification techniques in a distributed setting, with significant effort being made in both academia and industry to aid in this endeavour. Many formalisms have been proposed to tackle the difficulties faced by practitioners, with one that has seen widespread use in industry being TLA $$^+$$ + , adopted, for instance, by Amazon Web Services. TLA $$^+$$ + provides engineers with a way of specifying both systems and desired properties, and is supported by a number of verification tools. Despite their extensive use, such tools suffer considerably from lack of scalability. To solve this, we propose a novel encoding of TLA $$^+$$ + into SMT constraints to improve symbolic model checking efficiency. Our insight is the need to provide the SMT solver with structural information about the TLA $$^+$$ + specification encoded, i.e., how data structures and their component elements interact, which we do by relying on the SMT theory of arrays. We implemented our approach by modifying the SMT-based model checker Apalache and evaluated it against comparable tools. Our results show that our approach outperforms existing ones on a number of benchmarks, with an order of magnitude improvement in checking time.


title: A Formal CHERI-C Semantics for Verification

authors:
Seung Hoon Park
Rekha R. Pai
Tom Melham

abstract: Abstract CHERI-C extends the C programming language by adding hardware capabilities , ensuring a certain degree of memory safety while remaining efficient. Capabilities can also be employed for higher-level security measures, such as software compartmentalization, that have to be used correctly to achieve the desired security guarantees. As the extension changes the semantics of C, new theories and tooling are required to reason about CHERI-C code and verify correctness. In this work, we present a formal memory model that provides a memory semantics for CHERI-C programs. We present a generalised theory with rich properties suitable for verification and potentially other types of analyses. Our theory is backed by an Isabelle/HOL formalisation that also generates an OCaml executable instance of the memory model. The verified and extracted code is then used to instantiate the parametric Gillian program analysis framework, with which we can perform concrete execution of CHERI-C programs. The tool can run a CHERI-C test suite, demonstrating the correctness of our tool, and catch a good class of safety violations that the CHERI hardware might miss.


title: Propositional Proof Skeletons

authors:
Joseph E. Reeves
Benjamin Kiesl-Reiter
Marijn J. H. Heule

abstract: Abstract Modern SAT solvers produce proofs of unsatisfiability to justify the correctness of their results. These proofs, which are usually represented in the well-known DRAT format, can often become huge, requiring multiple gigabytes of disk storage. We present a technique for semantic proof compression that selects a subset of important clauses from a proof and stores them as a so-called proof skeleton. This proof skeleton can later be used to efficiently reconstruct a full proof by exploiting parallelism. We implemented our approach on top of the award-winning SAT solver CaDiCaL and the proof checker DRAT-trim. In an experimental evaluation, we demonstrate that we can compress proofs into skeletons that are 100 to 5, 000 times smaller than the original proofs. For almost all problems, proof reconstruction using a skeleton improves the solving time on a single core, and is around five times faster when using 24 cores.


title: Goblint: Autotuning Thread-Modular Abstract Interpretation - (Competition Contribution)

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

abstract: Abstract The static analyzer Goblint is dedicated to the analysis of multi-threaded C programs by abstract interpretation. It provides multiple techniques for increasing analysis precision, e.g., configurable context-sensitivity and a wide range of numerical analyses. As a rule of thumb, more precise analyses decrease scalability, while not always necessary for solving the task at hand. Therefore, Goblint has been enhanced with autotuning which, based on syntactical criteria, adapts analysis configuration to the given program such that relevant precision is obtained with acceptable effort.


title: Timed Automata Verification and Synthesis via Finite Automata Learning

abstract: Abstract We present algorithms for model checking and controller synthesis of timed automata, seeing a timed automaton model as a parallel composition of a large finite-state machine and a relatively smaller timed automaton, and using compositional reasoning on this composition. We use automata learning algorithms to learn finite automata approximations of the timed automaton component, in order to reduce the problem at hand to finite-state model checking or to finite-state controller synthesis. We present an experimental evaluation of our approach.


title: Automated Verification for Real-Time Systems - via Implicit Clocks and an Extended Antimirov Algorithm

authors:
Yahui Song
Wei-Ngan Chin

abstract: Abstract The correctness of real-time systems depends both on the correct functionalities and the realtime constraints. To go beyond the existing Timed Automata based techniques, we propose a novel solution that integrates a modular Hoare-style forward verifier with a term rewriting system (TRS) on Timed Effects ( TimEffs ). The main purposes are to: increase the expressiveness, dynamically manipulate clocks, and efficiently solve clock constraints. We formally define a core language $$ C^{t} $$ C t , generalizing the real-time systems, modeled using mutable variables and timed behavioral patterns, such as delay , timeout , interrupt , deadline . Secondly, to capture real-time specifications, we introduce TimEffs , a new effects logic, that extends regular expressions with dependent values and arithmetic constraints. Thirdly, the forward verifier reasons temporal behaviors – expressed in TimEffs – of target $$ C^{t} $$ C t programs. Lastly, we present a purely algebraic TRS, i.e., an extended Antimirov algorithm , to efficiently check language inclusions between TimEffs . To demonstrate the feasibility of our proposal, we prototype the verification system; prove its soundness; report on case studies and experimental results.


title: PIChecker: A POR and Interpolation based Verifier for Concurrent Programs (Competition Contribution)

authors:
Jie Su
Zuchao Yang
Hengrui Xing
Jiyu Yang
Cong Tian
Zhenhua Duan

abstract: Abstract is a tool for verifying reachability properties of concurrent C programs. It moderates the trace-space explosion problem, aggravated by thread alternation, through utilizing the PC-DPOR and C-Intp techniques. The PC-DPOR technique constructs a constrained dependency graph to refine dependencies between transitions. With this basis, the inherent imprecision of the dependence over-approximation can be overcome. Thereby, many redundant equivalent traces are prevented from being explored. On the other hand, the C-Intp technique performs conditional interpolation to confine the reachable regions of states, so that infeasible conditional branches which occur more frequently in concurrent verification tasks could be pruned automatically. We have implemented the above techniques on top of the open-source program analysis framework .


title: The Packing Chromatic Number of the Infinite Square Grid is 15

authors:
Bernardo Subercaseaux
Marijn J. H. Heule

abstract: Abstract A packing k -coloring is a natural variation on the standard notion of graph k -coloring, where vertices are assigned numbers from $$\{1, \ldots , k\}$$ { 1 , … , k } , and any two vertices assigned a common color $$c \in \{1, \ldots , k\}$$ c ∈ { 1 , … , k } need to be at a distance greater than c (as opposed to 1, in standard graph colorings). Despite a sequence of incremental work, determining the packing chromatic number of the infinite square grid has remained an open problem since its introduction in 2002. We culminate the search by proving this number to be 15. We achieve this result by improving the best-known method for this problem by roughly two orders of magnitude. The most important technique to boost performance is a novel, surprisingly effective propositional encoding for packing colorings. Additionally, we developed an alternative symmetry breaking method. Since both new techniques are more complex than existing techniques for this problem, a verified approach is required to trust them. We include both techniques in a proof of unsatisfiability, reducing the trusted core to the correctness of the direct encoding.


title: PyLTA: A Verification Tool for Parameterized Distributed Algorithms

authors:
Bastien Thomas
Ocan Sankur

abstract: Abstract We present the tool PyLTA, which can model check parameterized distributed algorithms against LTL specifications. The parameters typically include the number of processes and a bound on faulty processes, and the considered algorithms are round-based and either synchronous or asynchronous.


title: Robust Almost-Sure Reachability in Multi-Environment MDPs

authors:
Marck van der Vegt
Nils Jansen
Sebastian Junges

abstract: Abstract Multiple-environment MDPs (MEMDPs) capture finite sets of MDPs that share the states but differ in the transition dynamics. These models form a proper subclass of partially observable MDPs (POMDPs). We consider the synthesis of policies that robustly satisfy an almost-sure reachability property in MEMDPs, that is, one policy that satisfies a property for all environments. For POMDPs, deciding the existence of robust policies is an EXPTIME-complete problem. We show that this problem is PSPACE-complete for MEMDPs, while the policies require exponential memory in general. We exploit the theoretical results to develop and implement an algorithm that shows promising results in synthesizing robust policies for various benchmarks.


title: Extending a High-Performance Prover to Higher-Order Logic

authors:
Petar Vukmirovic
Jasmin Blanchette
Stephan Schulz

abstract: Abstract Most users of proof assistants want more proof automation. Some proof assistants discharge goals by translating them to first-order logic and invoking an efficient prover on them, but much is lost in translation. Instead, we propose to extend first-order provers with native support for higher-order features. Building on our extension of E to $$\lambda $$ -free higher-order logic, we extend E to full higher-order logic. The result is the strongest prover on benchmarks exported from a proof assistant.


title: Verification-guided Programmatic Controller Synthesis

authors:
Yuning Wang
He Zhu

abstract: Abstract We present a verification-based learning framework VEL that synthesizes safe programmatic controllers for environments with continuous state and action spaces. The key idea is the integration of program reasoning techniques into controller training loops. VEL performs abstraction-based program verification to reason about a programmatic controller and its environment as a closed-loop system. Based on a novel verification-guided synthesis loop for training, VEL minimizes the amount of safety violation in the proof space of the system, which approximates the worst-case safety loss, using gradient-descent style optimization. Experimental results demonstrate the substantial benefits of leveraging verification feedback for synthesizing provably correct controllers.


title: A GPU Tree Database for Many-Core Explicit State Space Exploration

authors:
Anton Wijs
Muhammad Osama

abstract: Abstract Various techniques have been proposed to accelerate explicit-state model checking with GPUs, but none address the compact storage of states, or if they do, at the cost of losing completeness of the checking procedure. We investigate how to implement a tree database to store states as binary trees in GPU memory. We present fine-grained parallel algorithms to find and store trees, experiment with a number of GPU-specific configurations, and propose a novel hashing technique, called Cleary-Cuckoo hashing, which enables the use of Cleary compression on GPUs. We are the first to assess the effectiveness of using a tree database, and Cleary compression, on GPUs. Experiments show processing speeds of up to 131 million states per second.


title: Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration

authors:
Tobias Winkler
Joost-Pieter Katoen

abstract: Abstract Probabilistic pushdown automata (pPDA) are a standard model for discrete probabilistic programs with procedures and recursion. In pPDA, many quantitative properties are characterized as least fixpoints of polynomial equation systems. In this paper, we study the problem ofcertifyingthat these quantities lie within certain bounds. To this end, we first characterize the polynomial systems that admit easy-to-check certificates for validating bounds on their least fixpoint. Second, we present a sound and complete Optimistic Value Iteration algorithm for computing such certificates. Third, we show how certificates for polynomial systems can be transferred to certificates for various quantitative pPDA properties. Experiments demonstrate that our algorithm computes succinct certificates for several intricate example programs as well as stochastic context-free grammars with $$> 10^4$$ production rules.


title: FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format

authors:
Shengping Xiao
Chengyu Zhang
Jianwen Li
Geguang Pu

abstract: Abstract We present , a fuzzer to generate random word-level model checking problems in Btor2 format. Btor2 is one of the mainstream input formats for word-level hardware model checking and was used in the most recent hardware model checking competition. Compared to bit-level one, word-level model checking is a more complex research field at an earlier stage of development. Therefore, it is necessary to develop a tool that can produce a large number of test cases in Btor2 format to test either existing or under-developed word-level model checkers. To evaluate the practicality of , we tested the state-of-the-art word-level model checkers and with the generated benchmarks. Experimental results show that both tools are buggy and not mature enough, which reflects the practical value of .


title: Verification under TSO with an infinite Data Domain

authors:
Parosh Aziz Abdulla
Mohamed Faouzi Atig
Florian Furbach
Shashwat Garg

abstract: Abstract We examine verification of concurrent programs under the total store ordering (TSO) semantics used by thex86architecture. In our model, threads manipulate variables over infinite domains and they can check whether variables are related for a range of relations. We show that, in general, the control state reachability problem is undecidable. This result is derived through a reduction from the state reachability problem of lossy channel systems with data (which is known to be undecidable). In the light of this undecidability, we turn our attention to a more tractable variant of the reachability problem. Specifically, we study context bounded runs, which provide an under-approximation of the program behavior by limiting the possible interactions between processes. A run consists of a number of contexts, with each context representing a sequence of steps where a only single designated thread is active. We prove that the control state reachability problem under bounded context switching is PSPACE complete.


title: Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers

authors:
Zsófia Ádám
Dirk Beyer
Po-Chun Chien
Nian-Ze Lee
Nils Sirrenberg

abstract: Abstract Formal verification is essential but challenging: Even the best verifiers may produce wrong verification verdicts.Certifyingverifiers enhance the confidence in verification results by generating awitnessfor other tools to validate the verdict independently. Recently, translating the hardware-modeling languageBtor2to software, such as the programming language C or LLVM intermediate representation, has been actively studied and facilitated verifying hardware designs by software analyzers. However, it remained unknown whether witnesses produced by software verifiers contain helpful information about the original circuits and how such information can aid hardware analysis. We propose a certifying and validating frameworkBtor2-Certto verify safety properties ofBtor2circuits, combiningBtor2-to-C translation, software verifiers, and a new witness validatorBtor2-Val, to answer the above open questions.Btor2-Certtranslates a softwareviolation witnessto aBtor2violation witness; As theBtor2language lacks a format forcorrectness witnesses, we encode invariants in software correctness witnesses asBtor2circuits. The validatorBtor2-Valchecks violation witnesses by circuit simulation and correctness witnesses byvalidation via verification. In our evaluation,Btor2-Certsuccessfully utilized software witnesses to improve quality assurance of hardware. By invoking the software verifierCbmcon translated programs, it uniquely solved, with confirmed witnesses, 8 % of the unsafe tasks for which the hardware verifierABCfailed to detect bugs.


title: On Dependent Variables in Reactive Synthesis

authors:
S. Akshay
Eliyahu Basa
Supratik Chakraborty
Dror Fried

abstract: Abstract Given a Linear Temporal Logic (LTL) formula over input and output variables, reactive synthesis requires us to design a deterministic Mealy machine that gives the values of outputs at every time step for every sequence of inputs, such that the LTL formula is satisfied. In this paper, we investigate the notion of dependent variables in the context of reactive synthesis. Inspired by successful pre-processing techniques in Boolean functional synthesis, we define dependent variables in reactive synthesis as output variables that are uniquely assigned, given an assignment to all other variables and the history so far. We describe an automata-based approach for finding a set of dependent variables. Using this, we show that dependent variables are surprisingly common in reactive synthesis benchmarks. Next, we develop a novel synthesis framework that exploits dependent variables to construct an overall synthesis solution. By implementing this framework using the widely used library , we show that reactive synthesis that exploits dependent variables can solve some problems beyond the reach of existing techniques. Furthermore, we observe that among benchmarks with dependent variables, if the count of non-dependent variables is low ( $$\le 3$$ ≤3 in our experiments), our method outperforms state-of-the-art tools for synthesis.


title: JPF: From 2003 to 2023

authors:
Cyrille Artho
Pavel Parízek
Daohan Qu
Varadraj Galgali
Pu (Luke) Yi

abstract: Abstract We give an account of JPF’s current architecture as it has evolved over the last 20 years. Key changes include a modular, extensible design, and Java 11 support. Java 11 brought with it fundamental changes in the language and its runtime, in particular, a new modular library system, different compilation of string expressions to bootstrap methods, and changes in many internal interfaces that allow access to the loaded code and the virtual machine state. These changes required numerous adaptations in JPF to ensure a successful compilation and correct behavior under Java 11.


title: Auction-Based Scheduling

authors:
Guy Avni
Kaushik Mallik
Suman Sadhukhan

abstract: Abstract Sequential decision-making tasks often require satisfaction of multiple, partially-contradictory objectives. Existing approaches are monolithic, where a singlepolicyfulfills all objectives. We presentauction-based scheduling, adecentralizedframework for multi-objective sequential decision making. Each objective is fulfilled using a separate and independent policy. Composition of policies is performed at runtime, where at each step, the policies simultaneously bid from pre-allocated budgets for the privilege of choosing the next action. The framework allows policies to be independently created, modified, and replaced. We study path planning problems on finite graphs with two temporal objectives and present algorithms to synthesize policies together with bidding policies in a decentralized manner. We consider three categories of decentralized synthesis problems, parameterized by the assumptions that the policies make on each other. We identify a class of assumptions calledassume-admissiblefor which synthesis is always possible for graphs whose every vertex has at most two outgoing edges.


title: Witch 3: Validation of Violation Witnesses in the Witness Format 2.0 - (Competition Contribution)

authors:
Paulína Ayaziová
Jan Strejcek

abstract: Abstract Witch 3 is a new validator of violation witnesses in the witness format 2.0. Note that our previous tool,Symbiotic-Witch 2, can validate only violation witnesses in the old GraphML format.Witch 3 validates witnesses of reachability of an error function, overflows, and invalid dereferences and deallocations. Similarly toSymbiotic-Witch 2, the tool is based on symbolic execution and uses parts of theSymbioticframework. Support of the witness format 2.0 inWitch 3 includes features not supported bySymbiotic-Witch 2, such as constraints on the program variables and function return values, specifying statements by column, and providing the concrete statement in which the violation occurs. These additional features can further restrict the explored state space, and, more importantly, allow for much more precise validation.


title: CTMCs with Imprecisely Timed Observations

authors:
Thom Badings
Matthias Volk
Sebastian Junges
Mariëlle Stoelinga
Nils Jansen

abstract: Abstract Labeled continuous-time Markov chains (CTMCs) describe processes subject to random timing and partial observability. In applications such as runtime monitoring, we must incorporate past observations. The timing of these observations matters but may be uncertain. Thus, we consider a setting in which we are given a sequence of imprecisely timed labels called the evidence. The problem is to compute reachability probabilities, which we condition on this evidence. Our key contribution is a method that solves this problem by unfolding the CTMC states over all possible timings for the evidence. We formalize this unfolding as a Markov decision process (MDP) in which each timing for the evidence is reflected by a scheduler. This MDP has infinitely many states and actions in general, making a direct analysis infeasible. Thus, we abstract the continuous MDP into a finite interval MDP (iMDP) and develop an iterative refinement scheme to upper-bound conditional probabilities in the CTMC. We show the feasibility of our method on several numerical benchmarks and discuss key challenges to further enhance the performance.


title: CPAchecker 2.3 with Strategy Selection - (Competition Contribution)

authors:
Daniel Baier
Dirk Beyer
Po-Chun Chien
Marek Jankola
Matthias Kettl
Nian-Ze Lee
Thomas Lemberger
Marian Lingsch Rosenfeld
Martin Spiessl
Henrik Wachowitz
Philipp Wendler

abstract: Abstract CPAcheckeris a versatile framework for software verification, rooted in the established concept ofconfigurable program analysis. Compared to the last published system description at SV-COMP 2015, theCPAcheckersubmission to SV-COMP 2024 incorporates new analyses for reachability safety, memory safety, termination, overflows, and data races. To combine forces of the available analyses inCPAcheckerand cover the full spectrum of the diverse program characteristics and specifications in the competition, we usestrategy selectionto predict a sequential portfolio of analyses that is suitable for a given verification task. The prediction is guided by a set of carefully picked program features. The sequential portfolios are composed based on expert knowledge and consist of bit-precise analyses usingk-induction, data-flow analysis, SMT solving, Craig interpolation, lazy abstraction, and block-abstraction memoization. The synergy of various algorithms inCPAcheckerenables support for all properties and categories of C programs in SV-COMP 2024 and contributes to its success in many categories.CPAcheckeralso generates verification witnesses in the new YAML format.


title: ConcurrentWitness2Test: Test-Harnessing the Power of Concurrency (Competition Contribution)

authors:
Levente Bajczi
Zsófia Ádám
Zoltán Micskei

abstract: Abstract ConcurrentWitness2Testis a violation witness validator for concurrent software. Taking both nondeterminism of data and interleaving-based nondeterminism into account, the tool aims to use the metadata described in the violation witnesses to synthesize an executable test harness. While plagued by some initial challenges yet to overcome, the validation performance ofConcurrentWitness2Testcorroborates the usefulness of the proposed approach.


title: EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution)

authors:
Levente Bajczi
Dániel Szekeres
Milán Mondok
Zsófia Ádám
Márk Somorjai
Csanád Telbisz
Mihály Dobos-Kovács
Vince Molnár

abstract: Abstract Thetais a model checking framework conventionally based on abstraction refinement techniques. While abstraction is useful for a large number of verification problems, the over-reliance on the technique led toThetabeing unable to meaningfully adapt. Identifying this problem in previous years of SV-COMP has led us to createEmergenTheta, a sandbox for the new approaches we wantThetato support. By differentiating between mature and emerging techniques, we can experiment more freely without hurting the reliability of the overall framework. In this paper we detail the development route toEmergenTheta, and its first debut on SV-COMP’24 in the ReachSafety category.


title: Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution)

authors:
Levente Bajczi
Csanád Telbisz
Márk Somorjai
Zsófia Ádám
Mihály Dobos-Kovács
Dániel Szekeres
Milán Mondok
Vince Molnár

abstract: Abstract Thetais a model checking framework, with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. In SV-COMP 2024, we use 1) an abstraction-aware partial order reduction; 2) a dynamic statement reduction technique; and 3) enhanced support for call stacks to handle recursive programs. We integrate these techniques in an improved architecture with inherent support for portfolio-based verification using dynamic algorithm selection, with a diverse selection of supported SMT solvers as well. In this paper we detail the advances ofThetaregarding concurrent and recursive software support.


title: Formally Verifying an Efficient Sorter

authors:
Bernhard Beckert
Peter Sanders
Mattias Ulbrich
Julian Wiesler
Sascha Witt

abstract: Abstract In this experience report, we present the complete formal verification of a Java implementation of inplace superscalar sample sort ( "Image missing") using the KeY program verification system. As "Image missing" is one of the fastest general purpose sorting algorithms, this is an important step towards a collection of basic toolbox components that are both provably correct and highly efficient. At the same time, it is an important case study of how careful, highly efficient implementations of complicated algorithms can be formally verified directly. We provide an analysis of which features of the KeY system and its verification calculus are instrumental in enabling algorithm verification without any compromise on algorithm efficiency.


title: Automated Software Verification of Hyperliveness

abstract: Abstract Hyperproperties relate multiple executions of a program and are commonly used to specify security and information-flow policies. Most existing work has focused on the verification ofk-safety properties, i.e., properties that state that allk-tuples of execution traces satisfy a given property. In this paper, we study the automated verification of richer properties that combine universal and existential quantification over executions. Concretely, we consider $$\forall ^k\exists ^l$$ ∀k∃l properties, which state that for allkexecutions, there existlexecutions that, together, satisfy a property. This captures important non-k-safety requirements, including hyperliveness properties such as generalized non-interference, opacity, refinement, and robustness. We design an automated constraint-based algorithm for the verification of $$\forall ^k\exists ^l$$ ∀k∃l properties. Our algorithm leverages a sound-and-complete program logic and a (parameterized) strongest postcondition computation. We implement our algorithm in a tool called and report on encouraging experimental results.


title: State of the Art in Software Verification and Witness Validation: SV-COMP 2024

abstract: Abstract The 13th edition of the Competition on Software Verification (SV-COMP 2024) was the largest competition of its kind so far: A total of 76 tools for verification and witness validation were compared. The competition evaluated 59 verification systems and 17 validation systems from 34 teams from 12 countries. This yields a good overview of the state of the art in tools for software verification. The competition was executed on a benchmark set with 30 300 verification tasks for C programs and 587 . verification tasks for Java programs. The specifications again included reachability, memory safety, overflows, and termination. This year was the second time that the competition had an extra competition track on witness validation. We introduced a new witness format 2.0, and a new scoring schema for the validation track. All meta data about the verification and validation tools are available in the FM-Tools repository.


title: Asynchronous Subtyping by Trace Relaxation

authors:
Laura Bocchi
Andy King
Maurizio Murgia

abstract: Abstract Session subtyping answers the question of whether a program in a communicating system can be safely substituted for another, when their communication behaviours are described by session types. Asynchronous session subtyping is undecidable, hence the interest in devising sound, although incomplete, subtyping algorithms. State-of-the-art algorithms are formulated in terms of a data-structure called input trees. We show how input trees can be replaced by sets of traces, which opens up opportunities for applying techniques abstract interpretation techniques to the problem of asynchronous session subtyping. Sets of traces can be relaxed (enlarged) whilst still allowing subtyping to be observed, and one can choose relaxations that can be finitely represented, even when the input trees are arbitrarily large. We instantiate this strategy using regular expressions and show that it allows subtyping to be mechanically proven for communication patterns that were previously out of reach.


title: Learning Explainable and Better Performing Representations of POMDP Strategies

authors:
Alexander Bork
Debraj Chakraborty
Kush Grover
Jan Kretínský
Stefanie Mohr

abstract: Abstract Strategies for partially observable Markov decision processes (POMDP) typically require memory. One way to represent this memory is via automata. We present a method to learn an automaton representation of a strategy using a modification of the $$L^*$$ L ∗ -algorithm. Compared to the tabular representation of a strategy, the resulting automaton is dramatically smaller and thus also more explainable. Moreover, in the learning process, our heuristics may even improve the strategy’s performance. We compare our approach to an existing approach that synthesizes an automaton directly from the POMDP, thereby solving it. Our experiments show that our approach can lead to significant improvements in the size and quality of the resulting strategy representations.


title: Dissipative quadratizations of polynomial ODE systems

authors:
Yubo Cai
Gleb Pogudin

abstract: Abstract Quadratization refers to a transformation of an arbitrary system of polynomial ordinary differential equations to a system with at most quadratic right-hand side. Such a transformation unveils new variables and model structures that facilitate model analysis, simulation, and control and offer a convenient parameterization for data-driven approaches. Quadratization techniques have found applications in diverse fields, including systems theory, fluid mechanics, chemical reaction modeling, and mathematical analysis. In this study, we focus on quadratizations that preserve the stability properties of the original model, specifically dissipativity at given equilibria. This preservation is desirable in many applications of quadratization including reachability analysis and synthetic biology. We establish the existence of dissipativity-preserving quadratizations, develop an algorithm for their computation, and demonstrate it in several case studies.


title: Bubaak-SpLit: Split what you cannot verify (Competition contribution)

authors:
Marek Chalupa
Cedric Richter

abstract: Abstract Bubaak-SpLit is a tool for dynamically splitting verification tasks into parts that can then be analyzed in parallel. It is built on top ofBubaak, a tool designed for running combinations of verifiers in parallel. In contrast toBubaak, that directly invokes verifiers on the inputs,Bubaak-SpLit first starts by splitting the input program into multiple modified versions calledprogram splits. During the splitting process,Bubaak-SpLit utilizes aweakverifier (in our case symbolic execution with a short timelimit) to analyze each generated program split. If the weak verifier fails on a program split, we split this program split again and start the verification process again on the generated program splits. We run the splitting process until a predefined number ofhard-to-verifyprogram splits is generated or a splitting limit is reached. During the main verification phase, we run a combination ofBubaak-LeeandSlowbeastin parallel on the remaining unsolved parts of the verification task.


title: Z3-Noodler: An Automata-based String Solver

authors:
Yu-Fang Chen
David Chocholatý
Vojtech Havlena
Lukás Holík
Ondrej Lengál
Juraj Síc

abstract: Abstract Z3-Noodleris a fork ofZ3that replaces its string theory solver with a custom solver implementing the recently introduced stabilization-based algorithm for solving word equations with regular constraints. An extensive experimental evaluation shows thatZ3-Noodleris a fully-fledged solver that can compete with state-of-the-art solvers, surpassing them by far on many benchmarks. Moreover, it is often complementary to other solvers, making it a suitable choice as a candidate to a solver portfolio.


title: CPV: A Circuit-Based Program Verifier

authors:
Po-Chun Chien
Nian-Ze Lee

abstract: Abstract We submit to SV-COMP 2024CPV, a circuit-based software verifier for C programs.CPVutilizes sequential circuits as its intermediate representation and invokes hardware model checkers to analyze the reachability safety of C programs. As the frontend, it uses Kratos2 , a recently proposed verification tool, to translate a C program to a sequential circuit. As the backend, state-of-the-art hardware model checkers ABC and AVR are employed to verify the translated circuits. We configure the hardware model checkers to run various analyses, including IC3/PDR, interpolation-based model checking, and $$k$$ k -induction. Information discovered by hardware model checkers is represented as verification witnesses. In the competition,CPVachieved comparable performance against participants whose intermediate representations are based on control-flow graphs. In the categoryReachSafety, it outperformed several mature software verifiers as a first-year participant.CPVmanifests the feasibility of sequential circuits as an alternative intermediate representation for program analysis and enables head-to-head algorithmic comparison between hardware and software verification.


title: Mata: A Fast and Simple Finite Automata Library

authors:
David Chocholatý
Tomás Fiedor
Vojtech Havlena
Lukás Holík
Martin Hruska
Ondrej Lengál
Juraj Síc

abstract: Abstract Mata is a well-engineered automata library written in C++ that offers a unique combination of speed and simplicity. It is meant to serve in applications such as string constraint solving and reasoning about regular expressions, and as a reference implementation of automata algorithms. Besides basic algorithms for (non)deterministic automata, it implements a fast simulation reduction and antichain-based language inclusion checking. The simplicity allows a straightforward access to the low-level structures, making it relatively easy to extend and modify. Besides the C++ API, the library also implements a Python binding. The library comes with a large benchmark of automata problems collected from relevant applications such as string constraint solving, regular model checking, and reasoning about regular expressions. We show that Mata is on this benchmark significantly faster than all libraries from a wide range of automata libraries we collected. Its usefulness in string constraint solving is demonstrated by the string solver Z3-Noodler, which is based on Mata and outperforms the state of the art in string constraint solving on many standard benchmarks.


title: TaSSAT: Transfer and Share SAT

authors:
Md. Solimul Chowdhury
Cayden R. Codel
Marijn J. H. Heule

abstract: Abstract We present , a powerful local search SAT solver that effectively solves hard combinatorial problems. Its unique approach of transferring clause weights in local minima enhances its efficiency in solving problem instances. Since it is implemented on top of , benefits from practical techniques such as restart strategies and thread parallelization. Our implementation includes a parallel version that shares data structures across threads, leading to a significant reduction in memory usage. Our experiments demonstrate that outperforms similar solvers on a vast set of SAT competition benchmarks. Notably, with the parallel configuration of , we improve lower bounds for several van der Waerden numbers.


title: Automate where Automation Fails: Proof Strategies for Frama-C/WP

authors:
Loïc Correnson
Allan Blanchard
Adel Djoudi
Nikolai Kosmatov

abstract: Abstract Modern deductive verification tools succeed in automatically proving the great majority of program annotations thanks in particular to constantly evolving SMT solvers they rely on. The remaining proof goals still require interactively created proof scripts. This tool demo paper presents a new solution for an automatic creation of proof scripts in /, a popular deductive verifier for C programs. The verification engineer defines a proof strategy describing several initial proof steps, from which proof scripts are automatically generated and applied. Our experiments on a large real-life industrial project confirm that the new proof strategy engine strongly facilitates the verification process by automating the creation of proof scripts, thus increasing the potential of industrial applications of deductive verification on large code bases.


title: NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis

authors:
Matthias Cosler
Christopher Hahn
Ayham Omar
Frederik Schmitt

abstract: Abstract We introduce , a neuro-symbolic portfolio solver framework for reactive synthesis. At the core of the solver lies a seamless integration of neural and symbolic approaches to solving the reactive synthesis problem. To ensure soundness, the neural engine is coupled with model checkers verifying the predictions of the underlying neural models. The open-source implementation of provides an integration framework for reactive synthesis in which new neural and state-of-the-art symbolic approaches can be seamlessly integrated. Extensive experiments demonstrate its efficacy in handling challenging specifications, enhancing the state-of-the-art reactive synthesis solvers, with contributing novel solves in the current SYNTCOMP benchmarks.


title: Deciding Boolean Separation Logic via Small Models

authors:
Tomás Dacík
Adam Rogalewicz
Tomás Vojnar
Florian Zuleger

abstract: Abstract We present a novel decision procedure for a fragment of separation logic (SL) with arbitrary nesting of separating conjunctions with boolean conjunctions, disjunctions, and guarded negations together with a support for the most common variants of linked lists. Our method is based on a model-based translation to SMT for which we introduce several optimisations—the most important of them is based on bounding the size of predicate instantiations within models of larger formulae, which leads to a much more efficient translation of SL formulae to SMT. Through a series of experiments, we show that, on the frequently used symbolic heap fragment, our decision procedure is competitive with other existing approaches, and it can outperform them outside the symbolic heap fragment. Moreover, our decision procedure can also handle some formulae for which no decision procedure has been implemented so far.


title: On-The-Fly Algorithm for Reachability in Parametric Timed Games

authors:
Mikael Bisgaard Dahlsen-Jensen
Baptiste Fievet
Laure Petrucci
Jaco van de Pol

abstract: Abstract Parametric Timed Games (PTG) are an extension of the model of Timed Automata. They allow for the verification and synthesis of real-time systems, reactive to their environment and depending on adjustable parameters. Given a PTG and a reachability objective, we synthesize the values of the parameters such that the game is winning for the controller. We adapt and implement the On-The-Fly algorithm for parameter synthesis for PTG. Several pruning heuristics are introduced, to improve termination and speed of the algorithm. We evaluate the feasibility of parameter synthesis for PTG on two large case studies. Finally, we investigate the correctness guarantee of the algorithm: though the problem is undecidable, our semi-algorithm produces all correct parameter valuations “in the limit”.


title: Scalable Tree-based Register Automata Learning

authors:
Simon Dierl
Paul Fiterau-Brostean
Falk Howar
Bengt Jonsson
Konstantinos Sagonas
Fredrik Tåquist

abstract: Abstract Existing active automata learning (AAL) algorithms have demonstrated their potential in capturing the behavior of complex systems (e.g., in analyzing network protocol implementations). The most widely used AAL algorithms generate finite state machine models, such as Mealy machines. For many analysis tasks, however, it is crucial to generate richer classes of models that also show how relations between data parameters affect system behavior. Such models have shown potential to uncover critical bugs, but their learning algorithms do not scale beyond small and well curated experiments. In this paper, we present $${SL}^{\lambda }$$ SL λ , an effective and scalable register automata (RA) learning algorithm that significantly reduces the number of tests required for inferring models. It achieves this by combining a tree-based cost-efficient data structure with mechanisms for computing short and restricted tests. We have implemented $${SL}^{\lambda }$$ SL λ as a new algorithm in RALib. We evaluate its performance by comparing it against $${SL}^{*}$$ SL ∗ , the current state-of-the-art RA learning algorithm, in a series of experiments, and show superior performance and substantial asymptotic improvements in bigger systems.


title: Knor: reactive synthesis using Oink

authors:
Tom van Dijk
Feije van Abbema
Naum Tomov

abstract: Abstract We present an innovative approach to the reactive synthesis of parity automaton specifications, which plays a pivotal role in the synthesis of linear temporal logic. We find that our method efficiently solves the SYNTCOMP synthesis competition benchmarks for parity automata from LTL specifications, solving all 288 models in under a minute. We therefore direct our attention to optimizing the circuit size and propose several methods to reduce the size of the constructed circuits: (1) leveraging different parity game solvers, (2) applying bisimulation minimisation to the winning strategy, (3) using alternative encodings from the strategy to an and-inverter graph, (4) integrating post-processing with the ABC tool. We implement these methods in the Knor tool, which has secured us multiple victories in the PGAME track of the SYNTCOMP competition.


title: Fully Generalized Reactivity(1) Synthesis

authors:
Rüdiger Ehlers
Ayrat Khalimov

abstract: Abstract Generalized Reactivity(1) (GR(1)) synthesis is a reactive synthesis approach in which the specification is split into two parts: a symbolic game graph, describing the safe transitions of a system, a liveness specification in a subset of Linear Temporal Logic (LTL) on top of it. Many specifications can naturally be written in this restricted form, and the restriction gives rise to a scalable synthesis procedure – the reasons for the high popularity of the approach. For specifications even slightly beyond GR(1), however, the approach is inapplicable. This necessitates a transition to synthesizers for full LTL specifications, introducing a huge efficiency drop. This paper proposes a synthesis approach that smoothly bridges the efficiency gap from GR(1) to LTL by unifying synthesis for both classes of specifications. The approach leverages a recently introduced canonical representation of omega-regular languages based on a chain of good-for-games co-Büchi automata (COCOA). By constructing COCOA for the liveness part of a specification, we can then build a fixpoint formula that can be efficiently evaluated on the symbolic game graph. The COCOA-based synthesis approach outperforms standard approaches and retains the efficiency of GR(1) synthesis for specifications in GR(1) form and those with few non-GR(1) specification parts.


title: DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories

authors:
Nick Feng
Alan J. Hu
Sam Bayless
Syed M. Iqbal
Patrick Trentin
Mike Whalen
Lee Pike
John Backes

abstract: Abstract Generating proofs of unsatisfiability is a valuable capability of most SAT solvers, and is an active area of research for SMT solvers. This paper introduces the first method to efficiently generate proofs of unsatisfiability specifically for an important subset of SMT: SAT Modulo Monotonic Theories (SMMT), which includes many useful finite-domain theories (e.g., bit vectors and many graph-theoretic properties) and is used in production at Amazon Web Services. Our method uses propositional definitions of the theory predicates, from which it generates compact Horn approximations of the definitions, which lead to efficient DRAT proofs, leveraging the large investment the SAT community has made in DRAT. In experiments on practical SMMT problems, our proof generation overhead is minimal (7.41% geometric mean slowdown, 28.8% worst-case), and we can generate and check proofs for many problems that were previously intractable.


title: HaliVer: Deductive Verification and Scheduling Languages Join Forces

authors:
Lars B. van den Haak
Anton Wijs
Marieke Huisman
Mark van den Brand

abstract: Abstract The HaliVer tool integrates deductive verification into the popular scheduling language Halide, used for image processing pipelines and array computations. HaliVer uses VerCors, a separation logic-based verifier, to verify the correctness of (1) the Halide algorithms and (2) the optimised parallel code produced by Halide when an optimisation schedule is applied to an algorithm. This allows proving complex, optimised code correct while reducing the effort to provide the required verification annotations. For both approaches, the same specification is used. We evaluated the tool on several optimised programs generated from characteristic Halide algorithms, using all but one of the essential scheduling directives available in Halide. Without annotation effort, HaliVer proves memory safety in almost all programs. With annotations HaliVer, additionally, proves functional correctness properties. We show that the approach is viable and reduces the manual annotation effort by an order of magnitude.


title: Happy Ending: An Empty Hexagon in Every Set of 30 Points

authors:
Marijn J. H. Heule
Manfred Scheucher

abstract: Abstract Satisfiability solving has been used to tackle a range of long-standing open math problems in recent years. We add another success by solving a geometry problem that originated a century ago. In the 1930s, Esther Klein’s exploration of unavoidable shapes in planar point sets in general position showed that every set of five points includes four points in convex position. For a long time, it was open if an empty hexagon, i.e., six points in convex position without a point inside, can be avoided. In 2006, Gerken and Nicolás independently proved that the answer is no. We establish the exact bound: Every 30-point set in the plane in general position contains an empty hexagon. Our key contributions include an effective, compact encoding and a search-space partitioning strategy enabling linear-time speedups even when using thousands of cores.


title: A State-of-the-Art Karp-Miller Algorithm Certified in Coq

authors:
Thibault Hilaire
David Ilcinkas
Jérôme Leroux

abstract: Abstract Petri nets constitute a well-studied model to verify and study concurrent systems, among others, and computing the coverability set is one of the most fundamental problems about Petri nets. Using the proof assistant Coq, we certified the correctness and termination of the MinCov algorithm by Finkel, Haddad, and Khmelnitsky (FOSSACS 2020). This algorithm is the most recent algorithm in the literature that computes the minimal basis of the coverability set, a problem known to be prone to subtle bugs. Apart from the intrinsic interest of a computer-checked proof, our certification provides new insights on the MinCov algorithm. In particular, we introduce as an intermediate algorithm a small-step variant of MinCov of independent interest.


title: OxiDD - A Safe, Concurrent, Modular, and Performant Decision Diagram Framework in Rust

authors:
Nils Husung
Clemens Dubslaff
Holger Hermanns
Maximilian A. Köhl

abstract: Abstract Decision diagrams (DDs) are an important data structure in computer science with applications ranging from circuit design and verification to machine learning. Most prominently, binary DDs are commonly used to succinctly represent Boolean functions. Due to the practical importance of DDs, there is an ongoing quest for high-performance software libraries supporting the construction and manipulation of DDs. With OxiDD, we present a new framework for DDs that focuses on safety, concurrency, and modularity. Following a highly modular design we implement OxiDD in Rust, which facilitates the integration of various kinds of DDs such as MTBDDs, ZBDDs, and TDDs, all within safe code also in a concurrent setting. Already in its initial release, OxiDD does not compromise performance, which we show to be on par with or even better than established highly optimized DD libraries.


title: Fast Symbolic Computation of Bottom SCCs

authors:
Anna Blume Jakobsen
Rasmus Skibdahl Melanchton Jørgensen
Jaco van de Pol
Andreas Pavlogiannis

abstract: Abstract The computation of bottom strongly connected components (BSCCs) is a fundamental task in model checking, as well as in characterizing the attractors of dynamical systems. As such, symbolic algorithms for BSCCs have received special attention, and are based on the idea that the computation of an SCC can be stopped early, as soon as it is deemed to be non-bottom. In this paper we introduce $$\textsc {Pendant}$$ P E N D A N T , a new symbolic algorithm for computing BSCCs which runs in linear symbolic time. In contrast to the standard approach of escaping non-bottom SCCs, $$\textsc {Pendant}$$ P E N D A N T aims to start the computation from nodes that are likely to belong to BSCCs, and thus is more effective in sidestepping SCCs that are non-bottom. Moreover, we employ a simple yet powerful deadlock-detection technique, that quickly identifies singleton BSCCs before the main algorithm is run. Our experimental evaluation on three diverse datasets of 553 models demonstrates the efficacy of our two methods: $$\textsc {Pendant}$$ P E N D A N T is decisively faster than the standard existing algorithm for BSCC computation, while deadlock detection improves the performance of each algorithm significantly.


title: Forward and Backward Constrained Bisimulations for Quantum Circuits

authors:
Antonio Jiménez-Pastor
Kim G. Larsen
Mirco Tribastone
Max Tschaikowski

abstract: Abstract Efficient methods for the simulation of quantum circuits on classic computers are crucial for their analysis due to the exponential growth of the problem size with the number of qubits. Here we study lumping methods based on bisimulation, an established class of techniques that has been proven successful for (classic) stochastic and deterministic systems such as Markov chains and ordinary differential equations. Forward constrained bisimulation yields a lower-dimensional model which exactly preserves quantum measurements projected on a linear subspace of interest. Backward constrained bisimulation gives a reduction that is valid on a subspace containing the circuit input, from which the circuit result can be fully recovered. We provide an algorithm to compute the constraint bisimulations yielding coarsest reductions in both cases, using a duality result relating the two notions. As applications, we provide theoretical bounds on the size of the reduced state space for well-known quantum algorithms for search, optimization, and factorization. Using a prototype implementation, we report significant reductions on a set of benchmarks. Furthermore, we show that constraint bisimulation complements state-of-the-art methods for the simulation of quantum circuits based on decision diagrams.


title: Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution - (Competition Contribution)

authors:
Martin Jonás
Kristián Kumor
Jakub Novák
Jindrich Sedlácek
Marek Trtík
Lukás Zaoral
Paulína Ayaziová
Jan Strejcek

abstract: Abstract Symbiotic 10 brings four substantial improvements. First, we extended our clone ofKleecalledJetKleewithlazy memory initialization. With this extension,JetKleecan symbolically execute a function without knowing its context. In SV-COMP, we use it to handle variables. Second, we have implemented the technique calledcompact symbolic executiontoSlowbeast. Third, we have implemented a non-trivialmay-happen-in-parallelanalysis, which improves slicing of parallel programs. Finally, we have implemented support for violation witnesses in the newwitness format 2.0.


title: Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage

authors:
Martin Jonás
Jan Strejcek
Marek Trtík
Lukás Urban

abstract: Abstract We present a gray-box fuzzing approach based on several new ideas. While standard gray-box fuzzing aims to cover all branches of the input program, our approach primarily aims to cover both results of each Boolean expression. To achieve this goal, we track the distances to flipping these results and we dynamically detect the input bytes that influence the distance. Then we use this information to efficiently flip the results. More precisely, we apply gradient descent on the detected bytes or we create new inputs by using detected bytes from different inputs. We implemented our approach in a tool called Fizzer. An evaluation on the benchmarks of Test-Comp 2023 shows that Fizzer is fully competitive with the winning tools of the competition, which use advanced formal methods like symbolic execution or bounded model checking, usually in combination with fuzzing.


title: Speculative SAT Modulo SAT

authors:
Hari Govind V. K.
Isabel Garcia-Contreras
Sharon Shoham
Arie Gurfinkel

abstract: Abstract State-of-the-art model-checking algorithms like IC3/PDR are based on uni-directional modular SAT solving for finding and/or blocking counterexamples. Modular SAT-solvers divide a SAT-query into multiple sub-queries, each solved by a separate SAT-solver (called a module), and propagate information (lemmas, proof obligations, blocked clauses, etc.) between modules. While modular solving is key to IC3/PDR, it is obviously not as effective as monolithic solving, especially when individual sub-queries are harder to solve than the combined query. This is partially addressed in SAT modulo SAT (SMS) by propagating unit literals back and forth between the modules and using information from one module to simplify the sub-query in another module as soon as possible (i.e., before the satisfiability of any sub-query is established). However, bi-directionality of SMS is limited because of the strict order between decisions and propagation – only one module is allowed to make decisions, until its sub-query is SAT. In this paper, we propose a generalization of SMS, called specSMS, that speculates decisions between modules. This makes it bi-directional – decisions are made in multiple modules, and learned clauses are exchanged in both directions. We further extend DRUP proofs and interpolation, these are useful in model checking, to specSMS. We have implemented specSMS in Z3 and empirically validate it on a series of benchmarks that are provably hard for SMS.


title: CESAR: Control Envelope Synthesis via Angelic Refinements

authors:
Aditi Kabra
Jonathan Laurent
Stefan Mitsch
André Platzer

abstract: Abstract This paper presents an approach for synthesizing provably correct control envelopes for hybrid systems. Control envelopes characterize families of safe controllers and are used to monitor untrusted controllers at runtime. Our algorithm fills in the blanks of a hybrid system’s sketch specifying the desired shape of the control envelope, the possible control actions, and the system’s differential equations. In order to maximize the flexibility of the control envelope, the synthesized conditions saying which control action can be chosen when should be as permissive as possible while establishing a desired safety condition from the available assumptions, which are augmented if needed. An implicit, optimal solution to this synthesis problem is characterized using hybrid systems game theory, from which explicit solutions can be derived via symbolic execution and sound, systematic game refinements. Optimality can be recovered in the face of approximation via a dual game characterization. The resulting algorithm, Control Envelope Synthesis via Angelic Refinements (CESAR), is demonstrated in a range of safe control envelope synthesis examples with different control challenges.


title: SootUp: A Redesign of the Soot Static Analysis Framework

authors:
Kadiray Karakaya
Stefan Schott
Jonas Klauke
Eric Bodden
Markus Schmidt
Linghui Luo
Dongjie He

abstract: Abstract Since its inception two decades ago, Soot has become one of the most widely used open-source static analysis frameworks. Over time it has been extended with the contributions of countless researchers. Yet, at the same time, the requirements for Soot have changed over the years and become increasingly at odds with some of the major design decisions that underlie it. In this work, we thus present SootUp, a complete reimplementation of Soot that seeks to fulfill these requirements with a novel design, while at the same time keeping elements that Soot users have grown accustomed to.


title: Enhancing GenMC's Usability and Performance

authors:
Michalis Kokologiannakis
Rupak Majumdar
Viktor Vafeiadis

abstract: Abstract GenMC is a state-of-the-art stateless model checker that can verify safety properties of concurrent C/C++ programs under a wide range of memory consistency models, such as SC, TSO, RC11, and IMM. In this paper, we improve the performance and usability of GenMC: we provide a probabilistic estimate of the expected verification cost, we automate the porting of new memory models, and employ caching and other data structure optimizations to improve the tool’s performance.


title: Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development

authors:
Lukas König
Christian Heinzemann
Alberto Griggio
Michaela Klauck
Alessandro Cimatti
Franziska Henze
Stefano Tonetta
Stefan Küperkoch
Dennis Fassbender
Michael Hanselmann

abstract: Abstract Automated driving functions are among the most critical software components to develop. Before deployment in series vehicles, it has to be shown that the functions drive safely and in compliance with traffic rules. Despite the coverage that can be reached with very large amounts of test drives, corner cases remain possible. Furthermore, the development is subject to time-to-delivery constraints due to the highly competitive market, and potential logical errors must be found as early as possible. We describe an approach to improve the development of an actual industrial behavior planner for the Automated Driving Alliance between Bosch and Cariad. The original process landscape for verification and validation is extended with model checking techniques. The idea is to integrate automated extraction mechanisms that, starting from the C++ code of the planner, generate a higher-level model of the underlying logic. This model, composed in closed loop with expressive environment descriptions, can be exhaustively analyzed with model checking. This results, in case of violations, in traces that can be re-executed in system simulators to guide the search for errors. The approach was exemplarily deployed in series development, and successfully found relevant issues in intermediate versions of the planner at development time.


title: Small Test Suites for Active Automata Learning

authors:
Loes Kruger
Sebastian Junges
Jurriaan Rot

abstract: Abstract A bottleneck in modern active automata learning is to test whether a hypothesized Mealy machine correctly describes the system under learning. The search space for possible counterexamples is given by so-called test suites, consisting of input sequences that have to be checked to decide whether a counterexample exists. This paper shows that significantly smaller test suites suffice under reasonable assumptions on the structure of the black box. These smaller test suites help to refute false hypotheses during active automata learning, even when the assumptions do not hold. We combine multiple test suites using a multi-armed bandit setup that adaptively selects a test suite. An extensive empirical evaluation shows the efficacy of our approach. For small to medium-sized models, the performance gain is limited. However, the approach allows learning models from large, industrial case studies that were beyond the reach of known methods.


title: IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL

authors:
Hanna Lachnitt
Mathias Fleury
Leni Aniva
Andrew Reynolds
Haniel Barbosa
Andres Nötzli
Clark W. Barrett
Cesare Tinelli

abstract: Abstract Satisfiability modulo theories (SMT) solvers are widely used to ensure the correctness of safety- and security-critical applications. Therefore, being able to trust a solver’s results is crucial. One way to increase trust is to generate independently checkable proof certificates, which record the reasoning steps done by the solver. A key challenge with this approach is that it is difficult to efficiently and accurately produce proofs for reasoning steps involving term rewriting rules. Previous work showed how a domain-specific language, Rare, can be used to capture rewriting rules for the purposes of proof production. However, in that work, the Rare rules had to be trusted, as the correctness of the rules themselves was not checked by the proof checker. In this paper, we present IsaRare, a tool that can automatically translate Rare rules into Isabelle/HOL lemmas. The soundness of the rules can then be verified by proving the lemmas. Because an incorrect rule can put the entire soundness of a proof system in jeopardy, our solution closes an important gap in the trustworthiness of SMT proof certificates. The same tool also provides a necessary component for enabling full proof reconstruction of SMT proof certificates in Isabelle/HOL. We evaluate our approach by verifying an extensive set of rewrite rules used by the cvc5 SMT solver.


title: Explainable Online Monitoring of Metric First-Order Temporal Logic

authors:
Leonardo Lima
Jonathan Julián Huerta y Munive
Dmitriy Traytel

abstract: Abstract Metric first-order temporal logic (MFOTL) is an expressive formalism for specifying temporal and data-dependent constraints on streams of time-stamped, data-carrying events. It serves as the specification language of several runtime monitors. These monitors input an MFOTL formula and an event stream prefix and output satisfying assignments to the formula’s free variables. For complex formulas, it may be unclear why a certain assignment is output. We propose an approach that accompanies assignments with detailed explanations, in the form of proof trees. We develop a new monitor that outputs such explanations. Our tool incorporates a formally verified checker that certifies the explanations and a visualization that allows users to interactively explore and understand the outputs.


title: A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Teleportation

authors:
Shang-Wei Lin
Tzu-Fan Wang
Yean-Ru Chen
Zhe Hou
David Sanán
Yon Shin Teo

abstract: Abstract Boolean satisfiability (SAT) solving is a fundamental problem in computer science. Finding efficient algorithms for SAT solving has broad implications in many areas of computer science and beyond. Quantum SAT solvers have been proposed in the literature based on Grover’s algorithm. Although existing quantum SAT solvers can consider all possible inputs at once, they evaluate each clause in the formula one by one sequentially, making the time complexityO(m), linear to the number of clausesm,per Grover iteration. In this work, we develop aparallelquantum SAT solver, which reduces the time complexity in each iteration to constant timeO(1) by utilising extra entangled qubits. To further improve the scalability of our solution in case of extremely large problems, we develop a distributed version of the proposed parallel SAT solver based on quantum teleportation such that the total qubits required are shared and distributed among a set of quantum computers (nodes), and the quantum SAT solving is accomplished collaboratively by all the nodes. We prove the correctness of our approaches and evaluate them in simulations and real quantum computers.


title: SWAT: Modular Dynamic Symbolic Execution for Java Applications using Dynamic Instrumentation (Competition Contribution)

authors:
Nils Loose
Felix Mächtle
Florian Sieck
Thomas Eisenbarth

abstract: Abstract SWAT is a novel dynamic symbolic execution engine for Java applications utilizing dynamic instrumentation. SWAT’s unique modular design facilitates flexible communication between its symbolic explorer and executor using HTTP endpoints, thus enhancing adaptability to diverse application scenarios. The symbolic executor’s ability to attach to Java applications enables efficient constraint generation and path exploration. SWAT employs JavaSMT for constraint generation and ASM for bytecode instrumentation, ensuring robust performance. SWAT’s efficacy is evaluated in the Java Track of SV-COMP 2024, achieving fourth place.


title: Rabin Games and Colourful Universal Trees

authors:
Rupak Majumdar
Irmak Saglam
K. S. Thejaswini

abstract: Abstract We provide an algorithm to solve Rabin and Streett games over graphs with n vertices, m edges, and k colours that runs in $$\tilde{O}\left( mn(k!)^{1+o(1)} \right) $$ O ~ m n ( k ! ) 1 + o ( 1 ) time and $$O(nk\log k \log n)$$ O ( n k log k log n ) space, where $$\tilde{O}$$ O ~ hides poly-logarithmic factors. Our algorithm is an improvement by a super quadratic dependence on k! from the currently best known run time of $$O\left( mn^2(k!)^{2+o(1)}\right) $$ O m n 2 ( k ! ) 2 + o ( 1 ) , obtained by converting a Rabin game into a parity game, while simultaneously improving its exponential space requirement. Our main technical ingredient is a characterisation of progress measures for Rabin games using colourful trees and a combinatorial construction of succinctly-represented, universal colourful trees. Colourful universal trees are generalisations of universal trees used by Jurdziński and Lazić (2017) to solve parity games, as well as of Rabin progress measures of Klarlund and Kozen (1991). Our algorithm for Rabin games is a progress measure lifting algorithm where the lifting is performed on succinct, colourful, universal trees.


title: ESBMC v7.4: Harnessing the Power of Intervals - (Competition Contribution)

authors:
Rafael Sá Menezes
Mohannad Aldughaim
Bruno Farias
Xianzhiyu Li
Edoardo Manino
Fedor Shmarov
Kunjian Song
Franz Brauße
Mikhail R. Gadelha
Norbert Tihanyi
Konstantin Korovin
Lucas C. Cordeiro

abstract: Abstract ESBMC implements many state-of-the-art techniques that combine abstract interpretation and model checking. Here, we report on new and improved features that allow us to obtain verification results for previously unsupported programs and properties. ESBMC now employs a new static interval analysis of expressions in programs to increase verification performance. This includes interval-based reasoning over booleans and integers, and forward-backward contractors. Other relevant improvements concern the verification of concurrent programs, as well as several operational models, internal ones, and also those of libraries such as pthread and the C mathematics library. An extended memory safety analysis now allows tracking of memory leaks that are considered still reachable.


title: Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains

authors:
Hannah Mertens
Joost-Pieter Katoen
Tim Quatmann
Tobias Winkler

abstract: Abstract We study the accurate and efficient computation of the expected number of times each state is visited in discrete- and continuous-time Markov chains. To obtain sound accuracy guarantees efficiently, we lift interval iteration and topological approaches known from the computation of reachability probabilities and expected rewards. We further study applications of expected visiting times, including the sound computation of the stationary distribution and expected rewards conditioned on reaching multiple goal states. The implementation of our methods in the probabilistic model checker scales to large systems with millions of states. Our experiments on the quantitative verification benchmark set show that the computation of stationary distributions via expected visiting times consistently outperforms existing approaches — sometimes by several orders of magnitude.


title: PROTON: PRObes for Termination Or Not (Competition Contribution)

authors:
Ravindra Metta
Hrishikesh Karmarkar
Kumar Madhukar
R. Venkatesh
Supratik Chakraborty

abstract: Abstract PROTON is a tool to check whether a given C program has a non-terminating behaviour or not. It is built around the C Bounded Model Checker (CBMC). CBMC cannot prove non-termination directly, as all non-terminating runs are unbounded. PROTON annotates the loops in a given program with assertions that check for a recurrent program state. Violation of such an assertion shows the existence of a recurrent state and thereby proves non-termination. PROTON also transforms the violating trace returned by CBMC into a non-termination witness for the program.


title: Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution)

authors:
Raphaël Monat
Marco Milanese
Francesco Parolini
Jérôme Boillot
Abdelraouf Ouadjaout
Antoine Miné

abstract: Abstract We present advances we brought to Mopsa for SV-Comp 2024. We significantly improved the precision of our verifier in the presence of dynamic memory allocation, library calls such as , -based loops, and integer abstractions. We introduced a witness validator for correctness witnesses. Thanks to these improvements, Mopsa won SV-Comp’sSoftwareSystemscategory by a large margin, scoring 2.5 times more points than the silver medalist, Bubaak-SpLit.


title: Most General Winning Secure Equilibria Synthesis in Graph Games

authors:
Satya Prakash Nayak
Anne-Kathrin Schmuck

abstract: Abstract This paper considers the problem of co-synthesis in k-player games over a finite graph where each player has an individual $$\omega $$ ω -regular specification $$\phi _i$$ ϕ i . In this context, a secure equilibrium (SE) is a Nash equilibrium w.r.t. the lexicographically ordered objectives of each player to first satisfy their own specification, and second, to falsify other players’ specifications. A winning secure equilibrium (WSE) is an SE strategy profile $$(\pi _i)_{i\in [1;k]}$$ ( π i ) i ∈ [ 1 ; k ] that ensures the specification $$\phi :=\bigwedge _{i\in [1;k]}\phi _i$$ ϕ : = ⋀ i ∈ [ 1 ; k ] ϕ i if no player deviates from their strategy $$\pi _i$$ π i . Distributed implementations generated from a WSE make components act rationally by ensuring that a deviation from the WSE strategy profile is immediately punished by a retaliating strategy that makes the involved players lose. In this paper, we move from deviation punishment in WSE-based implementations to a distributed, assume-guarantee based realization of WSE. This shift is obtained by generalizing WSE from strategy profiles to specification profiles $$(\varphi _i)_{i\in [1;k]}$$ ( φ i ) i ∈ [ 1 ; k ] with $$\bigwedge _{i\in [1;k]}\varphi _i = \phi $$ ⋀ i ∈ [ 1 ; k ] φ i = ϕ , which we call most general winning secure equilibria (GWSE). Such GWSE have the property that each player can individually pick a strategy $$\pi _i$$ π i winning for $$\varphi _i$$ φ i (against all other players) and all resulting strategy profiles $$(\pi _i)_{i\in [1;k]}$$ ( π i ) i ∈ [ 1 ; k ] are guaranteed to be a WSE. The obtained flexibility in players’ strategy choices can be utilized for robustness and adaptability of local implementations. Concretely, our contribution is three-fold: (1) we formalize GWSE for k-player games over finite graphs, where each player has an $$\omega $$ ω -regular specification $$\phi _i$$ ϕ i ; (2) we devise an iterative semi-algorithm for GWSE synthesis in such games, and (3) obtain an exponential-time algorithm for GWSE synthesis with parity specifications $$\phi _i$$ ϕ i .


title: Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking

authors:
Muhammad Osama
Anton Wijs

abstract: Abstract The need for massively parallel algorithms, suitable to exploit the computational power of hardware such as graphics processing units, is ever increasing. In this paper, we propose a new algorithm for the on-the-fly verification of Linear-Time Temporal Logic (LTL) formulae [45] that is aimed at running on such devices. We prove its correctness and termination guarantee, and experimentally compare a GPU implementation with state-of-the-art LTL model checkers. Our new GPU LTL-checking algorithm is up to 150 $$\times $$ × faster on proving the correctness of a system than LTSmin running on a 32-core high-end CPU, and is more economic in using the available memory.


title: Weakest Precondition Inference for Non-Deterministic Linear Array Programs

authors:
Sumanth Prabhu
Deepak D'Souza
Supratik Chakraborty
R. Venkatesh
Grigory Fedyukovich

abstract: Abstract Precondition inferenceis an important problem with many applications. Existing precondition inference techniques for programs with arrays have limited ability to find and prove the weakest preconditions, especially when programs have non-determinism. In this paper, we propose an approach to overcome the limitation. As the problem is uncomputable in general, our approach targets a special class of programs called linear array programs that are commonly encountered in practical applications and have been studied before. We also focus on a class of quantified formulas for pre- and postconditions that suffice to specify program properties in many applications. Our approach uses two novel techniques calledStructural Array Abduction(SAA) andSpecialized Maximality Checking(SMC). SAA is an abduction-based technique used to infer quantified preconditions and necessary inductive invariants. SMC proves that an inferred precondition is the weakest by finding an under-approximated program and solving the complement verification problem on it using SAA. When inconclusive, it attempts to weaken the precondition. Our approach can infer (and also prove) the weakest preconditions for a range of benchmarks relatively quickly, and outperforms competing techniques.


title: A Logical Treatment of Finite Automata

authors:
Nishant Rodrigues
Mircea Sebe
Xiaohong Chen
Grigore Rosu

abstract: Abstract We present a sound and complete axiomatization of finite words using matching logic. A unique feature of our axiomatization is that it gives a shallow embedding of regular expressions into matching logic, and a logical representation of finite automata. The semantics of both expressions and automata are precisely captured as matching logic formulae that evaluate to the corresponding language. Regular expressions are matching logic formulae as is, while the embedding of automata is a structural analog—computational aspects of automata are captured as syntactic features. We demonstrate that our axiomatization is sound and complete by showing that runs of Brzozowski’s procedure for equivalence checking correspond to matching logic proofs. We propose this as a general methodology for producing machine-checkable formal proofs, enabled by capturing structural analogs of computational artifacts in logic. The proofs produced can be efficiently checked by the Metamath Zero verifier. Work presented in this paper contributes to the general scheme of achieving verifiable computing via logical methods, where computations are reduced to logical reasoning, encoded as machine-checkable proof objects, and checked by a trusted proof checker.


title: Goblint Validator: Correctness Witness Validation by Abstract Interpretation - (Competition Contribution)

authors:
Simmo Saan
Julian Erhard
Michael Schwarz
Stanimir Bozhilov
Karoliine Holter
Sarah Tilscher
Vesal Vojdani
Helmut Seidl

abstract: Abstract Goblintis an abstract interpretation framework for C programs with a specialty in concurrency. Using a novel approach, we turn it into a validator of YAML correctness witnesses for all SV-COMP categories. We describe its results at SV-COMP 2024 which includes the first large-scale evaluation of our validator.


title: Goblint: Abstract Interpretation for Memory Safety and Termination - (Competition Contribution)

abstract: Abstract Goblintis an abstract interpreter of C programs, focusing on the analysis of multi-threaded code. It is equipped with a variety of abstract domains, as well as analyses which allow it to reason about an array of program properties in a highly configurable manner.Goblinthas been extended with support for the detection of memory safety bugs and non-termination.