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


(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.


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.


Related papers

Last publication date

23 March 2021

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.