index.md 2.64 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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
<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.
The language particualrily allows to:
<ol>
    <li></li>
    <li></li>
    <li></li>
    <li></li>

</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.
</p>
<h2>Features</h2>

<div class="column">
    <div >
        <img src="https://placeimg.com/150/150/any" />
        <h3>Feature 1</h3>
        <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>
<div style="clear: both;"/>
    <div class="column">
        <div >
            <img src="https://placeimg.com/150/150/any" />
            <h3>Feature 1</h3>
            <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>
    <div style="clear: both;"/>


        <!--    <h2>Getting Started</h2>


            <h2>Downloads</h2>

            <ul>
            <li>Version 1.0
            <p>
            <a href="#">psdb-0.9-alpha.jar</a>
            </p>
            </li>
            </ul>
        -->
        <footer style="border-top: #ccc 1px solid">
            Contact: <a href="https://formal.iti.kit.edu/~grebing/">Sarah Grebing</a>
        </footer>
        </p>