PV6 KeYgenerates a proof of desired properties, can proceed interactively if stuck otherwise

platform for deductive verification of Java programs

Application domain/field

Type of tool

Semi-interactive verifier

Expected input

Annotated source code

Format:

(Sequential) Java or Java Card 2.2.X program annotated with properties specified in JML or Java Dynamic Logic (JavaDL).

Expected output

Whether the specified properties can be proven correct.

Internals

translates source code to JavaDL. can translate to the SMT-LIB format and call an external SMT solver. The user can choose to use the tool in an automatic or interactive fashion. Typically the user would first try to let the prover find a proof automatically, if it then does not succeed, the user can get involved in the proving process.
Java

Links

Project page: https://www.key-project.org/

Last commit date

Latest stable release is from 18 December 2020 (https://www.key-project.org/download/).

Related papers

Last publication date

23 March 2021

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.