Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement
Abstract elided by the publisher.
2,069 papers · page 37 of 104
Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2
Abstract elided by the publisher.
Property Directed Equivalence via Abstract Simulation
Abstract elided by the publisher.
Bounded Cycle Synthesis
We introduce a new approach for the synthesis of Mealy machines from specifications in linear-time temporal logic (LTL), where the number of cycles in the state graph of the implementation is limited by a given bound. Bounding the number of cycles leads to implementations that ar…
Combining Model Learning and Model Checking to Analyze TCP Implementations
Abstract elided by the publisher.
BDD-Based Boolean Functional Synthesis
Abstract elided by the publisher.
XSat: A Fast Floating-Point Satisfiability Solver
Abstract elided by the publisher.
Model Checking at Scale: Automated Air Traffic Control Design Space Exploration
Abstract elided by the publisher.
PSI: Exact Symbolic Inference for Probabilistic Programs
Abstract elided by the publisher.
RV-Match: Practical Semantics-Based Program Analysis
Abstract elided by the publisher.
A Simple Algorithm for Solving Qualitative Probabilistic Parity Games
Abstract elided by the publisher.
Learning-Based Assume-Guarantee Regression Verification
Abstract elided by the publisher.
ParCoSS: Efficient Parallelized Compiled Symbolic Simulation
Abstract elided by the publisher.
Soufflé: On Synthesis of Program Analyzers
Abstract elided by the publisher.
Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata
Abstract elided by the publisher.
JayHorn: A Framework for Verifying Java programs
Abstract elided by the publisher.
Fast, Flexible, and Minimal CTL Synthesis via SMT
Abstract elided by the publisher.
Satisfiability Modulo Heap-Based Programs
Abstract elided by the publisher.
A SAT-Based Counterexample Guided Method for Unbounded Synthesis
Abstract elided by the publisher.
Trigger Selection Strategies to Stabilize Program Verifiers
SMT-based program verifiers often suffer from the so-called butterfly effect, in which minor modifications to the program source cause significant instabilities in verification times, which in turn may lead to spurious verification failures and a degraded user experience. This pa…