# Proof Script Debugger for the KeY System The proof script debugger is a prototypical implementation of an interaction concept for program verification systems that are rule based and use a program logic. The prototype is implemented on top of the interactive program verification system [KeY](http://www.key-project.org). KeY is an interactive program verification system for Java program annotated with the Java Modeling Language (JML). The protypical implementation includes a proof scripting language that is tailored to the problem domain of program verification. The main features of the language are: 1. integration of domain specific entities like goal, formula, term and rule as first-class citizens into the language; 1. an expressive proof goal selection mechanism * to identify and select individual proof branches, * to easily switch between proof branches, * to select multiple branches for uniform treatment (multi-matching); that is resilient to small changes in the proof 1. a repetition construct which allows repeated application of proof strategies; 1. support for proof exploration within the language. Together with the proof scripting language a debugging concept for failed proof attempts is implemented that leverages well-known concepts from program debugging to the analysis of failed proof attempts. ## Publications A full description of the language and debugging-concept is published at [HVC 2017](http://rdcu.be/E4fF) ## Features

Inspection of different parts of the proof state

The different parts of the proof state can be inspected:

Adjustable view on list of open goals

Explore the proof tree of KeY

Set a breakpoint and run execution to breakpoint

Mark lines with an (conditional) breakpoint to pause the script execution.

Stepwise evaluation for time travellers

Stepwise script execution: step over and into. Our special offers for time travellers: Go backwards in time and then Back to the Future,again!

Interactive Rule Application

Select rules for interactive application.

Getting Started

Downloads