Lazy Abstraction with Interpolants
Abstract elided by the publisher.
2,069 papers · page 68 of 104
EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation
Abstract elided by the publisher.
The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover
Abstract elided by the publisher.
SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation
Abstract elided by the publisher.
Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor Synthesis
Abstract elided by the publisher.
Fast and Generalized Polynomial Time Memory Consistency Verification
The problem of verifying multi-threaded execution against the memory consistency model of a processor is known to be an NP hard problem. However polynomial time algorithms exist that detect almost all failures in such execution. These are often used in practice for microprocessor…
CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools
Abstract elided by the publisher.
Model Checking Multithreaded Programs with Asynchronous Atomic Methods
Abstract elided by the publisher.
cascade: C Assertion Checker and Deductive Engine
Abstract elided by the publisher.
Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation
Abstract elided by the publisher.
LEVER: A Tool for Learning Based Verification
Abstract elided by the publisher.
Antichains: A New Algorithm for Checking Universality of Finite Automata
Abstract elided by the publisher.
Improved Probabilistic Models for 802.11 Protocol Verification
Abstract elided by the publisher.
Symbolic Compositional Verification by Learning Assumptions
Abstract elided by the publisher.
The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications
Abstract elided by the publisher.
Formal Verification of Backward Compatibility of Microcode
Abstract elided by the publisher.
IIV: An Invisible Invariant Verifier
Abstract elided by the publisher.
Model Checking x86 Executables with CodeSurfer/x86 and WPDS++
Abstract elided by the publisher.
Abstraction for Falsification
Abstract elided by the publisher.
Wolf - Bug Hunter for Concurrent Software Using Formal Methods
Abstract elided by the publisher.