Aspects of First-order Reasoning in the KeY system
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
First Order Theorem Proving (FTP), Liverpool, UK
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
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.
Sprache der Kurzfassung:
Englisch
Vortragstyp:
Hauptvortrag / Eingeladener Vortrag auf einer Tagung