index.md 3.43 KB
Newer Older
Alexander Weigl's avatar
Alexander Weigl committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
<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%;
            text-align: center;
        }

        .column img {
            width: 150px;
            text-align: center;
        }
</style>

<h1>Proof Script Debugger for the KeY System</h1>

<p>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
<a href="http://www.key-project.org">KeY</a>. KeY is an interactive program verification
system for Java program annotated with the Java Modeling Language (JML).
</p>

<p>
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
38
The main features of the language are:
Alexander Weigl's avatar
Alexander Weigl committed
39
<ol>
Sarah Grebing's avatar
Sarah Grebing committed
40
41
42
43
44
45
46
47
48
49
50
51
<li> integration of domain specific entities like goal, formula, term and rule as
first-class citizens into the language;</li>
<li> an expressive proof goal selection mechanism
<ul>
    <li>to identify and select individual proof branches,</li>
    <li>to easily switch between proof branches,</li>
    <li>to select multiple branches for uniform treatment (multi-matching);</li>
</ul>
that is resilient to small changes in the proof</li>
<li> a repetition construct which allows repeated application of proof strategies;</li>
<li> support for proof exploration within the language.</li>

Alexander Weigl's avatar
Alexander Weigl committed
52
53
54
55
56

</ol>
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
57

Alexander Weigl's avatar
Alexander Weigl committed
58
</p>
Sarah Grebing's avatar
Sarah Grebing committed
59
60
61
<h2>Publications</h2>
A full description of the language and debugging-concept is published at <a href="">HVC 2017</a>.

Alexander Weigl's avatar
Alexander Weigl committed
62
63
64
65
<h2>Features</h2>

<div class="column">
    <div >
66
67
68
<!--<img src="https://placeimg.com/150/150/any" />-->
        <h3>Stepping back and forth in Proof Script</h3>
        <p> 
Alexander Weigl's avatar
Alexander Weigl committed
69
70
71
72
        </p>
    </div>

    <div >
73
74
      <!--  <img src="https://placeimg.com/150/150/any" /> -->
        <h3>Different views onto one proof state</h3>
Alexander Weigl's avatar
Alexander Weigl committed
75
76
77
    </div>

    <div >
78
79
       <!-- <img src="https://placeimg.com/150/150/any" />--<
        <h3>Run To Breakpoints in Script-Evaluation</h3>
Alexander Weigl's avatar
Alexander Weigl committed
80
81
82
83
84
85
86
    </div>

</div>
<div style="clear: both;"/>
    <div class="column">
        <div >
            <img src="https://placeimg.com/150/150/any" />
87
            <h3>Inspect proof State</h3>
Alexander Weigl's avatar
Alexander Weigl committed
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
            <p>

            </p>
        </div>

        <div >
            <img src="https://placeimg.com/150/150/any" />
            <h3>Feature 2</h3>
        </div>

        <div >
            <img src="https://placeimg.com/150/150/any" />
            <h3>Feature 3</h3>
        </div>

    </div>
104
    <div style="clear: both;"/> 
Alexander Weigl's avatar
Alexander Weigl committed
105
106


107
108
 
        
Alexander Weigl's avatar
Alexander Weigl committed
109
110
111
112
        <footer style="border-top: #ccc 1px solid">
            Contact: <a href="https://formal.iti.kit.edu/~grebing/">Sarah Grebing</a>
        </footer>
        </p>
113
114
115
116
117
118
119
120
121
122
123
124
125
<!--  <h2>Getting Started</h2>
    
    
                <h2>Downloads</h2>
    
                <ul>
                <li>Version 1.0
                <p>
                <a href="#">psdb-0.9-alpha.jar</a>
                </p>
                </li>
                </ul>
       -->