Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2
Abstract elided by the publisher.
26,098 papers · page 496 of 1,305
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…
Liveness of Randomised Parameterised Systems under Arbitrary Schedulers
We consider the problem of verifying liveness for systems with a finite, but unbounded, number of processes, commonly known as parameterised systems. Typical examples of such systems include distributed protocols (e.g. for the dining philosopher problem). Unlike the case of verif…