Proof Automation (2025 Fall)

Topics

The focus is on proof automation, primirally in proof assistants. More specifically, we read papers on the following topics:

• Automation for separation logic (esp. Iris, and deductive provers like Viper)
• Decision procedures for specialised theories and premise selection
• Integration with external automatic provers

Format

• We meet to discuss papers every other week.
• There will normally be one person leading each meeting, who will present two or three related papers on a common topic, and lead the discussion.
• The presenter is supposed to prepare the presentation assuming that other participants have only read the abstract and introduction of the papers.
• The content of the presentation should be high-level, with emphasis on the user perspective. For instance, what the technologies are capable of and what their limitations are.
• The form of the presentation is flexible. It can be, for instance, slides, whiteboard, a demonstration of the artifact, or any combination thereof.
• A running instance of the artifact, if available, is useful for discussion where participants may explore the tool together.
• At the end of each meeting, we will decide who is going to present which papers for the next time.
• The specific time and location for each meeting is in the schedule below.

Suggested papers

Separation logic

1. Automated and Foundational Verification of Low-Level Programs (Part I), Sammler. PhD Thesis 2023.

2. Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris, Mulder et al. PLDI'22.

3. Unification for Subformula Linking under Quantifiers, Mulder et al. CPP'24.

4. Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq, Spies et al. PLDI'24.

5. Inductive Synthesis of Inductive Heap Predicates, Yang and Sergey. OOPSLA'25.

6. Raven: An SMT-Based Concurrency Verifier, Gupta et al. CAV'25.

7. Veil: A Framework for Automated and Interactive Verification of Transition Systems. CAV'25.

8. Viper: A Verification Infrastructure for Permission-Based Reasoning, Müller et al. VMCAI'16

9. Fifteen Years of Viper, Eilers et al. CAV'25.

10. Verification Algorithms for Automated Separation Logic Verifiers, Eilers et al. CAV'24.

Specialised theories

11. BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs, Zhu et al. OOPSLA'2022.

12. Interactive Bit Vector Reasoning using Verified Bitblasting, Böving et al. OOSPLA'25.

… Other specialised theories

Decision procedures and tactics

13. Hammering towards QED, Blanchette et al. Journal of Formalized Reasoning, 2015.

14. Lightweight relevance filtering for machine-generated resolution problems, Meng and Paulson. Journal of Applied Logic, 2009.

15. Extending Sledgehammer with SMT Solvers, Blanchette et al. Journal of Automated Reasoning, 2011.

16. Hammer for Coq: Automation for Dependent Type Theory, Czajka and Kaliszyk. Journal of Automated Reasoning, 2018.

17. Practical proof search for Coq by type inhabitation, Czajka. IJCAR'20.

18. Aesop: White-Box Best-First Proof Search for Lean, Limperg and From. CPP'23.

19. Lean-auto: An Interface between Lean 4 and Automated Theorem Provers, Qian et al. CAV'25.

20. Canonical for Automated Theorem Proving in Lean, Norman et al. ITP 25

21. Automated Discovery of Tactic Libraries for Interactive Theorem Proving, Xin et al. OOPSLA'25.

… AI-assisted approaches

Schedule

• When: every other Wednesday, 9:30-11:00
• Where: Nygaard 297
• Organizer: Zongyuan Liu