adding entries for mtrberzi sat-smt talk
authorPatrick Melanson <pj2melan@uwaterloo.ca>
Wed, 4 Mar 2015 02:21:41 +0000 (21:21 -0500)
committerPatrick Melanson <pj2melan@uwaterloo.ca>
Wed, 4 Mar 2015 02:21:41 +0000 (21:21 -0500)
events.xml
media/index.xml

index 359e7f8..bb9ebab 100644 (file)
@@ -77,8 +77,7 @@
       <br></br>
       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.
       <br></br>
       What else? Oh yes, refreshments and drinks will be served. Come out!
     </p>
index ba43076..e6f98a4 100644 (file)
     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>