|
|
|
@ -11,6 +11,41 @@ |
|
|
|
|
CD or DVD should you so choose. |
|
|
|
|
<ul class="media"> |
|
|
|
|
|
|
|
|
|
<mediaitem title="SAT and SMT solvers"> |
|
|
|
|
<abstract> |
|
|
|
|
<p> |
|
|
|
|
Does your program have an overflow error? Will it work with all inputs? |
|
|
|
|
How do you know for sure? Test cases are the bread and butter of |
|
|
|
|
resilient design, but bugs still sneak into software. What if we could |
|
|
|
|
prove our programs are error-free? |
|
|
|
|
</p> |
|
|
|
|
<p> |
|
|
|
|
Boolean Satisfiability (SAT) solvers determine the ‘satisfiability’ of |
|
|
|
|
boolean set of equations for a set of inputs. An SMT solver |
|
|
|
|
Satisfiability Modulo a Theory) applies SMT to bit-vectors, strings, |
|
|
|
|
arrays, and more. Together, we can reduce a program and prove it is |
|
|
|
|
satisfiable, or provide a concrete counter-example. The implications of |
|
|
|
|
this are computer-aided reasoning tools for error-checking in addition |
|
|
|
|
to much more robust programs. |
|
|
|
|
</p> |
|
|
|
|
<p> |
|
|
|
|
In this talk Murphy Berzish will give an overview of SAT/SMT theory and |
|
|
|
|
some real-world solution methods. He will also demonstrate applications |
|
|
|
|
of SAT/SMT solvers in theorem proving, model checking, and program |
|
|
|
|
verification. |
|
|
|
|
</p> |
|
|
|
|
<p> |
|
|
|
|
There are both .pdf slides and a .mp4 recording of the talk. Code samples |
|
|
|
|
and spellings of terms are in the slides, consider following along with |
|
|
|
|
the slides. |
|
|
|
|
</p> |
|
|
|
|
</abstract> |
|
|
|
|
<presentor>Murphy Berzish</presentor> |
|
|
|
|
<thumbnail file="mtrberzi-sat-smt-thumb-small.jpg" /> |
|
|
|
|
<mediafile file="mtrberzi-sat-smt.mp4" type="Talk (x264)" /> |
|
|
|
|
<mediafile file="mtrberzi-sat-smt-slides.pdf" type="Talk (PDF)" /> |
|
|
|
|
</mediaitem> |
|
|
|
|
|
|
|
|
|
<mediaitem title="Racket's Magical Match"> |
|
|
|
|
<abstract> |
|
|
|
|
<p> |
|
|
|
|