Satisfiability Modulo Theories

Modalita' d'esame

Per la parte di SMT sono previste due modalita':

• Prova orale: si portano le lezioni dalla 1 alla 9, di cui una lezione a scelta tra 2-7 in modo dettagliato. Per chi dovesse solo portare meta' programma, il tutto e' ridotto fino alla lezione 5 inclusa. Oppure
• Progetto: si porta l'implementazione dell'algoritmo di Floyd-Warshall come theory-solver per IDL in OpenSMT. Non e' necessario che l'implementazione sia efficiente. E' sufficiente che dia risultati corretti per almeno i seguenti files: job-shop (il loro status e' riportato nei file stessi). Si discuteranno a voce i dettagli dell'algoritmo e dell'implementazione. Si portano inoltre le lezioni 4 e 5.

La parte di SMT da sola non e' sufficiente per il Corso di Logica Matematica (Laurea Magistrale). Vedi link1, link2.

Lectures

Lecture 1: Slides (handouts) , Examples
Lecture 2: Slides (handouts) , Examples
Lecture 3: Slides (handouts)
Lecture 4: Slides (handouts) , OpenSMT (pwd protected) , Compilation Instructions
Lecture 5: Slides (handouts)
Lecture 6: Slides (handouts)
Lecture 7: Slides (handouts)
Lecture 8: Slides (handouts) , Examples , Link to MCMT page
Lecture 9: Slides (handouts) , "Original" and "Final" OpenSMT (pwd protected) , Examples
Lecture 10: Slides (handouts)

Manuscript

Satisfiability Modulo Theories: a pragmatic introduction (in preparation, up to chapter 1)

Resources

SMT-solvers (used in this course):

• smtlib2yices (developed by Alberto Griggio - requires Yices to work)
• Yices (developed at SRI, Stanford)
• Z3 (developed at MSR, Redmond)
• OpenSMT (developed at UniMi)

SMT-LIB website: a collection of theory definitions and benchmarks

SMT-COMP website: an annual competition for SMT-solvers