Aspects of First-order Reasoning in the KeY system

Description

The deductive program verification system developed as part of the KeY project is based on a sequent calculus for a certain dynamic logic, which is specially tailored to the verification of Java-Card programs. The sequent calculus symbolically executes programs, until proof obligations in first-order logic are obtained. To simplify reasoning about Objects of a Java program, the first-order logic of KeY has strongly typed terms and subtyping. In the context of program verification, it is desirable to be able to phave an integrated interactive and automated theorem prover, and moreover, an automated proof procedure without backtracking is desirable. Theory specific reasoning in KeY is done by enhancing the prover with theory specific rules, known as taclets, which can easily be formulated in a special rule language.

Period	13 Sept 2007
Event title	First Order Theorem Proving (FTP), Liverpool, UK
Event type	Conference
Location	United KingdomShow on map