index.md 4.82 KB
Newer Older
Alexander Weigl's avatar
Alexander Weigl committed
1 2
<style>
        #content {
Alexander Weigl's avatar
Alexander Weigl committed
3
            width: 50em;
Alexander Weigl's avatar
Alexander Weigl committed
4 5 6 7 8 9 10 11 12 13
            margin: auto;
            border: 1px #ccc solid;
            border-bottom-left-radius: 2em;
            border-top-right-radius: 2em;
            background: ghostwhite;
            padding: 2em;
        }

        .column>div{
            float: left;
Alexander Weigl's avatar
Alexander Weigl committed
14 15
            width: 30%;
            margin:1%;
16
            text-align: left;
Alexander Weigl's avatar
Alexander Weigl committed
17 18 19 20 21 22
        }

        .column img {
            width: 150px;
            text-align: center;
        }
Alexander Weigl's avatar
Alexander Weigl committed
23 24
        
        img.thumb {
Alexander Weigl's avatar
Alexander Weigl committed
25
            width:100%;           
Alexander Weigl's avatar
Alexander Weigl committed
26
            border-radius:50%;
Alexander Weigl's avatar
Alexander Weigl committed
27
        }
Alexander Weigl's avatar
Alexander Weigl committed
28 29
       
       .column h3 {
Alexander Weigl's avatar
Alexander Weigl committed
30
            text-align:center;
Alexander Weigl's avatar
Alexander Weigl committed
31 32 33
       }
       
       div.feature-caption {
Alexander Weigl's avatar
Alexander Weigl committed
34
           text-align: block;           
Alexander Weigl's avatar
Alexander Weigl committed
35 36
           text-align: justify;
           font-size: 80%;
Alexander Weigl's avatar
Alexander Weigl committed
37
           font-weight:bold;
Alexander Weigl's avatar
Alexander Weigl committed
38 39
       }
       
Alexander Weigl's avatar
Alexander Weigl committed
40 41
</style>

Alexander Weigl's avatar
Alexander Weigl committed
42
# Proof Script Debugger for the KeY System
Alexander Weigl's avatar
Alexander Weigl committed
43

