Petruchio: From Dynamic Networks to Nets

PESSOA: A tool for embedded controller synthesis.

Dsolve: Verification Via Liquid Type Inference

SPLIT: A Compositional LTL Verifier

PARAM: A Model Checker for Parametric Markov Models

LTSMIN: Distributed and Symbolic Reachability

RATSY - A new Requirements Analysis Tool with Synthesis

Comfusy: A Tool for Complete Functional Synthesis

JTLV : A Framework for Developing Verification Algorithms

GIST: A Solver for Probabilistic Games

libalf: the Automata Learning Framework

A NuSMV Extension for Graded-CTL Model Checking

A Model Checker for AADL

Merit: an Interpolating Model-Checker

The Static Driver Verifier Research Platform

CONTESSA: Concurrency Testing Augmented with Symbolic Analysis

Breach, A Simulation-based Toolbox for the Verification and  Parameter Synthesis of Hybrid Systems

Quantifier elimination by lazy model enumeration

Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification

A Dash of Fairness for Compositional Reasoning

Model Checking of Linearizability of Concurrent List Implementations

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

On Array Theory of Bounded Elements

An Abstraction-Refinement Approach to Verification of Artificial Neural Networks

Simulation Subsumption in Ramsey-based Buchi Automata Universality and Inclusion Testing

Efficient Emptiness Check for Timed Buchi 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

Robustness in the Presence of Liveness

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

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

Generating Litmus Tests for Contrasting Memory Consistency Models

Abstract Analysis of Symbolic Executions

Termination Analysis with Compositional Relations

Lazy Annotation for Program Testing and Verification

Safety Verification for Probabilistic Hybrid Systems