index.md 3.93 KB
Newer Older
Alexander Weigl's avatar
Alexander Weigl committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
<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;
            width: 33%;
Sarah Grebing's avatar
Sarah Grebing committed
15
            text-align: left;
Alexander Weigl's avatar
Alexander Weigl committed
16
17
18
19
20
21
        }

        .column img {
            width: 150px;
            text-align: center;
        }
Alexander Weigl's avatar
Alexander Weigl committed
22
23
24
25
26
27
        
        img.thumb {
            width:300px; 
            height:300px;
            border-radius:150px;
        }
Alexander Weigl's avatar
Alexander Weigl committed
28
29
</style>

Alexander Weigl's avatar
Alexander Weigl committed
30
# Proof Script Debugger for the KeY System
Alexander Weigl's avatar
Alexander Weigl committed
31

Alexander Weigl's avatar
Alexander Weigl committed
32
The proof script debugger is a prototypical implementation
Alexander Weigl's avatar
Alexander Weigl committed
33
34
35
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
Alexander Weigl's avatar
Alexander Weigl committed
36
[KeY](http://www.key-project.org. KeY is an interactive program verification
Alexander Weigl's avatar
Alexander Weigl committed
37
38
system for Java program annotated with the Java Modeling Language (JML).

Alexander Weigl's avatar
Alexander Weigl committed
39

Alexander Weigl's avatar
Alexander Weigl committed
40
41
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
42
The main features of the language are:
Alexander Weigl's avatar
Alexander Weigl committed
43
44

1. integration of domain specific entities like goal, formula, term and rule as
Sarah Grebing's avatar
Sarah Grebing committed
45
first-class citizens into the language;</li>
Alexander Weigl's avatar
Alexander Weigl committed
46
47
48
49
50
51
52
53
54
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
55
56
57
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
58

Alexander Weigl's avatar
Alexander Weigl committed
59
60
61
62
63
## Publications

A full description of the language and debugging-concept 
is published at [HVC 2017](hvc2017.pdf)

Sarah Grebing's avatar
Sarah Grebing committed
64

Alexander Weigl's avatar
Alexander Weigl committed
65
## Features
Alexander Weigl's avatar
Alexander Weigl committed
66
67

<div class="column">
Alexander Weigl's avatar
Alexander Weigl committed
68
    <div>
Sarah Grebing's avatar
Sarah Grebing committed
69
        <h3>Inspection of different parts of the proof state</h3>
70
        <p> 
Sarah Grebing's avatar
Sarah Grebing committed
71
72
73
74
75
76
77
        The different parts of the proof state can be inspected:
        <ul>
         <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>
        </p> 
Alexander Weigl's avatar
Alexander Weigl committed
78
79
    </div>
    <div >
Sarah Grebing's avatar
Sarah Grebing committed
80
        <h3>Adjustable view on list of open goals</h3>
Alexander Weigl's avatar
Alexander Weigl committed
81
        <img class="thumb" src="img/thumb_ScreenshotGoalList.png" />
Alexander Weigl's avatar
Alexander Weigl committed
82
83
    </div>
    <div >
Sarah Grebing's avatar
Sarah Grebing committed
84
        <h3>Explore the proof tree of KeY</h3>
Alexander Weigl's avatar
Alexander Weigl committed
85
         <img class="thumb" src="img/thumb_ScreenshotProofTree.png"/>
Alexander Weigl's avatar
Alexander Weigl committed
86
87
88
89
90
    </div>
</div>
<div style="clear: both;"/>
    <div class="column">
        <div >
Sarah Grebing's avatar
Sarah Grebing committed
91
            <h3>Set a breakpoint and run execution to breakpoint</h3>
Alexander Weigl's avatar
Alexander Weigl committed
92
93
94
95
            <img src="img/thumb_ScreenshotBreakpoint.png" class="thumb"/>
            <div class="feature-caption">
                Mark lines with an (conditional) breakpoint to pause the script execution.
            </div
Alexander Weigl's avatar
Alexander Weigl committed
96
        </div>
Alexander Weigl's avatar
Alexander Weigl committed
97
98
99
100
101
102
103
104
        <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!
            </div>
Alexander Weigl's avatar
Alexander Weigl committed
105
        </div>
Alexander Weigl's avatar
Alexander Weigl committed
106
        <div> 
Sarah Grebing's avatar
website    
Sarah Grebing committed
107
        <h3> Interactive Rule Application</h3>
Alexander Weigl's avatar
Alexander Weigl committed
108
109
110
111
            <img src="img/thumb_ScreenshotInteractive.png" class="thumb" />
            <div class="feature-caption">
            Select rules for interactive application.
            </div>
Alexander Weigl's avatar
Alexander Weigl committed
112
    </div>
Alexander Weigl's avatar
Alexander Weigl committed
113
114
115
</div>

<div style="clear: both;"/> 
Sarah Grebing's avatar
website    
Sarah Grebing committed
116
    
Alexander Weigl's avatar
Alexander Weigl committed
117
118
119
120
121
122
123
124
125
    

## Downloads

* PSDBG - **Version 1.0-FM** [JAR](~/releases/psdbg-1.0-fm.jar)
    Special Version for Formal Methods


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