Slides
Nikolaj Bjorner edited this page Jul 9, 2017
·
14 revisions
- Z3: An Efficient SMT Solver (PDF), TACAS, Budapest, Hungary, 2008 (Powerpoint Slides).
- SMT@Microsoft, Max Planck Institut Informatik, Germany, 2009.
- Satisfiability Modulo Theories: An Appetizer, SBMF 2009, Gramado, Brazil (Powerpoint Slides)
- Programming constraint services with Z3 [NUS 2016]
- Summer School on Formal Techniques, Menlo Park, 2014.
- Verified Software Summer School, Shanghai, Aug 2012 Lecture 1 Lecture 2 Lecture 3 Lecture 4
- First Summer School on Formal Techniques, Menlo Park, 2011.
- Satisfiability Modulo Theories (SMT): Ideas and Applications, Universita Degli Studi di Milano, Italy, March 2010 (part 1, part 2, part 3, part 4, assignment).
- Satisfiability with and without theories, Invited tutorial at KR'2010, Toronto, Canada, 2010
- On Designing and Implementing Satisfiability Modulo Theory Solvers, Summer School 2009: Verification Technology, Systems and Applications, Nancy, France (lecture 1, lecture 2)
- Invited Tutorial: Applications of SMT solvers in Software Verification, VSTTE'08, Toronto, Canada 2008 (Powerpoint Slides)
- Tutorial on SMT solvers in program analysis and Verification at Microsoft, Presented at IJCAR, Australia 2008 url:(PDF) (PowerPoint).
- SMT Solvers: Theory and Implementation, [Summer School on Logic and Theorem Proving in Programming Languages] Oregon 2008.
- SMT Solvers in Program Verification and Analysis, MSR India Summer School on Programming Languages, Analysis and Verification, Bangalore, June 2008. Lecture 1 Lecture 2 Lecture 3 Lecture 4 Lecture 5 Lab Exercises. Student solutions: Ashish Sharma.
- Tutorial on SMT solvers, FMCAD 2006.
- SMT: Techniques, Hurdles, Applications, First International SAT/SMT Solver Summer School 2011, MIT, 2011
- Orchestrating Decision Engines, CP'2011, Perugia, Italy, 2011
- Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development, Invited talk at IJCAR'2010, Edinburgh, UK, 2010
- Generalized and Efficient Array Decision Procedures, FMCAD, Austin TX, 2009.
- Applications and Challenges in Satisfiability Modulo Theories, WING 2009, York, England (Powerpoint Slides).
- Complete Instantiation for Quantified Formulas in SMT, CAV 2009, Grenoble, France.
- Quantifiers in Satisfiability Modulo Theories, Frontiers of Computational Reasoning, Cambridge, England (Powerpoint Slides).
- Accelerating lemma learning using joins, LPAR 2008, Doha, Qatar (Powerpoint Slides).
- Software Verification and Testing, NSF Workshop on Symbolic Computation for Constraint Satisfaction Problems, Virginia, 2008 (Powerpoint Slides).
- Experiments in Software Verification using SMT solvers, VS Experiments'08, Toronto, Canada 2008 (Powerpoint Slides).
- Engineering DPLL(T) + Saturation (PDF), IJCAR'08, Sydney, Australia 2008 (Powerpoint Slides).
- Efficient E-matching for SMT solvers, CADE 2007.
- Model-based Theory Combination, SMT 2007.
- Developing Efficient SMT Solvers, CMU 2007.