Constructive Methods and Formal Verification in Analysis
Abstract
The project will deliver, first, a betterunderstanding of dynamical systems and theoretical tools for reasoning about complex models inanalysis. It will also contribute to the development of two computational tools: Lean, a generalframework for proving and verifying theorems in mathematics, and KeYmaera X, a system designedspecifically for the verification of hybrid systems. These products contribute to the goals ofdesigning computational and mechanical systems that are reliable, efficient, and safe.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Apr 09, 2018
- Source ID
- FA95501810120
Entities
People
- Jeremy Avigad
Organizations
- Air Force Office of Scientific Research
- Massachusetts Institute of Technology
- United States Air Force