NEW! 25/07/2018: Our NIER paper Towards Counterexample-Guided k-Induction for Fast Bug Detection has been accepted at ESEC/FSE 2018.
NEW! 24/07/2018: ESBMC v5.1.0 for Linux released.
NEW! 03/07/2018: Our tool paper ESBMC 5.0: An Industrial-Strength C Model Checker has been accepted at ASE 2018.
NEW! 16/01/2018: ESBMC-kind won the Bronze Medal in the overall ranking of the 7th International Competition on Software Verification (SV-COMP 2018).
8/05/2017: The talk at FOSDEM 2017 on "Using clang as a Frontend on a Formal Verification Tool" is now available here.
2/03/2017: ESBMC v3.2 won one silver and one bronze medal in the 6th International Competition on Software Verification (SV-COMP 2017).
22/01/2016: ESBMC v2.1 won one gold and one silver medal in the 5th International Competition on Software Verification (SV-COMP 2016).
22/06/2015: 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.