Alexander Weigl's avatar
Alexander Weigl committed
44
The proof script debugger is a prototypical implementation
Alexander Weigl's avatar
Alexander Weigl committed
45 46 47
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
48
[KeY](http://www.key-project.org). KeY is an interactive program verification
Alexander Weigl's avatar
Alexander Weigl committed
49 50
system for Java program annotated with the Java Modeling Language (JML).

Alexander Weigl's avatar
Alexander Weigl committed
51

Alexander Weigl's avatar
Alexander Weigl committed
52 53
The protypical implementation includes a proof scripting language that is tailored to the
problem domain of program verification.
54
The main features of the language are:
Alexander Weigl's avatar
Alexander Weigl committed
55 56

1. integration of domain specific entities like goal, formula, term and rule as
57
first-class citizens into the language;</li>
Alexander Weigl's avatar
Alexander Weigl committed
58 59 60 61 62 63 64 65 66
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;</li>
1. support for proof exploration within the language.</li>


Alexander Weigl's avatar
Alexander Weigl committed
67 68 69
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.
70

Alexander Weigl's avatar
Alexander Weigl committed
71 72 73
## Publications

A full description of the language and debugging-concept 
74
is published at [HVC 2017](http://rdcu.be/E4fF)
Alexander Weigl's avatar
Alexander Weigl committed
75

Sarah Grebing's avatar
Sarah Grebing committed
76 77
## Debugging Script for Quicksort's `split` method.

Alexander Weigl's avatar
Alexander Weigl committed
78 79

<center>
Sarah Grebing's avatar
Sarah Grebing committed
80 81 82
The video will be uploaded on 23th, January. 

<!--
Alexander Weigl's avatar
Alexander Weigl committed
83 84 85 86
<video width="80%"  controls>
  <source src="quicksort.webm" type="video/webm">
Your browser does not support the video tag or WebM.
</video>
Sarah Grebing's avatar
Sarah Grebing committed
87
-->
Alexander Weigl's avatar
Alexander Weigl committed
88
</center>
89

Alexander Weigl's avatar
Alexander Weigl committed
90
## Features
Alexander Weigl's avatar
Alexander Weigl committed
91 92

<div class="column">
Alexander Weigl's avatar
Alexander Weigl committed
93
    <div>
94
        <h3>Inspection of different parts of the proof state</h3>
95
        <p> 
96 97
        The different parts of the proof state can be inspected:
        <ul>
Alexander Weigl's avatar
Alexander Weigl committed
98 99 100 101
        <li>list of open goals</li>
        <li>sequent of selected open goal</li>
        <li>path through program (if existing) for selected open goal</li>
        </ul>
102
        </p> 
Alexander Weigl's avatar
Alexander Weigl committed
103 104
    </div>
    <div >
105
        <h3>Adjustable view on list of open goals</h3>
Alexander Weigl's avatar
Alexander Weigl committed
106
        <img class="thumb" src="img/thumb_ScreenshotGoalList.png" />
Alexander Weigl's avatar
Alexander Weigl committed
107
        <div class="feature-caption"/></div>
Alexander Weigl's avatar
Alexander Weigl committed
108 109
    </div>
    <div >
110
        <h3>Explore the proof tree of KeY</h3>
Alexander Weigl's avatar
Alexander Weigl committed
111 112
        <img class="thumb" src="img/thumb_ScreenshotProofTree.png"/>
        <div class="feature-caption"/></div>
Alexander Weigl's avatar
Alexander Weigl committed
113 114 115
    </div>
</div>
<div style="clear: both;"/>
Alexander Weigl's avatar
Alexander Weigl committed
116 117 118 119 120 121 122

<div class="column">
    <div>
        <h3>Set a breakpoint and run execution to breakpoint</h3>
        <img src="img/thumb_ScreenshotBreakpoint.png" class="thumb"/>
        <div class="feature-caption">
            Mark lines with an (conditional) breakpoint to pause the script execution.
Alexander Weigl's avatar
Alexander Weigl committed
123
        </div>
Alexander Weigl's avatar
Alexander Weigl committed
124 125 126 127 128 129 130 131
    </div>
    <div> 
        <h3>Stepwise evaluation for time travellers</h3>
        <img src="img/thumb_ScreenshotStep.png" class="thumb" />
        <div class="feature-caption">
            Stepwise script execution: step over and into.
            Our special offers for time travellers: Go backwards in time
            and then Back to the Future,again!
Alexander Weigl's avatar
Alexander Weigl committed
132 133
        </div>
    </div>
Alexander Weigl's avatar
Alexander Weigl committed
134 135 136 137 138 139 140
    <div> 
      <h3> Interactive Rule Application</h3>
        <img src="img/thumb_ScreenshotInteractive.png" class="thumb" />
        <div class="feature-caption">
        Select rules for interactive application.
        </div>
  </div>
Alexander Weigl's avatar
Alexander Weigl committed
141 142 143 144
</div>

<div style="clear: both;"/> 

Alexander Weigl's avatar
Alexander Weigl committed
145
<h2>Downloads</h2>
Alexander Weigl's avatar
Alexander Weigl committed
146

Alexander Weigl's avatar
Alexander Weigl committed
147
<ul>
Sarah Grebing's avatar
Sarah Grebing committed
148
 <li>PSDBG - <strong>Version 1.0-FM will be available at 23th, January</strong> 
Alexander Weigl's avatar
Alexander Weigl committed
149 150
    <a href="~/releases/psdbg-1.0-fm.jar">psdbg-1.0-fm.jar</a>
    <br>
151 152 153 154
    Special Version for the tool paper at Formal Methods 2018.
    Including examples and all dependencies.
    <br>
    <a href="https://www.gnu.org/licenses/gpl-3.0.txt">License: GPLv3</a>
Alexander Weigl's avatar
Alexander Weigl committed
155 156 157
    <a href="thirdparty.txt">Third Party Licenses</a> 
    <br>
    Executable with <code>java -jar psdbg-1.0-fm.jar</code>
Alexander Weigl's avatar
Alexander Weigl committed
158 159
 </li>
</ul>
Alexander Weigl's avatar
Alexander Weigl committed
160 161

<div style="clear: both;"/>
Sarah Grebing's avatar
Sarah Grebing committed
162