Summer Term 2025
LLMs in Formal Verification
| Event Type: | Seminar |
|---|---|
| Target Group: | Master Computer Science |
| Scope: | 2 SWS / 3 ECTS |
| Events: |
Kickoff:
April t.b.a., 2025, t.b.a. in room t.b.a. (building 50.34) |
| Event Number: | 2400025 |
| ILIAS Course: | t.b.a. |
| Lecturers: |
Prof. Bernhard Beckert |
| Registration: | t.b.a. |
| Allocation of Places: | Topics will be distributed at the kickoff event. Priority will be given on a FCFS basis, considering preferences from registration. |
| Prerequisites: | No formal requirements, but prior experience with program analysis, verification or automated reasoning is helpful. |
| Language: | English |
Subject Area
Our chair specializes in formal methods across a broad spectrum of modern software development. Unfortunately, writing formal specifications, constructing proofs, and verifying real-world programs remain notoriously difficult, time-consuming, error-prone, and expertise-intensive tasks. With the rise of large language models (LLMs), a new research direction has emerged that explores how such models can assist—or even automate—various parts of the verification pipeline.
The goal of this seminar is to explore recent advances at the intersection of large language models (LLMs) and formal methods. We will examine in detail how LLMs are being applied to infer program specifications, synthesize invariants, assist in theorem proving, and repair or generate code with correctness guarantees. Furthermore, we will discuss their role in formalizing natural language requirements and learning effective proof strategies—all with the broader aim of making formal verification more accessible, scalable, and practical.
Tasks
For successful participation in the seminar, each participant is expected to achieve the following:
- Reading Assignment: Independently develop the content of the research topic to be presented (usually based on 1 or 2 papers). You will receive the necessary support in regular meetings with a supervisor.
- Presentation and Discussion: Prepare a 25-min presentation on the topic. After the presentations there will be an in-class discussion (roughly around 20 mins) that every student is expected to attend and participate in.
- Postprocessing: Write a report (7-8 pages, ACM Generic Journal Manuscript format) on the motivation of the research topic, state-of-the-art approaches, identify any shortcomings, write the relevant discussions from the class and mention how this research contributes to the broader landscape.
Slides and Material
- t.b.a.
Topics:
The following list of topics is intended to provide an overview.
If you have any questions about topics or organization, please contact Debasmita Lohar.
1. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs, ICLR 2023
2. Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data, NeurIPS-MATH-AI 2024
1. Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification, CAV 2024
2. Towards Combining the Cognitive Abilities of Large Language Models with the Rigor of Deductive Progam Verification, ISOLA 2024
1. Guiding Enumerative Program Synthesis with Large Language Models, CAV 2024
2. HYSYNTH: Context-Free LLM Approximation for Guiding Program Synthesis, NeurIPS 2024
1. Hybrid Automated Program Repair by Combining Large Language Models and Program Analysis, TOSEM 2024
2. Aligning the Objective of LLM-based Program Repair, ICSE 2025
1. Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?, FSE 2024
2. Can LLMs translate SATisfactorily? Assessing LLMs in Generating and Interpreting Formal Specifications? AAAI 2024
1. LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant Inference, ASE 2024
2. LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling, ASE 2024
...and more to come!