-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.html
executable file
·357 lines (314 loc) · 20.4 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
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
<!DOCTYPE html>
<!--[if lt IE 7]> <html lang="en" class="no-js lt-ie9 lt-ie8 lt-ie7"> <![endif]-->
<!--[if IE 7]> <html lang="en" class="no-js lt-ie9 lt-ie8"> <![endif]-->
<!--[if IE 8]> <html lang="en" class="no-js lt-ie9"> <![endif]-->
<!--[if gt IE 8]><!--> <html lang="en" class="no-js"> <!--<![endif]-->
<head>
<!-- meta character set -->
<meta charset="utf-8">
<!-- Always force latest IE rendering engine or request Chrome Frame -->
<meta http-equiv="X-UA-Compatible" content="IE=edge,chrome=1">
<title>SMACK Software Verifier and Verification Toolchain</title>
<!-- Meta Description -->
<meta name="description" content="Blue One Page Creative HTML5 Template">
<meta name="keywords" content="one page, single page, onepage, responsive, parallax, creative, business, html5, css3, css3 animation">
<meta name="author" content="Jonathan Whitaker">
<!-- Mobile Specific Meta -->
<meta name="viewport" content="width=device-width, initial-scale=1">
<!-- CSS
================================================== -->
<link href='http://fonts.googleapis.com/css?family=Open+Sans:400,300,700' rel='stylesheet' type='text/css'>
<!-- Fontawesome Icon font -->
<link rel="stylesheet" href="css/font-awesome.min.css">
<!-- bootstrap.min -->
<link rel="stylesheet" href="css/jquery.fancybox.css">
<!-- bootstrap.min -->
<link rel="stylesheet" href="css/bootstrap.min.css">
<!-- bootstrap.min -->
<link rel="stylesheet" href="css/owl.carousel.css">
<!-- bootstrap.min -->
<link rel="stylesheet" href="css/slit-slider.css">
<!-- bootstrap.min -->
<link rel="stylesheet" href="css/animate.css">
<!-- Main Stylesheet -->
<link rel="stylesheet" href="css/main.css">
<!-- Modernizer Script for old Browsers -->
<script src="js/modernizr-2.6.2.min.js"></script>
</head>
<body id="body">
<!-- preloader -->
<div id="preloader">
<div class="loder-box">
<div class="battery"></div>
</div>
</div>
<!-- end preloader -->
<!--
Fixed Navigation
==================================== -->
<header id="navigation" class="navbar-inverse navbar-fixed-top animated-header">
<div class="container">
<div class="navbar-header">
<!-- responsive nav button -->
<button type="button" class="navbar-toggle" data-toggle="collapse" data-target=".navbar-collapse">
<span class="sr-only">Toggle navigation</span>
<span class="icon-bar"></span>
<span class="icon-bar"></span>
<span class="icon-bar"></span>
</button>
<!-- /responsive nav button -->
<!-- logo -->
<h1 class="navbar-brand">
<a href="#body" style="color: #fff">SMACK</a>
</h1>
<!-- /logo -->
</div>
<!-- main nav -->
<nav class="collapse navbar-collapse navbar-right" role="navigation">
<ul id="nav" class="nav navbar-nav">
<li><a href="#body">Home</a></li>
<li><a href="#about">About</a></li>
<li><a href="#publications">Publications</a></li>
<li><a href="#people">People</a></li>
<li><a target="_blank" href="https://github.com/smackers/smack" class="external">GitHub</a></li>
</ul>
</nav>
<!-- /main nav -->
</div>
</header>
<!--
End Fixed Navigation
==================================== -->
<main class="site-content" role="main">
<!--
Home Slider
==================================== -->
<section id="home-slider">
<div class="slide-caption">
<div class="caption-content">
<img src="img/smack_logo.png" alt="SMACK">
<span class="animated fadeInDown">Software Verifier & Verification Toolchain</span>
<a target="_blank" href="https://github.com/smackers/smack" class="btn btn-color btn-effect">GitHub</a>
</div>
</div>
</section>
<!-- Service section -->
<section id="about">
<div class="container">
<div class="row">
<div class="sec-title text-center">
<h2 class="wow animated bounceInLeft">About</h2>
</div>
<div>
<p>
SMACK is both a modular software verification toolchain and a
self-contained software verifier. It can be used to verify the assertions
in its input programs. In its default mode, assertions are verified up to a
given bound on loop iterations and recursion depth; it contains experimental
support for unbounded verification as well.
Under the hood, SMACK is a translator from the LLVM
compiler's popular intermediate representation (IR) into the
Boogie intermediate verification language (IVL).
Sourcing LLVM IR exploits an increasing number of compiler front-ends,
optimizations, and analyses.
Targeting Boogie exploits a canonical
platform which simplifies the implementation of algorithms for verification,
model checking, and abstract interpretation.
</p>
</div>
</div>
</div>
</section>
<!-- end Service section -->
<!-- Publications section -->
<section id="publications">
<div class="container">
<div class="row">
<div class="sec-title text-center">
<h2 class="wow animated bounceInLeft">Publications</h2>
</div>
<div class="">
<ul class="list-group">
<li class="list-group-item"><a href="https://dl.acm.org/citation.cfm?id=3240485">CANAL: A Cache Timing Analysis Framework via LLVM Transformation</a>, Chungha Sung, Brandon Paulsen, Chao Wang, 33rd ACM/IEEE International Conference on Automated Software Engineering (ASE 2018)</li>
<li class="list-group-item"><a href="https://dl.acm.org/citation.cfm?id=3196055">Formal Security Verification of Concurrent Firmware in SoCs using Instruction-Level Abstraction for Hardware</a>, Bo-Yuan Huang, Sayak Ray, Aarti Gupta, Jason M. Fung, Sharad Malik, 55th Annual Design Automation Conference (DAC 2018)</li>
<li class="list-group-item"><a href="https://dl.acm.org/citation.cfm?id=3180259">Reducer-Based Construction of Conditional Verifiers</a>, Dirk Beyer, Marie-Christine Jakobs, Thomas Lemberger, Heike Wehrheim, 40th International Conference on Software Engineering (ICSE 2018)</li>
<li class="list-group-item"><a href="https://www.ndss-symposium.org/wp-content/uploads/2018/02/ndss2018_09-1_Kalra_paper.pdf">ZEUS: Analyzing Safety of Smart Contracts</a>, Sukrit Kalra, Seep Goel, Mohan Dhawan, Subodh Sharma, 25th Annual Network and Distributed System Security Symposium (NDSS 2018)</li>
<li class="list-group-item"><a href="https://link.springer.com/chapter/10.1007/978-3-319-72344-0_3">Formal Verification of Optimizing Compilers</a>, Yiji Zhang, Lenore D. Zuck, Keynote at the 14th International Conference on Distributed Computing and Internet Technology (ICDCIT 2018)</li>
<li class="list-group-item"><a href="https://soarlab.org/publications/2017_aplas_hr">Counterexample-Guided Bit-Precision Selection</a>, Shaobo He, Zvonimir Rakamaric, 15th Asian Symposium on Programming Languages and Systems (APLAS 2017)</li>
<li class="list-group-item"><a href="https://cseweb.ucsd.edu/~dstefan/pubs/cauligi:2017:fact.pdf">FaCT: A Flexible, Constant-Time Programming Language</a>, Sunjay Cauligi, Gary Soeller, Fraser Brown, Brian Johannesmeyer, Yunlu Huang, Ranjit Jhala, Deian Stefan, IEEE Secure Development Conference (SecDev 2017)</li>
<li class="list-group-item"><a href="https://soarlab.org/publications/2017_tapas_hllr">Static Assertion Checking of Production Software with Angelic Verification</a>, Shaobo He, Shuvendu Lahiri, Akash Lal, Zvonimir Rakamaric, 8th Workshop on Tools for Automatic Program Analysis (TAPAS 2017)</li>
<li class="list-group-item"><a href="https://www.microsoft.com/en-us/research/publication/refining-interprocedural-change-impact-analysis-using-equivalence-relations">Refining Interprocedural Change-Impact Analysis using Equivalence Relations</a>, Alex Gyori, Shuvendu Lahiri, Nimrod Partush, 26th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2017)</li>
<li class="list-group-item"><a href="https://soarlab.org/publications/2017_hotos_bbbprr">System Programming in Rust: Beyond Safety</a>, Abhiram Balasubramanian, Marek S. Baranowski, Anton Burtsev, Aurojit Panda, Zvonimir Rakamaric, Leonid Ryzhyk, 16th Workshop on Hot Topics in Operating Systems (HotOS 2017)</li>
<li class="list-group-item"><a href="https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/almeida">Verifying Constant-Time Implementations</a>, Jose Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Francois Dupressoir, Michael Emmi, 25th USENIX Security Symposium (2016)</li>
<li class="list-group-item"><a href="http://dl.acm.org/citation.cfm?id=2908126">Statistical Similarity of Binaries</a>, Yaniv David, Nimrod Partush, Eran Yahav, 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2016)</li>
<li class="list-group-item"><a href="https://soarlab.org/publications/2016_icse_chwre">SMACK Software Verification Toolchain</a>, Montgomery Carter, Shaobo He, Jonathan Whitaker, Zvonimir Rakamaric, Michael Emmi, Demonstrations Track at the 38th IEEE/ACM International Conference on Software Engineering (ICSE 2016)</li>
<li class="list-group-item"><a href="https://soarlab.org/publications/2015_ase_ddr">Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers</a>, Pantazis Deligiannis, Alastair F. Donaldson, Zvonimir Rakamaric, 30th IEEE/ACM International Conference on Automated Software Engineering (ASE 2015)</li>
<li class="list-group-item"><a href="https://soarlab.org/publications/2015_tacas_hcelqr">SMACK+Corral: A Modular Verifier (Competition Contribution)</a>, Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer, Zvonimir Rakamaric, 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015)</li>
<li class="list-group-item"><a href="http://madhu.cs.illinois.edu/CAV14ice.pdf">ICE: A Robust Framework for Learning Invariants</a>, Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider, 26th International Conference on Computer Aided Verification (CAV 2014)</li>
<li class="list-group-item"><a href="https://soarlab.org/publications/2014_cav_re">SMACK: Decoupling Source Language Details from Verifier Implementations</a>, Zvonimir Rakamaric, Michael Emmi, 26th International Conference on Computer Aided Verification (CAV 2014) <b>[MAIN REFERENCE]</b></li>
<li class="list-group-item"><a href="https://soarlab.org/publications/2011_thesis_rakamaric">Modular Verification of Shared-Memory Concurrent System Software</a>, Zvonimir Rakamaric, Ph.D. Thesis, Department of Computer Science, University of British Columbia, 2011</li>
<li class="list-group-item"><a href="https://soarlab.org/publications/2009_vmcai_rh">A Scalable Memory Model for Low-Level Code</a>, Zvonimir Rakamaric, Alan J. Hu, 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2009)</li>
<li class="list-group-item"><a href="https://soarlab.org/publications/2008_ase_rh">Automatic Inference of Frame Axioms Using Static Analysis</a>, Zvonimir Rakamaric, Alan J. Hu, 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008)</li>
</ul>
</div>
</div>
</div>
</section>
<!-- end Publications section -->
<!-- Persons section -->
<section id="people">
<div class="">
<div class="container">
<div class="row">
<div class="sec-title text-center">
<h2 class="">People</h2>
</div>
<div class="sec-subtitle text-center">
<h2 class="">Coordinators</h2>
</div>
<div class="row text-center">
<div class="col-md-6">
<div class="people-item text-center">
<a href="http://michael-emmi.github.io/"><img src="img/people/emmi.jpg" alt="Michael Emmi"></a>
<div>
<span>Michael Emmi</span>
</div>
</div>
</div>
<div class="col-md-6">
<div class="people-item text-center">
<a href="http://www.zvonimir.info/"><img src="img/people/zvonimir.jpg" alt="Zvonimir Rakamaric"></a>
<div>
<span>Zvonimir Rakamaric</span>
</div>
</div>
</div>
</div>
<div class="sec-subtitle text-center">
<h2 class="">Contributors</h2>
</div>
<div class="row">
<div class="col-md-4">
<div class="people-item text-center">
<a href="http://www.linkedin.com/pub/montgomery-carter/12/a89/512"><img src="img/people/carter.jpg" alt="Montgomery Carter"></a>
<div class="clearfix">
<span>Montgomery Carter</span>
</div>
</div>
</div>
<div class="col-md-4">
<div class="people-item text-center">
<a href="http://pdeligia.github.io/"><img src="img/people/deligiannis.jpg" alt="Pantazis Deligiannis"></a>
<div class="clearfix">
<span>Pantazis Deligiannis</span>
</div>
</div>
</div>
<div class="col-md-4">
<div class="people-item text-center">
<a href="http://www.cs.utah.edu/~haran"><img src="img/people/haran.jpg" alt="Arvind Haran"></a>
<div class="clearfix">
<span>Arvind Haran</span>
</div>
</div>
</div>
</div>
<div class="row">
<div class="col-md-4">
<div class="people-item text-center">
<a href="http://www.cs.utah.edu/~shaobo/"><img src="img/people/shaobo.jpg" alt="Shaobo He"></a>
<div class="clearfix">
<span>Shaobo He</span>
</div>
</div>
</div>
<div class="col-md-4">
<div class="people-item text-center">
<a href="http://jiten-thakkar.com/"><img src="img/people/thakkar.jpg" alt="Jiten Thakkar"></a>
<div class="clearfix">
<span>Jiten Thakkar</span>
</div>
</div>
</div>
<div class="col-md-4">
<div class="people-item text-center">
<a href="https://www.linkedin.com/in/jonathan-whitaker-5a8b2484"><img src="img/people/whitaker.jpg" alt="Jonathan Whitaker"></a>
<div class="clearfix">
<span>Jonathan Whitaker</span>
</div>
</div>
</div>
</div>
<div class="row">
<div class="col-md-4">
<div class="people-item text-center">
<a href="https://github.com/keram88"><img src="img/people/empty.jpg" alt="Marek Baranowski"></a>
<div class="clearfix">
<span>Marek Baranowski</span>
</div>
</div>
</div>
<div class="col-md-4">
<div class="people-item text-center">
<a href="https://www.linkedin.com/in/jack-j-garzella-7140a716"><img src="img/people/empty.jpg" alt="Jack J. Garzella"></a>
<div class="clearfix">
<span>Jack J. Garzella</span>
</div>
</div>
</div>
<div class="col-md-4">
<div class="people-item text-center">
<a href="https://github.com/liammachado"><img src="img/people/empty.jpg" alt="Liam Machado"></a>
<div class="clearfix">
<span>Liam Machado</span>
</div>
</div>
</div>
</div>
<div class="row">
<div class="col-md-4">
<div class="people-item text-center">
<a href="https://www.linkedin.com/in/dietrich-geisler-999204133"><img src="img/people/geisler.jpg" alt="Dietrich Geisler"></a>
<div class="clearfix">
<span>Dietrich Geisler</span>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</section>
<!-- end Persons section -->
</main>
<footer id="footer">
<div class="container">
<div class="row text-center">
<div class="footer-content">
</div>
</div>
</div>
</footer>
<!-- Essential jQuery Plugins
================================================== -->
<!-- Main jQuery -->
<script src="js/jquery-1.11.1.min.js"></script>
<!-- Twitter Bootstrap -->
<script src="js/bootstrap.min.js"></script>
<!-- Single Page Nav -->
<script src="js/jquery.singlePageNav.min.js"></script>
<!-- jquery.fancybox.pack -->
<script src="js/jquery.fancybox.pack.js"></script>
<!-- Owl Carousel -->
<script src="js/owl.carousel.min.js"></script>
<!-- jquery easing -->
<script src="js/jquery.easing.min.js"></script>
<!-- Fullscreen slider -->
<script src="js/jquery.slitslider.js"></script>
<script src="js/jquery.ba-cond.min.js"></script>
<!-- onscroll animation -->
<script src="js/wow.min.js"></script>
<!-- Custom Functions -->
<script src="js/main.js"></script>
</body>
</html>