-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.html
239 lines (239 loc) · 17.6 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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<meta content="all" name="robots" />
<meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">
<meta name="description" content="Usability in Formal Verification and Aartifact">
<meta name="author" content="Andrei Lapets">
<title>Usability in Formal Verification and Aartifact</title>
<link rel="shortcut icon" type="image/x-icon" href="data:image/x-icon;base64,iVBORw0KGgo="><!-- Suppress browser favicon.ico request. -->
<link rel="stylesheet" href="https://fonts.googleapis.com/css2?family=Lato:wght@300;400&display=swap">
<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css"
integrity="sha384-BVYiiSIFeK1dGmJRAkycuHAHRg32OmUcww7on3RYdg4Va+PmSTsz/K68vbdEjh4u"
crossorigin="anonymous">
<style>
html, body { height:100%; margin:0; color:#555555; font-family:'Lato',Helvetica,sans-serif; font-weight:300; }
body { margin:20px 0px 20px 0px; padding-top:70px; }
.content { margin-bottom:60px; }
.content .anchor { display:block; height:50px; margin-top:-50px; visibility:hidden; }
.content h1 { font-weight:300; font-size:36px; cursor:default; }
.content .sub-title { margin:-8px 0px 22px 0px; font-family:'Lato',Helvetica,sans-serif; font-weight:300; font-size:24px; cursor:default; }
.content .lead-intro { font-family:'Lato',Helvetica,sans-serif; font-weight:300; font-size:16px; cursor:default; }
.content .lead-contact { margin-bottom:50px; font-family:'Lato',Helvetica,sans-serif; font-weight:300; font-size:16px; cursor:default; }
.content h2 { padding-bottom:2px; border-bottom:1px solid #CCCCCC; font-family:'Lato',Helvetica,sans-serif; font-weight:400; font-size:24px; color:#888888; }
.content h4 { display:inline-block; margin:20px 0px 0px 20px; border-bottom:1px solid #CCCCCC; }
.content p { text-align:justify; font-family:'Lato',Helvetica,sans-serif; font-weight:400; color:#000000; }
.content ul { margin:20px 20px 0px 20px; font-family:'Lato',Helvetica,sans-serif; font-weight:400; color:#000000; }
.content li { padding:10px 0px; }
.content table { width:100%; margin:10px 10px 0px 10px; border-spacing:5px; font-family:'Lato',Helvetica,sans-serif; font-weight:400; }
.content table td { min-width:160px; padding:2px 10px 10px 10px; }
.content table .td-end { width:100%; }
.content .text { margin:20px 0px 0px 0px; }
.content a { color:#4E759A; text-decoration:none; }
.navbar-nav>li>a { font-family:'Lato',Helvetica,sans-serif; font-weight:400; }
@media (max-width:992px) { /* Collapse navigation menu. */
.content { margin-bottom:30px; }
.content table .td-end { min-width:0px; }
.navbar-header { float:none; }
.navbar-left,.navbar-right { float:none !important; }
.navbar-toggle { display:block; }
.navbar-collapse { border-top:1px solid transparent; box-shadow:inset 0 1px 0 rgba(255,255,255,0.1); }
.navbar-fixed-top { top:0; border-width:0 0 1px; }
.navbar-collapse.collapse { display:none!important; }
.navbar-nav { float:none!important; margin-top:7.5px; }
.navbar-nav>li { float:none; }
.navbar-nav>li>a { padding-top:10px; padding-bottom:10px; }
.collapse.in{ display:block !important; }
}
@media (max-width:580px) {
.content table .td-end { display:none; }
}
@media (max-width:525px) {
.content h1 { font-size:26px; }
.content h4 { margin-left:10px; }
.content .lead-intro { font-size:14px; line-height:18px; }
.content .lead-contact { font-size:14px; line-height:18px; }
.content li { line-height:18px; }
.content table { font-size:12px; }
.content table td { min-width:0px; padding:2px 2px 2px 2px; }
.content table .td-end { width:0px; }
.content .text { line-height:18px; }
}
</style>
<script src="https://cdnjs.cloudflare.com/ajax/libs/jquery/3.3.1/jquery.min.js"
integrity="sha256-FgpCb/KJQlLNfOu91ta32o/NMZxltwRo8QtmkMRdAu8="
crossorigin="anonymous"></script>
<script async src="https://www.googletagmanager.com/gtag/js?id=UA-153492261-2"></script>
<script>
window.dataLayer = window.dataLayer || [];
function gtag(){dataLayer.push(arguments);}
gtag('js', new Date());
gtag('config', 'UA-153492261-2');
</script>
<script>
var favIcon = "AAABAAEAICAAAAEACACoCAAAFgAAACgAAAAgAAAAQAAAAAEACAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAQEBAAICAgADAwMABAQEAAUFBQAGBgYABwcHAAkJCQAKCgoACwsLAAwMDAAREREAEhISABMTEwAUFBQAFRUVABYWFgAXFxcAGxsbABwcHAAdHR0AHh4eACMjIwAkJCQAJSUlACcnJwAoKCgAKioqACwsLAAzMzMANTU1ADY2NgA4ODgAOjo6ADs7OwA+Pj4ASUlJAExMTABOTk4AT09PAFJSUgBVVVUAV1dXAFhYWABZWVkAWlpaAFtbWwBfX18AYGBgAGFhYQBoaGgAa2trAG1tbQBubm4Ab29vAHFxcQB1dXUAd3d3AH9/fwCAgIAAg4ODAIWFhQCHh4cAkJCQAJGRkQCXl5cAmJiYAJmZmQCkpKQAqampAKqqqgCrq6sArKysAK6urgC0tLQAuLi4AL29vQC+vr4AwMDAAMHBwQDCwsIAxMTEAMfHxwDIyMgAysrKAMzMzADNzc0Az8/PANHR0QDU1NQA29vbAN3d3QDf398A4uLiAOPj4wDl5eUA6+vrAO3t7QDu7u4A7+/vAPDw8ADx8fEA8vLyAPPz8wD09PQA9fX1APb29gD4+PgA+fn5APr6+gD7+/sA/Pz8AP7+/gD///8AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAcnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJpZGxycnJycnJyaGVycnJycnJycnJycnJycnJycnJPLg0EFjVacnJyVzENByZdcnJycnJycnJycnJycnJyOwMAL0A0DQZCck0MACQ/GB1jcnJycnJycnJycnJyckkAAD1ycnJgMwA5IAAFWHJfCjRycnJycnJycnJycnJkFQARZHJycnJyPQAAAAlccnI0BmFycnJycnJycnJyckgAACJxcnJycnJyOAAAA1FyckwASXJycnJycnJycnJyOgAAJHFycnJycnJmEAAAQHJyZwsycnJycnJycnJycnIzAAAfb3JycnJycnInAAAocnJyKw5rcnJycnJycnJycjMAABJmcnJycnJycj8AABBicnJbS3BycnJycnJycnJyNwAABFZycnJycnJyVQMAAE1ycnJycnJycnJycnJycnJBAAAAQ3JycnJycnJsFwAAP3JycnJycnJycnJycnJyclQCAAAucnJycnJycnIsAAApcnJycnJycnJycnJycnJybyEAAA9hcnJycnJyckAAABRqcnJycnJycnJycnJycnJyRQAAAEdycnJycnJyUgIAAU9ycnJycnJycnJycnJycnJrHAAAKnJycnJycnJmEwAAPHJycnJycnJycnJycnJycnJKAAAHU3JycnJycnItAAAlcnJycnJycnJycnJycnJycnI5AAAjbXJycnJybh4AABFkcnJycnJycnJycnJycnJycm8qAAA2cnJycnJHAAAAAlBycnJycnJycnJycnJycnJycm04AAAvXnJyTg8aGQAARnJycnJycnJycnJycnJycnJycnJIHwAIJCAAG1pZJy9gcnJycnJycnJycnJycnJycnJycnJuUD4vMERjcnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycnJycgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA";
var docHead = document.getElementsByTagName('head')[0];
var newLink = document.createElement('link');
newLink.rel = 'shortcut icon';
newLink.type = 'image/x-icon';
newLink.href = 'data:image/png;base64,'+favIcon;
docHead.appendChild(newLink);
$(document).on('click','.navbar-collapse.in',function(e) {
if($(e.target).is('a')) {
$(this).collapse('hide');
}
});
</script>
</head>
<body>
<nav class="navbar navbar-default navbar-fixed-top">
<div class="container">
<div class="navbar-header">
<button type="button" class="navbar-toggle collapsed" data-toggle="collapse" data-target="#navbar" aria-expanded="false" aria-controls="navbar">
<span class="sr-only">Toggle navigation</span>
<span class="icon-bar"></span>
<span class="icon-bar"></span>
<span class="icon-bar"></span>
</button>
<a class="navbar-brand" href="#">Usability in Formal Verification & Aartifact</a>
</div>
<div id="navbar" class="navbar-collapse collapse">
<ul class="nav navbar-nav navbar-right">
<li><a href="#software">Software</a></li>
<li><a href="#publications">Publications</a></li>
<li><a href="#acknowledgments">Acknowledgments</a></li>
<li><a href="https://github.com/aartifact">GitHub</a></li>
<li><a href="mailto:[email protected]">Contact</a></li>
</ul>
</div><!--/.nav-collapse -->
</div>
</nav>
<div class="container content">
<div class="row">
<div class="col-sm-12">
<h1 class="mt-5">Usability and Accessibility of Formal Modeling and Verification Software</h1>
<p class="sub-title">
Aartifact Lightweight Verification System and Related Frameworks
</p>
<p class="lead-intro">
From 2008 until 2013, this research effort undertaken at Boston University investigated, prototyped, and evaluated (within the classroom and for domain-specific use cases) features and techniques that could improve the usability and accessibility of formal modeling and verification software tools and services. It included the development of variants of a verification system called Aartifact, focusing on the use of heuristic algorithms, fact databases, interactive interfaces, and browser compatibility. Related and/or interoperable frameworks for visualization of mathematical concepts and mathematical content management and presentation were also developed as part of this work and peripheral efforts.
</p>
</div>
</div>
<span id="software" class="anchor"></span>
<div class="row">
<div class="col-sm-12">
<h2>Software Prototypes and Frameworks</h2>
<ul class="list-unstyled">
<li>
<b><a href="https://github.com/aartifact/aartifact-verifier">Aartifact Verification System</a>.</b>
<br/>A Haskell implementation of a formal verification system that can leverage a database of formal facts and an ensemble of heuristic symbolic search algorithms to verify mathematical proofs assembled in a human-legible style and level of detail.
</li>
<li>
<b><a href="https://github.com/aartifact/aartifact-light">Aartifact Light Web-Based Verifier</a>.</b>
<br/>A browser-compatible lightweight variant of the Aartifact Verification System implemented using JavaScript.
</li>
<li>
<b><a href="https://sheaf.io">Sheaf</a> and <a href="https://protoql.org">Protoql</a>.</b>
<br/>Early versions of the Sheaf framework for web-based presentation of mathematical content and the Protoql visualization library were developed as part of this effort. This included the integration of the Aartifact Light interactive proof environment directly into the assignment sections of course notes written and presented using Sheaf, as well as the embedding of Protoql interactive visualizations into the same Sheaf course notes.
</li>
</ul>
</div>
</div>
<span id="publications" class="anchor"></span>
<div class="row">
<div class="col-sm-12">
<h2>Publications and Reports</h2>
<ul class="list-unstyled">
<li>
<b><a href="https://lapets.io/pub/integdep.pdf">Towards Accessible Integration and Deployment of Formal Tools and Techniques</a>.</b>
[
<a href="https://www.computer.org/csdl/proceedings-article/topi/2013/06597189/12OmNBSSVez">web</a>,
<a href="https://lapets.io/pub/integdep.pdf">pdf</a>
]
<br/>Andrei Lapets, Richard Skowyra, Azer Bestavros, and Assaf Kfoury
<br/>Proceedings of <a href="https://www.computer.org/csdl/proceedings/topi/2013/12OmNxETa7R">TOPI 2013: The 3rd Workshop on Developing Tools as Plug-ins</a>.
San Francisco, CA, USA. May 2013.
</li>
<li>
<b><a href="https://www.cs.bu.edu/techreports/pdf/2012-015-env-classroom-math.pdf">Accessible Integrated Formal Reasoning Environments in Classroom Instruction of Mathematics</a>.</b>
[
<a href="https://cps-vo.org/node/3338">web</a>,
<a href="https://www.cs.bu.edu/techreports/pdf/2012-015-env-classroom-math.pdf">pdf</a>
]
<br/>Andrei Lapets
<br/>Proceedings of <a href="https://cps-vo.org/node/6777">HCSS 2012: The High Confidence Software and Systems Conference</a>.
Annapolis, MD, USA. May 2012.
</li>
<li>
<b><a href="https://www.cs.bu.edu/techreports/pdf/2010-011-aartifact-interface.pdf">A User-friendly Interface for a Lightweight Verification System</a>.</b>
[
<a href="https://dl.acm.org/doi/abs/10.1016/j.entcs.2012.06.004">web</a>,
<a href="https://www.cs.bu.edu/techreports/pdf/2010-011-aartifact-interface.pdf">pdf</a>
]
<br/>Andrei Lapets and Assaf Kfoury
<br/><a href="https://dl.acm.org/toc/entcs/2012/285/C"><i>Electronic Notes in Theoretical Computer Science</i>, <b>285</b>(C)</a>:29-41, 2012.
</li>
<li>
<b><a href="https://www.cs.bu.edu/techreports/pdf/2010-025-formal-sla-verification.pdf">Formal Verification of SLA Transformations</a>.</b>
[
<a href="https://ieeexplore.ieee.org/document/6012789">web</a>,
<a href="https://www.cs.bu.edu/techreports/pdf/2010-025-formal-sla-verification.pdf">pdf</a>
]
<br/>Vatche Ishakian, Andrei Lapets, Azer Bestavros, and Assaf Kfoury
<br/>Proceedings of <a href="http://www.wikicfp.com/cfp/servlet/event.showcfp?eventid=15158">CloudPerf 2011: IEEE International Workshop on Performance Aspects of Cloud and Service Virtualization</a>.
Washington, D.C., USA. July 2011.
</li>
<li>
<b><a href="https://www.cs.bu.edu/techreports/pdf/2010-010-aartifact-discussion.pdf">User-friendly Support for Common Concepts in a Lightweight Verifier</a>.</b>
[
<a href="https://easychair.org/publications/paper/6shl">web</a>,
<a href="https://easychair.org/publications/open/6shl">pdf</a>,
<a href="https://www.cs.bu.edu/techreports/pdf/2010-010-aartifact-discussion.pdf">report</a>
]
<br/>Andrei Lapets
<br/>Proceedings of <a href="http://www.floc-conference.org/VERIFY-home.html">VERIFY-2010: The 6th International Verification Workshop</a>.
Edinburgh, UK. July 2010.
</li>
<li>
<b><a href="https://www.cs.bu.edu/techreports/pdf/2010-012-aartifact-ontology.pdf">Ontology Support for a Lightweight Formal Verification System</a>.</b>
<br/>Andrei Lapets, Prakash Lalwani, and Assaf Kfoury
<br/>Technical Report BUCS-TR-2010-012, CS Dept., Boston University, May 2010.
</li>
<li>
<b><a href="https://www.cs.bu.edu/techreports/pdf/2009-032-classroom-verification-functional.pdf">Lightweight Formal Verification in Classroom Instruction of Reasoning about Functional Code</a>.</b>
<br/>Andrei Lapets
<br/>Technical Report BUCS-TR-2009-032, CS Dept., Boston University, November 2009.
</li>
</ul>
</div>
</div>
<span id="acknowledgments" class="anchor"></span>
<div class="row">
<div class="col-sm-12">
<h2>Acknowledgments</h2>
<div class="text">
<p>
This effort benefitted from the support and cooperation of <a href="https://www.bu.edu">Boston University</a>, including the <a href="https://www.bu.edu/cs/">Department of Computer Science</a>, the <a href="https://www.bu.edu/hic">Hariri Institute for Computing</a>.
</p>
<p>
This work was partially supported by the National Science Foundation under Grants
#<a href="https://www.nsf.gov/awardsearch/showAward?AWD_ID=0720604">0720604</a>,
#<a href="https://www.nsf.gov/awardsearch/showAward?AWD_ID=0735974">0735974</a>,
#<a href="https://www.nsf.gov/awardsearch/showAward?AWD_ID=0820138">0820138</a>,
#<a href="https://www.nsf.gov/awardsearch/showAward?AWD_ID=0952145">0952145</a>, and
#<a href="https://www.nsf.gov/awardsearch/showAward?AWD_ID=1012798">1012798</a>.
Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.
</p>
</div>
</div>
</div>
</div>
<script src="https://cdnjs.cloudflare.com/ajax/libs/jquery/3.2.1/jquery.min.js"></script>
<script src="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/js/bootstrap.min.js"
integrity="sha384-Tc5IQib027qvyjSMfHjOMaLkfuWVxZxUPnCJA7l2mCWNIpG9mGCD8wGNIcPD7Txa"
crossorigin="anonymous">
</script>
</body>
</html>