Applications of Formal Methods to
Control Theory and Dynamical Systems

June 23, 2018
Carnegie Mellon University
Organizer: Jeremy Avigad


This workshop was concerned with uses of formal methods to reason about systems that evolve over time. These can be modeled as continuous, discrete, or hybrid dynamical systems with various types of associated mathematical structure. An important domain of application is engineering and control theory, toward the design of systems that are safe, robust, and efficient.

Workshop participants represented a range of perspectives. They came from academe, industry, and government research, with background in mathematics, computer science, and engineering. They brought expertise in interactive theorem proving, automated reasoning, and numerical methods. The goal of the workshop was to develop a better shared understanding of the practical and theoretical problems, as well as the theory and tools that can be used to address them.

This workshop was supported by grant FA9550-18-1-0325 from the Air Force Office of Scientific Research. It was held in Baker Hall 336B. The opinions and results in the talks do not necessarily reflect the views of the AFOSR.


9:00 - 9:45 Cyril Cohen, Formalization Techniques for Asymptotic Reasoning in Classical Analysis
9:45 - 10:30 Soonho Kong, Real Problems on the Road
coffee break
11:00 - 11:45 Nima Roohi, Robustness as a Remedy for Model Checking Cyber-Physical Systems
11:45 - 12:30 Anthony Narkawicz, Applied Nonlinear Arithmetic in PVS
1:30 - 2:15 Valentin Blot, SMTCoq: Bringing Automation from SMT Solvers to Coq
2:15 - 3:00 Ivan Papusha, Affine Multiplexing Networks
coffee break
3:30 - 4:15 Jacek Cyranka, Rigorous Numerics and Computer Assisted Proofs for Dynamical Systems
4:15 - 5:00 Jeremy Avigad, Formal Methods in Analysis: Plans and Prospects


Jeremy Avigad (Carnegie Mellon)
Seul Baek (Carnegie Mellon)
Valentin Blot (Paris-sud)
Jasmin Blanchette (Vrije Universiteit Amsterdam)
Mario Carneiro (Carnegie Mellon)
Cyril Cohen (Inria Sophia Antipolis)
Katherine Cordwell (Carnegie Mellon)
Jacek Cyranka (University of California, San Diego)
Georges Gonthier (Inria Saclay)
Thomas Hales (University of Pittsburgh)
John Harrison (Amazon Web Services)
Favonia (Kuen-Bang Hou) (Institute for Advanced Studies)
Johannes Hölzl (Vrije Universiteit Amsterdam)
Soonho Kong (Toyota Research Institute)
Robert Y. Lewis (Vrije Universiteit Amsterdam)
Anthony Narkawicz (NASA)
Paula Neeley (Portland State University, Carnegie Mellon)
Tobias Nipkow (Technical University of Munich)
Ivan Papusha (Johns Hopkins)
Zesen Qian (Carnegie Mellon)
Nima Roohi (University of Pennsylvania, University of California at San Diego)
William Simmons (University of Pennsylvania)
Alexey Solovyev (independent software developer)
Sebastian Ullrich (Karlsruhe Institute of Technology)
Josef Urban (Czech Institute of of Informatics, Robotics and Cybernetics)
Scott Viteri (Massachusetts Institute of Technology)
Bohua Zhan (Technical University of Munich, Chinese Academy of Sciences)