-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathindex.html
253 lines (207 loc) · 11.3 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
---
sidebar:
nav: "homenav"
---
<html>
<head>
<link rel="apple-touch-icon" sizes="180x180" href="favicon/apple-touch-icon.png">
<link rel="icon" type="image/png" sizes="32x32" href="favicon/favicon-32x32.png">
<link rel="icon" type="image/png" sizes="16x16" href="favicon/favicon-16x16.png">
<link rel="manifest" href="/site.webmanifest">
<title>Project Yin-Yang</title>
</head>
<body onload="load()" style="font-size: 20px;">
<!-- <link type="text/css" rel="stylesheet" href="style.css"> -->
<!-- <font face="ariel,helvetica"> -->
<br><br>
<center><img class="" src="/img/tool_logo.png" alt="" width="230pt"/></center>
<br><br>
<center><h1 id="introduction">Introduction</h1></center>
Satisfiability Modulo Theory (SMT) solvers are foundational tools for
many subareas of computer science, including formal verification,
programming languages, and software engineering. Their reliability and
robustness are crucial, especially for the safety-critical
domains. However, effectively validating SMT solvers has been a
longstanding challenge. The goal of Project Yin-Yang is to develop
novel, effective, practical methods and techniques to help make SMT
solvers more reliable, powerful, and usable.
<!-- To this end, we have introduced two novel, highly effective techniques
for stress-testing SMT solvers: <i>semantic fusion</i> [1]
and <i>type-aware operator mutation</i> [2]. The key idea behind
semantic fusion is to systematically combine two existing
equisatisfiable (i.e., both satisfiable or unsatisfiable) formulas
into a new formula that, by construction, preserves
satisfiability. Type-aware operator mutation is a simple, general,
unusually effective approach for differentially testing SMT solvers by
generating diverse type-correct formulas. -->
Our tools have demonstrated their remarkable effectiveness by
having already found 1,500+ bugs in Z3 and CVC4/5, the two
state-of-the-art SMT solvers.
<br><br>
<center><h1 id="results">Results</h1></center>
We have maintained our continuous, extensive effort in stress-testing
Z3 and CVC4/5 to benefit the SMT solver developer, user, and research
communities:
<br><br>
<center><div style="font-size: 23px;"><b>Yin-Yang project has found <b><span id="totalnum"> </span></b> (total) / <b><span id='fixednum'> </span></b> (fixed) bugs.</b></div></center>
<br>
<p>[Z3 bugs: <b>1199</b> (total) / <b>889</b> (fixed)]<br>
[CVC4/5 bugs: <b>465</b> (total) / <b>354</b> (fixed)]<br>
<p>[Bugs in default mode (Z3): <b>709</b> (total) / <b>532</b> (fixed)]<br>
[Bugs in default mode (CVC4/5): <b>243</b> (total) / <b>182</b> (fixed)]<br>
<p>[Soundness bugs (Z3): <b>386</b> (total) / <b>256</b> (fixed)]<br>
[Soundness bugs (CVC4/5): <b>77</b> (total) / <b>68</b> (fixed)]<br>
<p>[Incompleteness bugs (Z3): <b>13</b> (total) / <b>8</b> (fixed)]<br>
[Incompleteness bugs (CVC4/5): <b>18</b> (total) / <b>11</b> (fixed)]<br>
</p>
Semantic Fusion (<a href="yinyang_bugs.html">report links</a>) <br>
Type-aware Operator Mutation (<a href="opfuzz_bugs.html">report links</a>) <br>
Generative Type-aware Mutation (<a href="typefuzz_bugs.html">report links</a>) <br>
Weakening and Strengthening (<a href="janus.html">report links</a>)
</p>
Please follow us on
Twitter <img class="" src="/img/2021 Twitter logo - blue.png" alt="" width="20pt"/> <a href="https://twitter.com/testsmtsolvers">@testsmtsolvers</a> for
important project developments and regular tweets about interesting
bugs in Z3 and CVC4.
<br><br>
<center><h1 id="publications">Tools & Publications</h1></center>
<h3>Tools</h3>
<div class="notice--primary">
<img class="" src="/img/GitHub-Mark-64px.png" alt="" width="20pt"/> <b>yinyang</b>: <a href="https://github.com/testsmt/yinyang">https://github.com/testsmt/yinyang</a>
</div>
<div style="width: 60%; display: inline-block;">
<iframe width="1280" height="720" src="https://www.youtube.com/embed/JFu8cJYbxBI?start=5" title="17 June 1420 Validating SMT Solvers via Semantic Fusion" frameborder="0" allow="accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture" allowfullscreen></iframe></div>
<h3>Publications</h3>
<div class="notice--primary">
<!--<a href="https://testsmt.github.io/papers/winterer-zhang-su-pldi20.pdf">-->
[1] <a href="https://dl.acm.org/doi/pdf/10.1145/3385412.3385985">
<b>Validating SMT Solvers via Semantic Fusion</b></a>. <br> [<a href="https://testsmt.github.io/slides/pldi20-semantic-fusion.pdf">slides</a> |
<a href="https://www.youtube.com/watch?list=PLyrlk8Xaylp5mvxARtX5ncjy9p4X_Ajwd&time_continue=1&v=JFu8cJYbxBI&feature=emb_logo">abstract video</a> |
<a href="https://www.youtube.com/watch?v=hEWpbO5yXPw&list=PLyrlk8Xaylp5mvxARtX5ncjy9p4X_Ajwd&index=178">talk video</a>] <br>
Dominik Winterer<sup>*</sup>, Chengyu Zhang<sup>*</sup> and Zhendong Su </br>
In <a href="https://conf.researchr.org/home/pldi-2020"><I>Proceedings of PLDI 2020</I></a>, London, UK, June 2020. </br>
<div style="font-size:10pt"><sup>*</sup>
Both authors contributed equally to this work.
</div>
<img class="" src="/img/award.png" alt="" width="20pt"/> <font color="#d9381e">PLDI Distinguished Paper Award</font>
</div>
<div class="notice--primary">
[2] <a href="https://dl.acm.org/doi/abs/10.1145/3428261"><b>On the Unusual Effectiveness of Type-aware Operator Mutations for Testing SMT Solvers</b></a>. <br> [<a href="https://testsmt.github.io/slides/oopsla20-type-aware-op-mutation.pdf">slides</a> |
<a href="https://www.youtube.com/watch?v=uCEN3AnBYC0&feature=emb_title">abstract video</a> |
<a href="https://www.youtube.com/watch?v=sbQX2SnCKHA">talk video</a>]
<br>
Dominik Winterer<sup>*</sup>, Chengyu Zhang<sup>*</sup> and Zhendong Su</br>
In <a href="https://2020.splashcon.org/"><I>Proceedings of SPLASH/OOPSLA 2020</I></a>, November 2020.
</br>
<div style="font-size:10pt;margin-bottom:-10pt"><sup>*</sup> Both authors contributed equally to this work. </div>
</div>
<div class="notice--primary">
[3] <a href="https://wintered.github.io/papers/park-etal-oopsla21.pdf"><B>Generative Type-Aware Mutation for Testing SMT Solvers.</B></a>
<br> [<a href="https://www.youtube.com/watch?v=Jxc4N4mrm8o&t=2s&ab_channel=ACMSIGPLAN">talk video</a>] <br>
Jiwon Park<sup>*</sup>, Dominik Winterer<sup>*</sup>, Chengyu Zhang and Zhendong Su</br>
In <a href="https://2021.splashcon.org/track/splash-2021-oopsla"><I>Proceedings of SPLASH/OOPSLA 2021</I></a>, October 2021 </br>
<div style="font-size:10pt;margin-bottom:-10pt "><sup>*</sup>
Both authors contributed equally to this work.
</div>
</div>
<div class="notice--primary">
[4] <a href="https://testsmt.github.io/papers/bringolf-winterer-su-ase22.pdf"><B>Finding and Understanding Incompleteness Bugs in SMT Solvers.</B></a> <br>
<!--[<a href="https://testsmt.github.io/slides/oopsla21-generative-type-aware-mutation.pdf">slides</a> | -->
<!--<a href="https://www.youtube.com/watch?v=Jxc4N4mrm8o&t=2s&ab_channel=ACMSIGPLAN">talk video</a>] <br>-->
Mauro Bringolf, Dominik Winterer and Zhendong Su</br>
In <a href="https://conf.researchr.org/home/ase-2022"><I>Proceedings of ASE 2022</I></a>, October 2022 </br>
</div>
<center><h1 id="contributors">Contributors</h1></center><br>
<div style="width: 19%; display: inline-block; text-align: center;">
<div class="author__avatar">
<a href="https://wintered.github.io/"><img src="/img/dominik.png" itemprop="image"></a>
</div>
<div class="author__content">
<h3 class="author__name" itemprop="name"><a href="https://wintered.github.io/">Dominik <br> Winterer</a></h3>
</div>
</div>
<div style="width: 19%; display: inline-block; text-align: center">
<div class="author__avatar">
<a href="http://chengyuzhang.com"><img src="/img/chengyu.jpg" itemprop="image"></a>
</div>
<div class="author__content">
<h3 class="author__name" itemprop="name"><a href="http://chengyuzhang.com">Chengyu <br> Zhang</a></h3>
</div>
</div>
<div style="width: 19%; display: inline-block; text-align: center;">
<div class="author__avatar">
<a href="https://www.linkedin.com/in/jiwon-park-473998170/?originalSubdomain=fr"><img src="/img/jiwon.jpg" itemprop="image"></a>
</div>
<div class="author__content">
<h3 class="author__name" itemprop="name"><a href="https://www.linkedin.com/in/jiwon-park-473998170/?originalSubdomain=fr">Jiwon <br> Park</a></h3>
</div>
</div>
<div style="width: 19%; display: inline-block; text-align: center;">
<div class="author__avatar">
<a href="https://maurobringolf.ch/"><img src="/img/Mauro.jpg" itemprop="image"></a>
</div>
<div class="author__content">
<h3 class="author__name" itemprop="name"><a href="https://maurobringolf.ch/">Mauro <br> Bringolf</a></h3>
</div>
</div>
<div style="width: 19%; display: inline-block; text-align: center;">
<div class="author__avatar">
<a href="https://people.inf.ethz.ch/suz"><img src="/img/zhendong.jpg" itemprop="image"></a>
</div>
<div class="author__content">
<h3 class="author__name" itemprop="name"><a href="https://people.inf.ethz.ch/suz">Zhendong <br> Su</a></h3>
</div>
</div>
<br>
<br>
<!-- <a href="https://wintered.github.io/">Dominik Winterer</a> <br>
<a href="http://chengyuzhang.com">Chengyu Zhang</a> <br>
<a href="https://www.linkedin.com/in/jiwon-park-473998170/?originalSubdomain=fr">Jiwon Park</a> <br>
<a href="https://maurobringolf.ch/">Mauro Bringolf</a> <br>
<a href="https://people.inf.ethz.ch/suz">Zhendong Su</a> <br><br> -->
<center><h1 id="acknowledgments">Acknowledgments</h1></center>
This project is partially supported by an <a href="https://www.amazon.science/research-awards/recipients/zhendong-su-fall-2021">Amazon Research Award (Fall '21)</a>.
We are also grateful to Google for an <a href="https://opensource.googleblog.com/2021/04/announcing-first-group-of-google-open-source-peer-bonus-winners.html">open source peers bonus</a>.
</font>
<br>
<br>
<br>
<center><a class="twitter-timeline" data-width="600" data-height="400" data-theme="light" href="https://twitter.com/testsmtsolvers?ref_src=twsrc%5Etfw">Tweets by testsmtsolvers</a> <script async src="https://platform.twitter.com/widgets.js" charset="utf-8"></script></center>
<br><br><br><br>
<tt>last modified: 2022.09.29</tt>
<script>
function animate(obj, initVal, lastVal, duration) {
let startTime = null;
//get the current timestamp and assign it to the currentTime variable
let currentTime = Date.now();
//pass the current timestamp to the step function
const step = (currentTime ) => {
//if the start time is null, assign the current time to startTime
if (!startTime) {
startTime = currentTime ;
}
//calculate the value to be used in calculating the number to be displayed
const progress = Math.min((currentTime - startTime)/ duration, 1);
//calculate what to be displayed using the value gotten above
obj.innerHTML = Math.floor(progress * (lastVal - initVal) + initVal);
//checking to make sure the counter does not exceed the last value (lastVal)
if (progress < 1) {
window.requestAnimationFrame(step);
} else {
window.cancelAnimationFrame(window.requestAnimationFrame(step));
}
};
//start animating
window.requestAnimationFrame(step);
}
let text1 = document.getElementById('totalnum');
let text2 = document.getElementById('fixednum');
const load = () => {
animate(text1, 0, 1667, 3000);
animate(text2, 0, 1244, 3000);
}
</script>
</body>
</html>
<!-- cannot change the footer template because it's computed only once for all pages -->
<style>#footer {display: none} </style>