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 Jan (GMT-07:00) Tijuana, Baja California change

10:30 - 12:00: CPP 2018 - Verifying Programs and Systems at Museum A
Chair(s): Natarajan ShankarSRI International, USA
CPP-201810:30 - 11:00
Antal Spector-Zabusky, Joachim BreitnerUniversity of Pennsylvania, Christine RizkallahUniversity of Pennsylvania, USA, Stephanie WeirichUniversity of Pennsylvania, USA
CPP-201811:00 - 11:30
Damien RouhlingUniversity of Côte d'Azur, France
CPP-201811:30 - 12:00
Christian DoczkalCNRS, France, Joachim BardSaarland University, Germany