POPL 2018 (series) / CPP 2018 (series) / CPP 2018 - The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs /
A Formal Proof in Coq of a Control Function for the Inverted Pendulum
Mon 8 Jan 2018 11:00 - 11:30 at Museum A - Verifying Programs and Systems Chair(s): Natarajan Shankar
Control theory provides techniques to design controllers, or control
functions, for dynamical systems with inputs, so as to grant a particular
behaviour of such a system. The inverted pendulum is a classic system in
control theory: it is used as a benchmark for nonlinear control techniques and
is a model for several other systems with various applications. We formalized
in the {\sc Coq} proof assistant the proof of soundness of a control function for
the inverted pendulum. This is a first step towards the formal verification of
more complex systems for which safety may be critical.
Mon 8 JanDisplayed time zone: Tijuana, Baja California change
Mon 8 Jan
Displayed time zone: Tijuana, Baja California change
10:30 - 12:00 | |||
10:30 30mTalk | Total Haskell is Reasonable Coq CPP Antal Spector-Zabusky , Joachim Breitner University of Pennsylvania, Christine Rizkallah University of Pennsylvania, USA, Stephanie Weirich University of Pennsylvania, USA DOI | ||
11:00 30mTalk | A Formal Proof in Coq of a Control Function for the Inverted Pendulum CPP Damien Rouhling University of Côte d'Azur, France DOI | ||
11:30 30mTalk | Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq CPP DOI | ||