diff --git a/events.xml b/events.xml
index 359e7f8..bb9ebab 100644
--- a/events.xml
+++ b/events.xml
@@ -77,8 +77,7 @@
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 verifica-
- tion.
+ SAT/SMT solvers in theorem proving, model checking, and program verification.
What else? Oh yes, refreshments and drinks will be served. Come out!
+ 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? +
++ 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. +
++ 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. +
++ 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. +
+