thufv / deagle Goto Github PK

# About

Deagle is an SMT-based concurrent program verification tool. It is built on top of CBMC (front-end) and MiniSAT (back-end). The basic idea of Deagle is to integrate into the SAT solver an ordering consistency theory that handles ordering relations over shared variable accesses in the program. The front-end encodes the input program into an extended Boolean formula that contains ordering constraints. The back-end is reinforced with a solver for the ordering consistency theory. Additionally, Deagle transplants some features from Yogar-CBMC for availability, including preprocessing and counterexample generation.

Please refer to https://github.com/thufv/Deagle for our source code.

# Compile

Run command "cd src & make"
This generates executable deagle in directory src/cbmc.

# Usage

./deagle --32 --no-unwinding-assertions --closure [*.i]