(12- or 24-unit Honours or Masters project)
This project explores the use of generative AI to construct formal abstractions of concrete program implementations — ideally multithreaded ones — that are amenable to formal analysis via model checking or interactive theorem proving. The student will apply a chosen GenAI workflow to a target program, produce such an abstraction, and critically assess whether the abstraction is faithful to the original.
Background
Formal verification, whether by model checking (SPIN, CBMC, …) or by developments in proof assistants such as Isabelle/HOL or HOL4, typically begins with an abstraction of the system under analysis. Constructing such an abstraction is notoriously difficult: too concrete and the analysis does not scale, too coarse and the property of interest is lost. Classical techniques such as predicate abstraction and counterexample-guided abstraction refinement (CEGAR) automate parts of this process for restricted settings, but real-world verification still relies heavily on hand-crafted models, particularly for concurrent code where shared state and interleaving make the abstraction step delicate. Recent large language models exhibit a notable ability to read, explain, and translate code across formalisms, which raises the possibility of using GenAI to construct verification-ready abstractions directly from concrete implementations. Whether such generated abstractions soundly and faithfully approximate the source code is, however, an open question.
Scope
The project will select a small but non-trivial multithreaded program and use a chosen GenAI workflow to produce an abstraction suitable for a specific verification backend such as SPIN/Promela, or an Isabelle/HOL development. The student will then investigate the faithfulness of the generated abstraction: does it preserve the safety and liveness properties of interest, and does it spuriously rule out or admit behaviours? The project is designed as a case study; a larger-scope version will distil the case study into a general method, with a view to a longer-term goal of certifying generated abstractions, for example by emitting a refinement relation that can be discharged in a proof assistant.
References
- E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, Counterexample-Guided Abstraction Refinement, CAV 2000, LNCS 1855, Springer.
- S. Graf, H. Saïdi, Construction of Abstract State Graphs with PVS, CAV 1997, LNCS 1254, Springer.
- C. Baier, J.-P. Katoen, Principles of Model Checking, MIT Press, 2008.
- L. Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, Addison-Wesley, 2002.
- G.J. Holzmann, The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley, 2003.