ESBMC (Efficient SMT-Based Context-Bounded Model Checker)
line decor
line decor

APPLICATIONS
 

Bounded Model Checking of State-Space Digital Systems

ESBMC is used to verify State-Space Digital Systems.

Verificação de Códigos Lua Utilizando BMCLua

ESBMC is used to verify a C version of the respective Lua program.

CSeq: A Sequentialization Tool for C

ESBMC is used as sequential verification back-end to model check multi-threaded programs.

Sound and Unified Software Verification for Weak Memory Models

ESBMC is used as a sequential consistency software verification tool in real-life C programs.

Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples

The counter-example produced by ESBMC is used to automatically debug software systems.

Verifying Embedded C Software with Timing Constraints using an Untimed Model Checker

ESBMC is used as an untimed software model checker to verify real-time software.

Scalable hybrid verification for embedded software

ESBMC is used as a verification engine to model check embedded (sequential) software.

Getting Rid of Store-Buffers in TSO Analysis

ESBMC is used to verify sequential consistency concurrent C programs.