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
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