tools

BMCLua

The goal of the BMCLua is to extend the features of ESBMC, which is a context-bounded model checker for embedded software C/C++, for the Lua programming language. The ESBMC model checker is based on Satisfiability Modulo Theories (SMT) solvers. The BMCLua runs in the Linux operating system, requiring the instalation of the ESBMC software and a Lua interpreter. As the BMCLua is developed in Java, it also is necessary to install the JRE for Linux.

DepthK

DepthK is a software verification tool that employs a proof by induction algorithm that combines k-induction with invariant inference. In order to e fficiently and effectively verify and falsify safety properties in C programs, DepthK infers program invariants using polyhedral constraints.

DSVerifier

DSVerifier (Digital Systems Verifier) is a bounded model checker to aid enginners to check for overflow, limit cycle, error, timing, stability, and minimum phase in digital systems, considering finite word length (FWL) effects.

ESBMC

ESBMC is a context-bounded model checker for embedded C/C++ software based on Satisfiability Modulo Theories (SMT) solver. It allows the verification engineer to verify single- and multi-threaded software (with shared variables and locks); to reason about arithmetic under- and overflow, pointer safety, memory leaks, array bounds, atomicity and order violations, deadlock and data race; to verify programs that make use of bit-level, pointers, structs, unions and fixed-point arithmetic.

ESBMC-GPU

ESBMC-GPU is a context-bounded model checker based on the satisfiability modulo theories (SMT) to check for data race, deadlock, pointer safety, array bounds, arithmetic overflow, division by zero, and user-specified assertions in programs written in Compute Unified Device Architecture (CUDA).

EZProofC

EZProofC automates the collection and manipulation of counterexamples to generate new instantiated code to reproduce the identified error.

Map2Check

Map2Check is a tool for automatically generating and checking unit tests for C programs. The generation of unit tests is based on assertions extracted from (memory) safety properties, which are generated by the ESBMC tool. In particular, Map2Check checks for invalid-free, invalid-dereference, and memory-leak properties in C programs.

QtOM

Qt Operational Model (QtOM) is an abstract representation of the Qt Cross-Platform Framework. Qt Operational Model (QtOM) is an abstract representation of the Qt Cross-Platform Framework. Indeed, QtOM is integrated into a bounded model checking (BMC) tool based on satisfiability modulo theories (SMT), known as the Efficient SMT-based Context-Bounded Model Checker (ESBMC++), in order to verify specific properties in Qt/C++ programs.

JBMC

JBMC is a bounded model checker for Java bytecode, built on the CProver framework. It verifies memory safety, exceptions and user-specified assertions, and takes part in the Java track of the international competition on software verification.