Constructive Methods and Formal Verification in Analysis
Abstract
This project aimed to develop logical and formal methods to verify and support reasoning and formal methods in analysis, as well as applications to control theory and dynamical systems. For the first two years, the project was based on three distinct but interrelated centers. First, the project contributed libraries, reasoning procedures, and infrastructure around the interactive theorem proving system, Lean. These included additions to the library for topology and analysis, a reflected reasoning procedure for Presburger arithmetic, and a package for defining inductive and coinductive data types. We also contributed to the library for dynamical systems in the Isabelle theorem prover, including a proof of the Poincare-Bendixson theorem and properties of the Laplace transform. Second, the project has extended the use of a logical framework known as differential dynamic logic and the KeYmaera X theorem prover, a system for verifying claims about hybrid systems. In particular, the project developed capabilities to extract fully verified code from specifications, ensuring that software running in safety-critical contexts behaves as intended. This includes improved tactics for reasoning about Taylor models, implemented state of the art data structures and algorithms (including Taylor model flow pipes and preconditioning techniques), and developed novel means of extracting certificates from these computations that allow complete verification of the results, and the integration of the CakeML verified compiler with a formalization of KeYmaera X in the Isabelle theorem prover. Finally, the project made use of a formal logical framework known as homotopy type theory, and extensions that make use of modal operators. These are intended to model cohesive aspects of geometric structures, for example, to mediate between set-theoretic, topological, and differential aspects of such structures. After the first two years, the project was descoped and focused on the first two centers.
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 31, 2022
- Accession Number
- AD1230396
Entities
People
- Jeremy Avigad
Organizations
- Carnegie Mellon University