Slides

Slide

Introductory

• 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)

Tutorials and Summer Schools

• 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)|http://research.microsoft.com/projects/z3/slides/z3tutorial.pdf] [url:(PowerPoint)|http://research.microsoft.com/projects/z3/slides/z3tutorial.pptx].
• [url:SMT Solvers: Theory and Implementation|http://research.microsoft.com/~leonardo/oregon08.pdf], [url:Summer School on Logic and Theorem Proving in Programming Languages|http://www.cs.uoregon.edu/research/summerschool/summer08], Oregon 2008.
• SMT Solvers in Program Verification and Analysis, [url:MSR India Summer School on Programming Languages, Analysis and Verification|http://research.microsoft.com/ur/india/erp/summerschool2008/], Bangalore, June 2008. [url:Lecture 1|http://research.microsoft.com/~nbjorner/lecture1.pptx] [url:Lecture 2|http://research.microsoft.com/~nbjorner/lecture2.pptx] [url:Lecture 3|http://research.microsoft.com/~nbjorner/lecture3.pptx] [url:Lecture 4|http://research.microsoft.com/~nbjorner/lecture4.pptx] [url:Lecture 5|http://research.microsoft.com/~nbjorner/lecture5.pptx] [url:Lab Exercises|http://research.microsoft.com/~nbjorner/lab.pdf]. Student solutions: [url:Ashish Sharma|http://summerschool-ashish.blogspot.com/].
• [url:Tutorial on SMT solvers|http://research.microsoft.com/projects/z3/fmcad06-slides.pdf], [url:FMCAD 2006|http://www.cc.gatech.edu/~manolios/fmcad06/program.html].

Technical presentations

• [url:SMT: Techniques, Hurdles, Applications|http://research.microsoft.com/en-us/um/people/leonardo/mit2011.pdf], [url:First International SAT/SMT Solver Summer School 2011|http://people.csail.mit.edu/vganesh/summerschool/], MIT, 2011
• [url:Orchestrating Decision Engines|http://research.microsoft.com/~leonardo/cp2011.pdf], [url:CP'2011|http://www.dmi.unipg.it/cp2011/program.html], Perugia, Italy, 2011
• [url:Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development|http://research.microsoft.com/~leonardo/IJCAR2010_slides.pdf], Invited talk at [url:IJCAR'2010|http://www.floc-conference.org/IJCAR-home.html], Edinburgh, UK, 2010
• [url:Generalized and Efficient Array Decision Procedures|http://research.microsoft.com/~leonardo/fmcad09-slides.pdf], [url:FMCAD|http://fmv.jku.at/fmcad09], Austin TX, 2009.
• [url:Applications and Challenges in Satisfiability Modulo Theories|http://research.microsoft.com/~leonardo/wing09.pdf], [url:WING 2009|http://mtc.epfl.ch/events/WING09/], York, England ([url:Powerpoint Slides|http://research.microsoft.com/~leonardo/wing09.pptx]).
• [url:Complete Instantiation for Quantified Formulas in SMT|http://research.microsoft.com/~leonardo/cav2009.pdf], [url:CAV 2009|http://www-cav2009.imag.fr/], Grenoble, France.
• [url:Quantifiers in Satisfiability Modulo Theories|http://research.microsoft.com/~leonardo/qsmt.pdf], [url:Frontiers of Computational Reasoning|http://www.dcs.qmul.ac.uk/~ohearn/Workshops/Reasoning09], Cambridge, England ([url:Powerpoint Slides|http://research.microsoft.com/~leonardo/qsmt.pptx]).
• [url:Accelerating lemma learning using joins|http://research.microsoft.com/~leonardo/LPAR08.pdf], [url:LPAR 2008|http://www.qatar.cmu.edu/lpar08/program.shtml], Doha, Qatar ([url:Powerpoint Slides|http://research.microsoft.com/~leonardo/LPAR08.pptx]).
• [url:Software Verification and Testing|http://research.microsoft.com/~leonardo/NSF2008.pdf], [url:NSF Workshop on Symbolic Computation for Constraint Satisfaction Problems|http://www.cis.upenn.edu/~alur/nsfsymbolic08.html], Virginia, 2008 ([url:Powerpoint Slides|http://research.microsoft.com/~leonardo/NSF2008.pptx]).
• [url:Experiments in Software Verification using SMT solvers|http://research.microsoft.com/~leonardo/vs_experiments.pdf], [url:VS Experiments'08|http://web.me.com/kiniry/VS-EXPERIMENTS/WORKSHOP_ON_EXPERIMENTS_IN_VERIFIED_SOFTWARE.html], Toronto, Canada 2008 ([url:Powerpoint Slides|http://research.microsoft.com/~leonardo/vs_experiments.pptx]).
• [url:Engineering DPLL(T) + Saturation (PDF)|http://research.microsoft.com/~leonardo/ijcar08.pdf], [url:IJCAR'08|http://www.ijcar.org/2008], Sydney, Australia 2008 ([url:Powerpoint Slides|http://research.microsoft.com/~leonardo/ijcar08.pptx]).
• [url:Efficient E-matching for SMT solvers|http://research.microsoft.com/projects/z3/cade07-slides.pdf], [url:CADE 2007|http://www.cadeconference.org/meetings/cade21].
• [url:Model-based Theory Combination|http://research.microsoft.com/projects/z3/smt07-slides.pdf], [url:SMT 2007|http://www.lsi.upc.edu/~oliveras/smt07].
• [url:Developing Efficient SMT Solvers|http://research.microsoft.com/projects/z3/cmu07.pdf], [url:CMU 2007|http://www.cs.cmu.edu/~svc/talks/20070507-deMoura.html].