ReFuncTion: Conditional Termination by Abstract Interpretation of Numerical C Programs - (Competition Contribution)
Abstract elided by the publisher.
21,147 papers · page 21 of 1,058
Goblint: A Portfolio for Mixed Flow-Sensitive Abstract Interpretation - (Competition Contribution)
Abstract elided by the publisher.
Trace Repair for Temporal Behavior Trees
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…
Real-time Proof Checking for Distributed Incremental SAT Solving
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 …
Massively Parallel Bit-Precise Verification with Bitwuzla and Mallob
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…
Exploring the SMT-LIB Benchmark Library
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…
Re3ver: Reverse and Verify - (Competition Contribution)
Abstract elided by the publisher.
VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
Abstract elided by the publisher.
Data Structure Analysis for Binaries
Abstract elided by the publisher.
Automatically Tightening Access Control Policies with Restricter
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…
Quantifier Elimination Meets Treewidth
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…
Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver
Abstract elided by the publisher.
Reachability in Multi-agent Transfer Systems
Abstract elided by the publisher.
Efficiently Verifying Quantum Programs with Few T Gates
Abstract elided by the publisher.
Atomic Gliders and Cellular Automata as Language Generators
Abstract elided by the publisher.
A Hybrid Meta-Learning Framework for Adaptive Safe Controller Synthesis of Dynamic Systems
Abstract elided by the publisher.
Proof Minimization in Neural Network Verification
Abstract elided by the publisher.
Finding Photonics Circuits via δ-Weakening SMT
For quantum computers based on photonics, one main problem is the synthesis of a photonic circuit that emulates quantum computing gates. The problem requires using photonic components to build a circuit that act like a quantum computing gate with some probability of success. This…
Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
Control flow in unstructured programs can be complex and dynamic, which makes static analysis difficult. Yet, automated reasoning about unstructured control flow is important when certifying properties of binary (machine) code in trustworthy systems, e.g., cryptographic routines.…
SAT-Based Synthesis of Minimal Deterministic Real-Time Automata via 3DRTA Representation
Abstract elided by the publisher.