642 papers · page 1 of 33
Reachability in Multi-agent Transfer Systems
Efficiently Verifying Quantum Programs with Few T Gates
Atomic Gliders and Cellular Automata as Language Generators
A Hybrid Meta-Learning Framework for Adaptive Safe Controller Synthesis of Dynamic Systems
Proof Minimization in Neural Network Verification
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
Try-Mopsa: Relational Static Analysis in Your Pocket
Input-Based Three-Valued Abstraction Refinement
Unlike Counterexample-Guided Abstraction Refinement (CEGAR), Three-Valued Abstraction Refinement (TVAR) is able to verify all properties of the mu-calculus. We present a novel algorithmic framework for TVAR that employs a simulator-like approach to build and refine the abstract s…
Efficient Discovery of Actual Causality in Stochastic Systems
Identifying the actual cause of events in engineered systems is a fundamental challenge in system analysis. Finding such causes becomes more challenging in the presence of noise and stochastic behavior in real-world systems. In this paper, we adopt the notion of probabilistic act…
Termination Resilience Static Analysis
Verification of Generic VHDL Designs and Their Translation to Rocq
Data Race Detection by Digest-Driven Abstract Interpretation
Multi-variable Quantification of BDDs in External Memory using Nested Sweeping
A Formal Executable Semantics of PROMELA
Probabilistic Verification for Modular Network-on-Chip Systems
A Static Analysis of Entanglement
1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
Despite the advances in probabilistic model checking, the scalability of the verification methods remains limited. In particular, the state space often becomes extremely large when instantiating parameterized Markov decision processes (MDPs) even with moderate values. Synthesizin…