Automatically Proving the Correctness of Refactoring Rules with Abstract Execution and REFINITY

Automatic, Second-Order
Relational Program Verification

Downloads

You need at least a Java Development Kit (JDK) 8 to run the bundled REFINITY Jar. You can start KeY with REFINITY by simply running “java -jar key-2.7-AE.jar“. Have a look at the descriptions below to get started.

Note: You might experience problems with the KeY extension “Origin Tracking”, which is why we recommend to turn off this feature. You can do so by choosing Options > Show Settings, and unchecking the box at “Origin Tracking” in the “Extensions” category. You have to restart REFINITY/KeY afterward. We are working at ruling out these problems, such that origin tracking can be used together with Abstract Execution.

Example

To see an abstract program model for the equivalence proof of a refactoring in action, download and run KeY-AE and load the example “Extract Prefix” (see screenshot below) from the examples dialog. This will open the REFINITY window for inspection of the model (see screenshots section further down). To edit the model, save it to another place. By clicking the “Play” button in REFINITY’s toolbar, a proof obligation will be created and loaded in the KeY main window. Proof search will start automatically. In the lower right of the status bar in REFINITY, you get some information about the current proof status. You can also directly inspect the status in the KeY main window, which is especially useful if a proof does not close (e.g., because the model is not correct, or because of a prover incapacity).

Path in the Examples Dialog to the “Extract Prefix” Example.
All “Abstract Execution” examples will start the REFINITY user interface.

Screenshots

The Button for Starting REFINITY

Changelog

## 2019-12-29 (v0.9.3) Dominic Steinhoefel <steinhoefel@cs.tu-darmstadt.de>

  * Changed AE rules: Initialization of result and exception objects in abstract update scope. Breaks
    backwards compatibility with existing proofs!
  * Adapted Strategies: Simplification of abstract updates has now same priority as simplification of
    concrete update. Leads to a performance boost.

## 2019-12-06 (v0.9.2) Dominic Steinhoefel <steinhoefel@cs.tu-darmstadt.de>

  * Bug fixes in conversion to KeY file
  * Different behavior when pressing Ctrl+S for yet unsaved model: Show dialog instead of status message
  * Fixed bug in pre- postcondition relation fields about unrecognized symbols which actually have been added

## 2019-12-06 (v0.9.1) Dominic Steinhoefel <steinhoefel@cs.tu-darmstadt.de>

  * Supporting relational preconditions
  * Better heap simplification (abstract update simplification for select expressions, removing 
    ineffective anonymizations) 

## 2019-12-05 (v0.9) Dominic Steinhoefel <steinhoefel@cs.tu-darmstadt.de>

  * JML Support for relation to verify
  * Fixed compilation bug when using Java 8
  * Started KeY-independent versioning, displaying version number in title

Relevant Blog Posts

References

2019

Steinhöfel, Dominic; Hähnle, Reiner

Abstract Execution Inproceedings

ter Beek, Maurice H; McIver, Anabelle; Oliveira, José N (Ed.): Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings, pp. 319–336, Springer, Cham, 2019, ISBN: 978-3-030-30941-1.

Abstract | Links | BibTeX