JBMC was victorious at the International Competition on Software Verification SV-COMP at ETAPS 2019 in Prague.
In addition to the traditional tracks for C programs, the 8th edition of the competition featured a Java track for the first time.
The Java Bounded Model Checker (JBMC) successfully demonstrated that it is ahead of competing tools in analyzing Java bytecode.
JBMC is able to detect exceptions (including runtime exceptions such as NullPointerException or ArrayIndexOutOfBoundsException) that crash a Java program and report the execution trace that led to the error. Moreover, it can prove that a method does not throw runtime exceptions in any input environment.
The International Competition on Software Verification (SV-COMP) is an annual competition of software verification tools which aims to provide a snapshot of the state-of-the-art in software verification.
It compares the performance of fully automatic software verification tools on a benchmark set contributed by the developer community. SV-COMP has been successfully driving research and industrial practice of software verification in the last decade.
We are looking forward to the 2020 competition!
