index.md 4.25 KB
Newer Older
Alexander Weigl's avatar
Alexander Weigl committed
1
2
3
4
5
6
7
8
9
10
11
12
13
<style>
        #content {
            width: 60em;
            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%;
Sarah Grebing's avatar
Sarah Grebing committed
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
27
            border-radius:150px;
        }
Alexander Weigl's avatar
Alexander Weigl committed
28
29
30
31
32
33
34
35
36
37
38
       
       .column h3 {
       
       }
       
       div.feature-caption {
            text-align: block;           
           text-align: justify;
           font-size: 80%;
       }
       
Alexander Weigl's avatar
Alexander Weigl committed
39
40
</style>

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

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

Alexander Weigl's avatar
Alexander Weigl committed
50

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

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

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

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

Sarah Grebing's avatar
Sarah Grebing committed
75

Alexander Weigl's avatar
Alexander Weigl committed
76
## Features
Alexander Weigl's avatar
Alexander Weigl committed
77
78

<div class="column">
Alexander Weigl's avatar
Alexander Weigl committed
79
    <div>
Sarah Grebing's avatar
Sarah Grebing committed
80
        <h3>Inspection of different parts of the proof state</h3>
81
        <p> 
Sarah Grebing's avatar
Sarah Grebing committed
82
83
        The different parts of the proof state can be inspected:
        <ul>
Alexander Weigl's avatar
Alexander Weigl committed
84
85
86
87
        <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>
Sarah Grebing's avatar
Sarah Grebing committed
88
        </p> 
Alexander Weigl's avatar
Alexander Weigl committed
89
90
    </div>
    <div >
Sarah Grebing's avatar
Sarah Grebing committed
91
        <h3>Adjustable view on list of open goals</h3>
Alexander Weigl's avatar
Alexander Weigl committed
92
        <img class="thumb" src="img/thumb_ScreenshotGoalList.png" />
Alexander Weigl's avatar
Alexander Weigl committed
93
        <div class="feature-caption"/></div>
Alexander Weigl's avatar
Alexander Weigl committed
94
95
    </div>
    <div >
Sarah Grebing's avatar
Sarah Grebing committed
96
        <h3>Explore the proof tree of KeY</h3>
Alexander Weigl's avatar
Alexander Weigl committed
97
98
        <img class="thumb" src="img/thumb_ScreenshotProofTree.png"/>
        <div class="feature-caption"/></div>
Alexander Weigl's avatar
Alexander Weigl committed
99
100
101
    </div>
</div>
<div style="clear: both;"/>
Alexander Weigl's avatar
Alexander Weigl committed
102
103
104
105
106
107
108

<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
109
        </div>
Alexander Weigl's avatar
Alexander Weigl committed
110
111
112
113
114
115
116
117
    </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
118
119
        </div>
    </div>
Alexander Weigl's avatar
Alexander Weigl committed
120
121
122
123
124
125
126
    <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
127
128
129
130
</div>

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

Alexander Weigl's avatar
Alexander Weigl committed
131
<h2>Getting Started</h2>
Alexander Weigl's avatar
Alexander Weigl committed
132

Alexander Weigl's avatar
Alexander Weigl committed
133
<h2>Downloads</h2>
Alexander Weigl's avatar
Alexander Weigl committed
134

Alexander Weigl's avatar
Alexander Weigl committed
135
136
137
138
139
140
141
<ul>
 <li>PSDBG - <strong>Version 1.0-FM</strong> 
    <a href="~/releases/psdbg-1.0-fm.jar">psdbg-1.0-fm.jar</a>
    <br>
    Special Version for the tool paper at Formal Methods 2018. 
 </li>
</ul>
Alexander Weigl's avatar
Alexander Weigl committed
142
143

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