Quantifier elimination by lazy model enumeration
Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification
SPLIT: A Compositional LTL Verifier
A Dash of Fairness for Compositional Reasoning
Model Checking of Linearizability of Concurrent List Implementations
JTLV : A Framework for Developing Verification Algorithms
PARAM: A Model Checker for Parametric Markov Models
The Static Driver Verifier Research Platform
Model-checking parameterized concurrent programs using linear interfaces
Bounded Underapproximations
Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs
Symbolic Bounded Synthesis
GIST: A Solver for Probabilistic Games
libalf: the Automata Learning Framework
On Array Theory of Bounded Elements
An Abstraction-Refinement Approach to Verification of Artificial Neural Networks
Comfusy: A Tool for Complete Functional Synthesis
Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing
A NuSMV Extension for Graded-CTL Model Checking
RATSY - A new Requirements Analysis Tool with Synthesis
Efficient Emptiness Check for Timed Büchi Automata
Automated Assume-Guarantee Reasoning through Implicit Learning
A Logical Product Approach to Zonotope Intersection
Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems
Achieving Distributed Control Through Model Checking
A Model Checker for AADL
Robustness in the Presence of Liveness
Petruchio: From Dynamic Networks to Nets
CONTESSA: Concurrency Testing Augmented with Symbolic Analysis
Fast Acceleration of Ultimately Periodic Relations
Invariant Synthesis for Programs Manipulating Lists with Unbounded Data
Dynamic Cutoff Detection in Parameterized Concurrent Programs
Fences in Weak Memory Models
Automatically proving linearizability
Directed Proof Generation for Machine Code
Global Reachability in Bounded Phase Multi-Stack Pushdown Systems
Breach, A Simulation-based Toolbox for the Verification and Parameter Synthesis of Hybrid Systems
Verifying Low-Level Implementations of High-Level Datatypes
Measuring and Synthesizing Systems in Probabilistic Environments
Local Verification of Global Invariants in Concurrent Programs
Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication Fabrics
Learning Component Interfaces with May and Must Abstractions
Merit: an Interpolating Model-Checker
LTSMIN: Distributed and Symbolic Reachability
Generating Litmus Tests for Contrasting Memory Consistency Models
Abstract Analysis of Symbolic Executions
Termination Analysis with Compositional Relations
PESSOA: A tool for embedded controller synthesis.
Dsolve: Verification Via Liquid Type Inference
Lazy Annotation for Program Testing and Verification
Safety Verification for Probabilistic Hybrid Systems