1,553 papers · page 4 of 78
We present DeGAS, a differentiable Gaussian approximate semantics for loopless probabilistic programs that enables sample-free, gradient-based optimization in models with both continuous and discrete components. DeGAS evaluates programs under a Gaussian-mixture semantics and repl…
Abstract elided by the publisher.
Abstract elided by the publisher.
We present methods for repairing traces against specifications given as temporal behavior trees (TBT). TBT are a specification formalism for action sequences in robotics and cyber-physical systems, where specifications of sub-behaviors, given in signal temporal logic, are compose…
Distributed clause-sharing SAT solvers are powerful automated reasoning tools capable of rapidly solving many difficult instances. Users of SAT solving often rely on incremental SAT solving, i.e., interactive solve calls over an evolving formula. We present the first approach to …
We present a distributed platform for massively parallel SMT solving that supports various theories for bit-precise reasoning, with and without quantifiers and push-pop incrementality. Our system is based on an integration of the state-of-the-art SMT solver Bitwuzla into the dist…
The SMT-LIB benchmark collection is a large set of problems for SMT solvers. It has been continuously maintained and expanded since its creation in the early 2000s by the SMT-LIB initiative. It has been used since 2005 by the annual SMT solver competition to compare the performan…
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Robust access control is a cornerstone of secure software, systems, and networks. An access control mechanism is as effective as the policy it enforces. However, authoring effective policies that satisfy desired properties such as the principle of least privilege is a challenging…
In this paper, we address the complexity barrier inherent in Fourier-Motzkin elimination (FME) and cylindrical algebraic decomposition (CAD) when eliminating a block of (existential) quantifiers. To mitigate this, we propose exploiting structural sparsity in the variable dependen…
Abstract Machine-assisted theorem proving refers to the process of conducting structured reasoning to automatically generate proofs for mathematical theorems. Recently, there has been a surge of interest in using machine learning models in conjunction with proof assistants to per…
Abstract The International Competition on Software Verification (SV-COMP) has been an important driver of progress in the formal verification community, fostering tool development, benchmarking, and reproducibility. As the competition grows in scale and complexity, a reproducibil…
Abstract Analyzing concurrent programs often involves reasoning about happens-before relations, handled by dedicated SMT theory solvers. Recently, preventative propagation rules have been introduced for consistency models to avoid unnecessary computations. This paper analyses the…
Abstract Recent advances in satisfiability modulo theories have brought practical software verification within reach. The advent of the LLVM project presents a common representation which allows verification between programs written in different languages such as C and Rust. New …
Abstract Automatic decision and prediction systems are increasingly deployed in applications where they significantly impact the livelihood of people, such as for predicting the creditworthiness of loan applicants or the recidivism risk of defendants. These applications have give…
Abstract CPAchecker is a tool for software verification, witness validation, and test-case generation, based on the concept of configurable program analysis. One of its main applications is to validate correctness and violation witnesses in versions 1.0 and 2.0. The witness valid…
Abstract The 14th edition of the Competition on Software Verification (SV-COMP 2025) evaluated 62 verification tools and 18 witness validation tools, making it the largest comparison of its kind so far. Out of these, 35 verification and 13 validation tools participated with an ac…
Abstract Ordered binary decision diagrams (OBDDs) are a fundamental data structure for the manipulation of Boolean functions, with strong applications to finite-state symbolic model checking. OBDDs allow for efficient algorithms using top-down dynamic programming. From an automat…