Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Automated Reasoning: Formal Verification with LISA
This lecture introduces the Lab for Automated Reasoning and Analysis, focusing on formal verification using the LISA proof assistant. Topics include formal mathematical proofs, proof assistants like Coq and Isabelle, and recent work on the OCBSL Equivalence Checker. The lecture covers the development of LISA in Scala, its application in logic, set theory, and program correctness, and the algorithm for checking equivalence of propositional formulas. The OCBSL word problem's decidability in log-linear time and reduction to normal form are discussed, highlighting its efficiency and predictability in practice.