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

platform for deductive verification of Java programs

Application domain/field

• design contract
• floating point
• Interactive theorem prover
• Deductive verification
• Functional verification

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.