-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathindex_old.html
140 lines (113 loc) · 7.28 KB
/
index_old.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
<!DOCTYPE doctype PUBLIC "-//w3c//dtd html 4.0 transitional//en">
<html>
<head>
<meta http-equiv="Content-Type"content="text/html; charset=iso-8859-1">
<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">
<meta name="msapplication-TileColor" content="#da532c">
<meta name="theme-color" content="#ffffff">
<title>Project Yin-Yang</title>
</head>
<body bgcolor="#ffffff">
<link type="text/css" rel="stylesheet" href="style.css">
<font face="ariel,helvetica">
<h2>Project Yin-Yang for SMT Solver Testing</h2>
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.
YinYang and OpFuzz, the realizations of semantic fusion and type-aware
operator mutation, have demonstrated their remarkable effectiveness by
having already <b>found 1,500+ bugs in Z3 and CVC4/5</b>, the two
state-of-the-art SMT solvers.
<p>
We have maintained our continuous, extensive effort in stress-testing
Z3 and CVC4 to benefit the SMT solver developer, user, and research
communities:
<p>[Summary: <b>1,677</b> (total) / <b>1,244</b> (fixed)]<br>
<p>[Z3 bugs: <b>1,199</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>
<p><img class="" src="./img/tool_logo.png" alt="" width="25pt" style="margin-bottom:-8px; margin-right:5px"/> <b>yinyang Tool</b>: <a href="https://github.com/testsmt/yinyang">https://github.com/testsmt/yinyang</a></p>
Please follow us on
Twitter <a href="https://twitter.com/testsmtsolvers">@testsmtsolvers</a> for
important project developments and regular tweets about interesting
bugs in Z3 and CVC4.
<h3>Contributors</h3>
<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>
<h3>Publications</h3>
<!--<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>. [<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">video abstract</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;margin-bottom:-10pt "><sup>*</sup>
Both authors contributed equally to this work.
</div>
<br> <img class="" src="./img/award.png" alt="" width="20pt"/> <font color="red">PLDI Distinguished Paper Award</font> <br><br>
[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">video abstract</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>
</br>
</br>
[3] <a href="https://wintered.github.io/papers/park-etal-oopsla21.pdf"><B>Generative Type-Aware Mutation for Testing SMT Solvers.</B></a>
[<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>
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>
<br>
<br>
[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>
<br>
<h3>Acknowledgments</h3>
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><br>
<tt>last modified: 2022.09.15</tt>
</body>
</html>