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

NEWS

NEW!22/01/2016: ESBMC v2.1 won one gold and one silver medal in the 5th International Competition on Software Verification (SV-COMP 2016).

NEW!ESBMC v2.0.0 is now open source

19/12/2014: ESBMC v1.24.1 won two gold and two bronze medals in the 4th International Competition on Software Verification (SV-COMP 2015).

13/12/2013: 20/11/2014: ESBMC v1.24.1 for Linux released for the SV-COMP 2015.

13/12/2013: ESBMC v1.22 won the gold medal in the SequentializedConcurrent category of the Third Intl. Competition on Software Verification (SVCOMP'14).

26/04/2013: ESBMC++ v1.21 for Linux released.

19/02/2013: ESBMC v1.21 for Linux released.

09/01/2013: ESBMC v1.20 won the  Bronze Medal in the overall ranking of the second Intl. Competition on Software Verification (SVCOMP'13).

20/01/2012: ESBMC v1.18 for Linux and Windows released.

12/12/2011: ESBMC v1.17 won the Gold Medal in the "SystemC" and "Concurrency" categories and the  Bronze Medal in the overall ranking of the first Intl. Competition on Software Verification (SVCOMP'12).

11/01/2011: The collaboration between Southampton and Manaus is now supported by the Royal Society through an International Exchange grant.

10/05/2011: Support for state hashing to reduce the state space exploration (to enable it use the option --state-hashing).

08/11/2010: Preliminary support for writing an SMT formula into a file (use the options --qf_aufbv or --qf_auflira followed by --outfile filename.smt).

18/10/2010: Preliminary support for memory leak detection (use the option --memory-leak-check).

13/10/2010: Support for static partial order reduction (to disable it use the option --no-por).

29/09/2010: We provide an Eclipse plug-in for ESBMC.

17/09/2010: Support for checking atomicity violation at visible statements (use the option --atomicity-check).

19/03/2010: ESBMC v1.3 supports the verification of multi-threaded software with shared variable communication between the threads.