Publications

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

DBLP » Google Scholar »

Talks

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

• Verifying Verified Code. October 23, 2023. Invited talk at the 15th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2023), Ames, Iowa, USA (PPT) (PDF)
• Program Verification with Constrained Horn Clauses. April 12, 2023. Invited talk at Florida State University (PPT) (PDF) (IPYNB)
• Program Verification with Constrained Horn Clauses. August 10, 2022. Invited talk at 34th International Conference on Computer-Aided Verification (CAV 2022) (PPT) (PDF) (YouTube)
• Science, Art, and Magic of Constrained Horn Clauses. September 6, 2019. 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2019) (PPT) (PDF) (IPYNB) (IPYNB2)
• Machine Learning and Invariant Synthesis. August 28, 2019. Waterloo ML + Security + Verification Workshop (PPT) (PDF)
• Quantified Solutions for Constrained Horn Clauses. July 13, 2019. The Best of Model Checking -- Workshop in Honor of Orna Grumberg (PPT) (PDF)
• The Curse of Interpolation. May 20, 2019. ANDREI-60: Automating New-Era Deductive Reasoning Event in Iberia (PPT) (PDF)
• Quantifiers on Demand. October 9, 2018. 16th International Symposium on Automated Technology for Verification and Analysis (AVTA 2018) (PPT) (PDF)
• Spacer: Model Checking in the land of Theorem Provers, September 2018. Coverif Workshop on Combining Abstract Interpretation and Constraint Programming at Centre International de Rencontres Mathématiques. (PPT) (PDF)
• Algorithmic Logic-based Verification, August 2018. International Summer School Marktoberdorf on Engineering Secure and Dependable Software Systems (PPT) (PDF)
• Discovering Universally Quantified Solutions for Constrained Horn Clauses, July 13, 2018. The International Workshop on Satisfiability Modulo Theories (PPT) (PDF)
• Solving Constrained Horn Clauses with SMT. Invited lecture at International Summer School on Satisfiability, Satisfiability Modulo Theories, and Automated Reasoning, 2018 (PPT) (PDF)
• 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)

Teaching

• Fall 2023, ECE 653, Software Testing, Quality Assurance, and Maintenance, University of Waterloo
• Fall 2023, ECE 351, Compilers, University of Waterloo
• Fall 2022, ECE 351, Compilers, University of Waterloo
• Winter 2022, ECE 453 / CS 447 / CS 647, Software Testing, Quality Assurance, and Maintenance, University of Waterloo
• Winter 2022, ECE 650, Methods and Tools for Software Engineering, University of Waterloo
• Fall 2021, ECE 351, Compilers, University of Waterloo
• Winter 2021, ECE 453 / CS 447 / CS 647, Software Testing, Quality Assurance, and Maintenance, University of Waterloo
• Fall 2020, ECE 650, Methods and Tools for Software Engineering, University of Waterloo
• Winter 2020, ECE 351, Compilers, University of Waterloo
• Winter 2020, ECE 453 / CS 447 / CS 647, Software Testing, Quality Assurance, and Maintenance, University of Waterloo
• Fall 2019, ECE750t29, Automated Program Verification, University of Waterloo
• Fall 2019, ECE 650, Methods and Tools for Software Engineering, University of Waterloo
• Winter 2019, ECE 453 / CS 447 / CS 647, Software Testing, Quality Assurance, and Maintenance, University of Waterloo
• Fall 2018, ECE750t29, Automated Program Verification, University of Waterloo
• Winter 2018, ECE 453 / CS 447, Software Testing, Quality Assurance, and Maintenance, University of Waterloo
• Winter 2018, ECE 653, Software Testing, Quality Assurance, and Maintenance, University of Waterloo
• Fall 2017, ECE 650, Methods and Tools for Software Engineering, University of Waterloo
• Winter 2017, ECE 653, Software Testing, Quality Assurance, and Maintenance, University of Waterloo
• Spring 2014, 15–414/614, Bug Catching: Automated Program Verification, Carnegie Mellon University
• Fall 2012, 15–414/614, Bug Catching: Automated Program Verification, Carnegie Mellon University
• Fall 2011, 15-414, Bug Catching: Automated Program Verification and Testing, Carnegie Mellon University

Service

2018

• PC: ICSE, TACAS, CAV

2017

• PC: SAS, ANT, TMPA, SAC-SVT, SPIN, NFM, PSI, SYNASC, FMCAD, VSTTE.

2016

• PC: POPL, TACAS, SAC-SVT, VMCAI, VSSE (Chair), CAV (ERC), HCVS, NFM, FM, SYNASC, FMCAD.

2015

• PC: TACAS, SV-COMP, FM, CAV, VSTTE (Chair), HCVS (Chair), CAV-ART (Chair), ASE, PSI, SYNASC, TAPAS.

2014

• PC: SV-COMP, ASE, ASE-TOOLS (Chair), NFM, SPIN, FormaliSE, PSI, WING, VSTTE, GandALF, ICMS (Session Chair).

2013

• PC: SV-COMP, CAV, SAS, FORTE/FMOODS, ASE, VSTTE, FormaliSE.
• Reviewer:
  • Conferences: TACAS, SPIN, ICTAC
  • Formal Methods in System Design
  • Theoretical Computer Science
  • Software Tools for Technology Transfer