-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathindex.html
112 lines (111 loc) · 4.53 KB
/
index.html
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
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
<html version="-//W3C//DTD XHTML 1.1//EN"
xmlns="http://www.w3.org/1999/xhtml" xml:lang="en"
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xsi:schemaLocation="http://www.w3.org/1999/xhtml
http://www.w3.org/MarkUp/SCHEMA/xhtml11.xsd">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<meta name="viewport" content="initial-scale=1.0"/>
<title>ProVerB — SLEBoK</title>
<link href="main.css" rel="stylesheet" type="text/css" />
<script type="text/javascript">
var _gaq = _gaq || [];
_gaq.push(['_setAccount', 'UA-3743366-7']);
_gaq.push(['_setDomainName', 'github.io']);
_gaq.push(['_setAllowLinker', true]);
_gaq.push(['_trackPageview']);
(function() {
var ga = document.createElement('script'); ga.type = 'text/javascript'; ga.async = true;
ga.src = ('https:' == document.location.protocol ? 'https://ssl' : 'http://www') + '.google-analytics.com/ga.js';
var s = document.getElementsByTagName('script')[0]; s.parentNode.insertBefore(ga, s);
})();
</script>
</head>
<body>
<div class="left">
<div class="logo">
<a href="index.html"><img src="proverb.png" alt="ProVerB"/></a>
<h3>Program<br/>Verification<br/>Book</h3>
</div>
<nav>
<ul style="margin: 0;padding: 0;">
<li>
<a href="index.html">Homepage</a>
</li>
<li>
<a href="all.html">All tools</a>
</li>
<ul>
<li>
<a href="pv0.html" title="unprocessed/nonverifying">PV0</a>
</li><li>
<a href="pv1.html" title="solvers/linters">PV1</a>
</li><li>
<a href="pv2.html" title="synthesisers">PV2</a>
</li><li>
<a href="pv3.html" title="property checkers">PV3</a>
</li><li>
<a href="pv4.html" title="monoverifiers">PV4</a>
</li><li>
<a href="pv5.html" title="spec compilers">PV5</a>
</li><li>
<a href="pv6.html" title="proof assistants">PV6</a>
</li><li>
<a href="framework.html">Frameworks</a>
</li></ul>
<li>
<a href="tags.html">Tags</a>
</li><li>
<a href="specificationformat.html">Specification formats</a>
</li><li>
<a href="credits.html">About</a>
</li>
</ul>
</nav>
</div>
<div class="main">
<h1 class="fbs">ProVerB: Program Verification Book</h1>
<br clear="both"/>
<p><strong>ProVerB</strong> is a project aimed at explaining program verification tools to practicing software developers, and at helping them to find they way around the available tools, clearly and briefly summarising the main purpose of the tool, its current status, relations to other tools, etc. You can <a href="credits.html" class="nobold">read more about the project on the credits page</a> or <a href="https://github.com/Sophietje/Verification-Tool-Overview">visit the dataset repository</a>.</p>
<p>We classify all tools in this book as belonging to one of the six levels:</p>
<ul>
<li>
<a href="pv0.html">PV0</a>
<<PV_TEXT$0$>>
</li>
<li>
<a href="pv1.html">PV1</a>
<<PV_TEXT$1$>>
</li>
<li>
<a href="pv2.html">PV2</a>
<<PV_TEXT$2$>>
</li>
<li>
<a href="pv3.html">PV3</a>
<<PV_TEXT$3$>>
</li>
<li>
<a href="pv4.html">PV4</a>
<<PV_TEXT$4$>>
</li>
<li>
<a href="pv5.html">PV5</a>
<<PV_TEXT$5$>>
</li>
<li>
<a href="pv6.html">PV6</a>
<<PV_TEXT$6$>>
</li>
</ul>
<p class="red"><strong>NB</strong>: this project is a work in progress, and thus may momentarily contain imperfect or erroneous data! Use at your own risk or <a href="mailto:s.a.m.lathouwers@utwente.nl,v.zaytsev@utwente.nl">get in touch</a>!</p>
<p>The PV-hierarchy does not represent how “worthy” or “important” a tool is, merely how much it expects and demands of its end user, and what it can offer back. In many cases having a lower-PV-level tool is more preferable because it is easier in use and is less ambitious about the effort investment. Often tools of a lower PV-level are built “on top” of tools of higher level which they run as a backend.</p>
<br/><hr/>
<div class="f">
Last updated: <strong>December 2022</strong>.
</div>
</div>
</body>
</html>