-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
256 lines (247 loc) · 11.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
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>Proof Engineering</title>
<link rel='stylesheet' type='text/css' href='css/main.css'>
</head>
<body>
<div id='header'>
<div class='floatL'>
<h1 id='header-title'>Proof Engineering</h1>
</div>
<div class='floatR'>
<img id='header-logo' src='img/pe-logo.png'>
</div>
<div class='clearB'></div>
</div>
<p>
Specifying, building, verifying, and maintaining software systems using proof assistants such as
<a href="https://coq.inria.fr">Coq</a>, <a href="https://isabelle.in.tum.de">Isabelle/HOL</a>,
and <a href="https://hol-theorem-prover.org">HOL4</a>
enables high trustworthiness, but is currently challenging in many ways.
</p>
<p>
Proof scripts may break easily when definitions are changed, new theorems may be hard to add,
and updating the proof assistant itself may break existing definitions and proofs.
Proof assistant logics are also highly expressive; engineers must ensure that their
specifications can be satisfied with reasonable effort while disallowing undesirable behavior.
Large-scale projects often require extensive proof automation, forcing
engineers to measure and optimize the performance of low-level reasoning steps.
</p>
<p>
To help address challenges like these, the
<a href="https://github.com/ProofEngineering">Proof Engineering</a>
(PE) project is collecting best
practices and developing techniques and tools for building large systems in
the demanding and foundational context of proof assistants.
</p>
<h2>News</h2>
<p>
<span class='post-date'>May 2020</span> Extended abstract at Coq Workshop 2020.
</p>
<p>
<span class='post-date'>Mar 2020</span> Paper in IJCAR 2020.
</p>
<p>
<span class='post-date'>Jan 2020</span> Papers in TACAS 2020 and ICSE-Demo 2020.
</p>
<p>
<span class='post-date'>Nov 2019</span> Paper in CPP 2020.
</p>
<p>
<span class='post-date'>Sep 2019</span> Paper in FTPL.
</p>
<p>
<span class='post-date'>Aug 2019</span> Paper in ASE 2019.
</p>
<p>
<span class='post-date'>May 2019</span> Paper in ITP 2019.
</p>
<span class='post-date'>Nov 2018</span> Won a <a href="https://research.fb.com/announcing-the-winners-of-the-facebook-continuous-reasoning-research-awards/">research award</a> from Facebook.
</p>
<p>
<span class='post-date'>May 2018</span> Paper in ISSTA 2018.
</p>
<p>
<span class='post-date'>Feb 2018</span> Paper in ICSE-Demo 2018.
</p>
<p>
<span class='post-date'>Nov 2017</span> Papers in ASE 2017 and CPP 2018.
</p>
<p>
<span class='post-date'>May 2017</span> Site goes live.
</p>
<h2>Errata and resources for proof engineering survey</h2>
<p>
We maintain <a href="qed_errata.html">errata</a> for our proof engineering survey (<a href="https://arxiv.org/abs/2003.06458">QED at Large</a>).
If you find any additional errors, please report them as a GitHub <a href="https://github.com/proofengineering/proofengineering.github.io/issues">issue</a>, as a <a href="https://github.com/proofengineering/proofengineering.github.io/pulls">pull request</a> modifying the errata <a href="https://github.com/proofengineering/proofengineering.github.io/blob/master/qed_errata.md">source file</a>, or by contacting the survey authors directly.</p>
<p>
The complete source code for the verified regular expression matcher Coq project used as a motivating example in Chapter 2 of the survey is <a href="https://github.com/proofengineering/regmatch/tree/qed-at-large">available on GitHub</a>.
</p>
<p>
Talia has written a <a href="https://taliasplse.wordpress.com/2019/09/14/proof-engineering-survey-paper-qed-a/">Q&A</a> for the survey, including reading
guides for readers of different backgrounds.
</p>
<h2>Publications</h2>
<ul>
<li>
Pengyu Nie, Karl Palmskog, Junyi Jessy Li, and Milos Gligoric<br>
<i>
<a href="https://arxiv.org/abs/2006.16743">Learning to Format Coq Code Using Language Models</a>
</i>
<br>
The Coq Workshop<br>
(Coq 2020), Paris, France, July 2020.
</li>
<li>
Pengyu Nie, Karl Palmskog, Junyi Jessy Li, and Milos Gligoric<br>
<i>
<a href="https://arxiv.org/abs/2004.07761">Deep Generation of Coq Lemma Names Using Elaborated Terms</a>
</i>
<br>
International Joint Conference on Automated Reasoning<br>
(IJCAR 2020), 97-118, Paris, France, July 2020.
</li>
<li>
Kush Jain, Karl Palmskog, Ahmet Celik, Emilio Jesús Gallego Arias, and Milos Gligoric<br>
<i>
<a href="http://users.ece.utexas.edu/~gligoric/papers/JainETAL20mCoqTool.pdf">mCoq: Mutation Analysis for Coq Verification Projects</a>
</i>
<br>
International Conference on Software Engineering, Tool Demonstrations Track<br>
(ICSE Demo 2020), 89-92, Seoul, South Korea, July 2020.
</li>
<li>
Karl Palmskog, Ahmet Celik, and Milos Gligoric<br>
<i>
<a href="http://users.ece.utexas.edu/~gligoric/papers/PalmskogETAL20Chip.pdf">Practical Machine-Checked Formalization of Change Impact Analysis</a>
</i>
<br>
International Conference on Tools and Algorithms for the Construction and Analysis of Systems<br>
(TACAS 2020), 137-157, 2020.
</li>
<li>
Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner<br>
<i>
<a href="http://tlringer.github.io/pdf/analytics.pdf">REPLICA: REPL Instrumentation for Coq Analysis</a>
</i>
<br>
International Conference on Certified Programs and Proofs<br>
(CPP 2020), 99-113, New Orleans, LA, USA, January 2020.
</li>
<li>
Ahmet Celik, Karl Palmskog, Marinela Parovic, Emilio Jesús Gallego Arias, and Milos Gligoric<br>
<i>
<a href="https://users.ece.utexas.edu/~gligoric/papers/CelikETAL19mCoq.pdf">Mutation Analysis for Coq</a>
</i>
<br>
International Conference on Automated Software Engineering<br>
(ASE 2019), 539-551, San Diego, CA, USA, November 2019.
</li>
<li>
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman<br>
<i>
<a href="https://tlringer.github.io/pdf/ornpaper.pdf">Ornaments for Proof Reuse in Coq</a>
</i>
<br>
International Conference on Interactive Theorem Proving<br>
(ITP 2019), 26:1-26:19, Portland, OR, USA, September 2019.
</li>
<li>
Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock<br>
<i>
<a href="https://arxiv.org/abs/2003.06458">QED at Large: A Survey of Engineering of Formally Verified Software</a>
</i>
<br>
Foundations and Trends in Programming Languages<br>
(FTPL), Vol. 5: No. 2-3, pp 102-281, September 2019.
</li>
<li>
Karl Palmskog, Ahmet Celik, and Milos Gligoric<br>
<i>
<a href="http://users.ece.utexas.edu/~gligoric/papers/PalmskogETAL18piCoq.pdf">piCoq: Parallel Regression Proving for Large-Scale Verification Projects</a>
</i>
<br>
International Symposium on Software Testing and Analysis<br>
(ISSTA 2018), 344-355, Amsterdam, The Netherlands, July 2018.
</li>
<li>
Ahmet Celik, Karl Palmskog, and Milos Gligoric<br>
<i>
<a href="http://users.ece.utexas.edu/~gligoric/papers/CelikETAL18iCoqTool.pdf">A Regression Proof Selection Tool for Coq</a>
</i>
<br>
International Conference on Software Engineering, Tool Demonstrations Track<br>
(ICSE Demo 2018), 117-120, Gothenburg, Sweden, May 2018.
</li>
<li>
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman<br>
<i>
<a href="http://tlringer.github.io/pdf/pumpkinpaper.pdf">Adapting Proof Automation to Adapt Proofs</a>
</i>
<br>
International Conference on Certified Programs and Proofs<br>
(CPP 2018), 115-129, Los Angeles, CA, USA, January 2018.
</li>
<li>
Ahmet Celik, Karl Palmskog, and Milos Gligoric<br>
<i>
<a href="http://users.ece.utexas.edu/~gligoric/papers/CelikETAL17iCoq.pdf">iCoq: Regression Proof Selection for Large-Scale Verification Projects</a>
</i>
<br>
International Conference on Automated Software Engineering<br>
(ASE 2017), 171-182, Urbana-Champaign, IL, USA, November 2017.
</li>
</ul>
<h2>Current Projects</h2>
<p>
<ul>
<li>Proof assistant machine learning datasets (<a href="https://github.com/EngineeringSoftware/math-comp-corpus">MathComp corpus</a>)</li>
<li>Learning and suggesting proof assistant coding conventions (<a href="https://github.com/EngineeringSoftware/roosterize">Roosterize</a>)</li>
<li>Proof assistant change analytics (<a href="https://github.com/uwplse/analytics-data">Coq data</a>)</li>
<li>Mutation proving (<a href="http://cozy.ece.utexas.edu/mcoq">mCoq</a>)</li>
<li>Ornamental search (<a href="https://github.com/uwplse/ornamental-search">DEVOID</a>)</li>
<li>Survey of proof engineering theory, techniques, tools, and best practices (<a href="https://arxiv.org/abs/2003.06458">QED at Large</a>)</li>
<li>Proof checking parallelization (<a href="https://cozy.ece.utexas.edu/icoq">piCoq</a>)</li>
<li>Proof repair (<a href="https://github.com/uwplse/PUMPKIN-PATCH">PUMPKIN-PATCH</a>)</li>
<li>Regression proof selection (<a href="https://cozy.ece.utexas.edu/icoq">iCoq</a> and <a href="https://github.com/palmskog/chip">Chip</a>)</li>
<li>Proof engineering bibliography (<a href="https://github.com/proofengineering/proofengineering-bib">proofengineering-bib</a>)</li>
<li>Proof document serialization (<a href="https://github.com/ejgallego/coq-serapi">SerAPI</a>)</li>
</ul>
<h2>Contributors</h2>
<p>
PE is an international collaboration between researchers at
<a href="https://www.washington.edu">University of Washington</a>, <a href="https://www.yale-nus.edu.sg">Yale-NUS College</a>,
<a href="https://www.utexas.edu">The University of Texas at Austin</a>, <a href="https://www.kth.se">KTH Royal Institute of Technology</a>, <a href="https://www.inria.fr">Inria</a>, and <a href="https://u-paris.fr">Université de Paris</a>.
People currently working on PE include:
</p>
<ul>
<li><a href="https://ahmet-celik.github.io">Ahmet Celik</a></li>
<li><a href="https://www.irif.fr/~gallego/">Emilio Jesús Gallego Arias</a></li>
<li><a href="https://users.ece.utexas.edu/~gligoric">Milos Gligoric</a></li>
<li><a href="https://homes.cs.washington.edu/~djg">Dan Grossman</a></li>
<li><a href="https://setoid.com">Karl Palmskog</a></li>
<li><a href="https://tlringer.github.io">Talia Ringer</a></li>
<li><a href="https://ilyasergey.net">Ilya Sergey</a></li>
<li><a href="https://homes.cs.washington.edu/~ztatlock">Zachary Tatlock</a></li>
</ul>
<p>
We're very grateful for the contributions of the following people:
</p>
<ul>
<li>Justin Adsuara</li>
<li><a href="http://ryandoeng.es">Ryan Doenges</a></li>
<li>Kush Jain</li>
<li><a href="https://www.halfaya.org/leo/">John Leo</a></li>
<li><a href="https://cseweb.ucsd.edu/~lerner/">Sorin Lerner</a></li>
<li><a href="http://jessyli.com">Junyi Jessy Li</a></li>
<li><a href="https://cozy.ece.utexas.edu/~pynie">Pengyu Nie</a></li>
<li><a href="http://alex.uwplse.org">Alex Sanchez-Stern</a></li>
<li>Marinela Parovic</li>
<li><a href="https://jamesrwilcox.com">James R. Wilcox</a></li>
<li><a href="https://www.dougwoos.com">Doug Woos</a></li>
<li><a href="https://nyazdani.com">Nathaniel Yazdani</a></li>
</ul>
</body>
</html>