Last VORACE workshop

20 February 2017
Charles Square Campus of the Czech Technical University in Prague, Czech Republic


The workshop, organized by Didier Henrion and Josef Urban aims at reporting recent achievements in formal verification methods of computer science, with application in theorem proving and optimization of dynamical systems. It is the last workshop of the project called VORACE (Verified fast optimization for embedded control) funded by the French Government Defense Agency (DGA) and managed by the French National Research Agency (ANR).

Date and venue

The workshop takes place on Monday 20 February 2017 in room 14, building E (ground floor on your right hand side when entering the building) on the Charles Square Campus of the Czech Technical University in Prague, Czechia. Please refer to these maps for instructions to reach this building. The campus entrance is restricted to badge holders, so please ask the doorperson to let you in through the electronic gates.


  • 9:00-10:00 - Josef Urban (CIIRC CVUT Prague) - AI and Theorem Proving (see also the following talk)

  • 10:00-11:00 - Eric Feron (Georgia Tech Atlanta) - Validation of convex optimization algorithms and credible implementation for model predictive control

  • 11:30-12:30 - Stefan Ratschan (CS Czech Acad Sci) - Simulation-driven Safety Verification of Dynamical Systems

  • 12:30-14:00 - Lunch break - attendees on their own

  • 14:00-15:00 - Jan Jakubuv (CIIRC CVUT Prague)- BliStrTune: hierarchical invention of theorem proving strategies

  • 15:00-16:00 - Pierre-Loïc Garoche (ONERA Toulouse) - Proving numerical algorithms used in embedded systems -- our experience with theorem provers

  • 16:30-17:30 - Thibault Gauthier (Univ Innsbruck) - TacticToe: Learning to Reason with HOL4 Tactics