Most of my publications are available on-line. See DBLP and Google Scholar for more details.

DBLP » Google Scholar »


Many of the PowerPoint slides use TexPoint. It might need to be installed to see them properly.

  • Regression Verification of Multi-Threaded Programs, April 10, 2018, Program Equivalence, Dagstuhl Seminar 18151. (PPT) (PDF)
  • SeaHorn: Software Model Checking with SMT and AI. Invited tutorial at Haifa Verification Conference (HVC). Haifa, 2017. (PPT) (PDF)
  • Pushing to the Top with k-induction, November 12, 2017, The Technion, Haifa. (PPT) (PDF)
  • A Context Sensitive Memory Model for Software Model Checking, November 5, 2017, Tel Aviv University. (PPT) (PDF)
  • Solving Constrained Horn Clauses by Property Directed Reachability, August 7, 2017, Workshop on Horn Clauses for Verification and Synthesis (HCVS) (PPT) (PDF).
  • System Verification by Abstract Interpretation and Model Checking, January 21, 2017, N40AI Workshop. (PPT)
  • Algorithmic Logic-Based Verification with SeaHorn, November 16, 2016, University of Washington, Seattle. (PPT)
  • SMT-Based Verification of Parameterized Systems, Foundations of Software Engineering (FSE), November 15, 2016, Seattle. (PPT) (PDF) (Paper)
  • Algorithmic Logic-Based Verification with SeaHorn, October 7, 2016, 4th Workshop on Software Correctness and Reliability , ETH, Zurich. (PPT) (PDF) (Video)
  • Algorithmic Logic-Based Verification with SeaHorn, October 6, 2016, Università della Svizzera Italiana (PPT)
  • Algorithmic Logic-Based Verification: Parameterized Systems, Tenth IFIP WG 1.9/2.15 Meeting on Verified Software, Montauban, France, October 2, 2016. (PPT) (PDF)
  • Algorithmic Logic-Based Verification, May 19, 2016, Synergies among Testing, Verification, and Repair for Concurrent Programs, Dagstuhl Seminar 16201 . (PPT) (PDF)
  • Lecture on Automated Program Analysis with Software Model Checking, February, 2016. (PPT) (PDF)
  • Algorithmic Logic-based Verification with SeaHorn. Invited tutorial at the 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2015). September, 2015. (PPT) (PDF)
  • Parametric Symbolic Reachability, September 14, 2015, Information from Deduction: Models and Proofs, Dagstuhl Seminar 13051. (PPT) (PDF)
  • Interpolating Property Directed Reachability. Invited talk at 3rd International Workshop on Interpolation: From Proofs to Applications (PPT)
  • Building Program Verifiers from Compilers and Theorem Provers, Fifth Summer School on Formal Techniques (materials)
  • The SeaHorn Verification Framework, April 2015, Invited talk at 3rd International Workshop on Verification and Program Transformation (VPT 2015). (PPT) (PDF)
  • Property Directed Polyhedral Abstraction, January 2015, VMCAI 2015. (PPT)
  • Synthesizing Bit-Precise Safe Invariants, April 7, 2014, TACAS 2014. (PPT)
  • Verifying Programs by Evolving (Under)-Approximations, April 5, 2014, Third workshop on Valid Strategies for Software Evolution (VSSE). (PPT)
  • Vinta: Verification with INTerpolation and Abstract Interpretation, August 1, 2013, Bell Labs. (PPT)
  • Trust in Formal Methods Toolchains, July, 2013, VeriSure: Verification and Assurance. (PDF) (PPT)
  • Vinta: Combining Model Checking and Abstract Interpretation, June 4, 2013, Microsoft Research. (Video) (PPT)
  • UFO: From Underapproximations to Overapproximations and Back!, May, 2013, CMACS Seminar, Carnegie Mellon University. (PDF) (PPT)
  • UFO: Verification with Interpolationa and Abstract Interpretation, March, 2013, Software Verification Competition (SV-COMP 2013). (PDF) (PPT)
  • Static Analysis of Real Time Embeded Systems with REK, January 31, 2013, Certification: Theories and Tools, Dagstuhl Seminar 13051. (PDF) (PPT)
  • VINTA: Verification with INTerpolation and Abstract interpetation, January 24, 2013, Università della Svizzera Italiana (PDF) (PPT)
  • From Under-approximations to Over-approximations and Back!, August 6, 2012, Microsoft Research (Video)
  • Time-Bounded Analysis of Real-Time Systems, September 10, 2012, Laboratoire d'Informatique Algorithmique: Fondements et Applications (LIAFA), Université Paris Diderot - Paris 7 (PDF) (PPT)
  • From Under-approximations to Over-approximations and Back!, May 2012, Università della Svizzera Italiana (PDF) (PPT)
  • BOXES: Abstract Domain of Boxes, January 28, 2011, University of Iowa, Colloquium (PDF) (PPT)
  • BOXES: A Symbolic Abstract Domain of Boxes, September 16, 2010, Static Analysis Symposium (PDF) (PPT)
  • Supporting Construction, Analysis, and Understanding of Software Models, April 20, 2006, Microsoft Research (Video)