1,553 papers · page 7 of 78
Abstract Many verification tools currently rely on logic solvers as backend reasoning engines. Despite playing such a pivotal role, bugs are not uncommon in the complex codebases of these solvers. Validating their results is thus critical, with correctness witnesses often being u…
Abstract In the evolving landscape of SAT solving, leveraging parallel computation has become increasingly significant. The portfolio strategy, combined with clause sharing, has emerged as the leading approach for both local and distributed parallelization on CPUs. Frameworks suc…
Abstract We present a data-driven approach for producing policies that are provably robust across unknown stochastic environments. Existing approaches can learn models of a single environment as an interval Markov decision processes (IMDP) and produce a robust policy with a proba…
Abstract We present , a tool for automatically proving (non-) confluence and termination of logically constrained rewrite systems. We compare to other tools for logically constrained rewriting. Extensive experiments demonstrate the promise of .
Abstract Branch-and-bound (BaB) is among the most effective techniques for neural network (NN) verification. However, existing works on BaB for NN verification have mostly focused on NNs with piecewise linear activations, especially ReLU networks. In this paper, we develop a gene…
Abstract Model checking is a technique to automatically establish whether a model of the behaviour of a system meets its requirements. Evidence explaining why the behaviour does (not) meet its requirements is essential for the user to understand the model checking result. Willems…
Abstract Theta is a model checking framework with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. In SV-COMP 2025, we complement our existing approach (abstraction-aware partial order reduction) for multi-threaded program…
Abstract When validated neural networks (NNs) are pruned (and retrained) before deployment, it is desirable to prove that the new NN behaves equivalently to the (original) reference NN. To this end, our paper revisits the idea of differential verification which performs reasoning…
Abstract Mission-time Linear Temporal Logic (MLTL), a widely used subset of popular specification logics like STL and MTL, is often used to model and verify real world systems in safety-critical contexts. As the results of formal verification are only as trustworthy as their inpu…
Abstract ESBMC v7.7 improves the verification of concurrent C programs by incorporating techniques such as dynamic thread scheduling, incremental SMT solving, and partial order reduction (POR). These improvements enhance the tool’s performance, particularly in exploring complex m…
Abstract Reactive synthesis is an automated process for deriving correct-by-construction reactive systems from temporal specifications. GR(1), in particular, is a popular LTL fragment that balances efficient synthesis complexity and expressiveness. In this paper, we present a set…
Abstract There has been a massive interest in utilizing Linear Temporal Logic on finite traces ( $$\textsc {ltl}_f$$ L T L f ) as a specification language in the last decade, particularly in reactive synthesis. This highlights the need for a unified and efficient framework to ful…
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 t…
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, tra…
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. I…
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 lib…
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 s…
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 in…
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…
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 reach…