Personal tools
You are here: Home Events Paul Jackson: Better real arithmetic provers for hybrid systems verification

Paul Jackson: Better real arithmetic provers for hybrid systems verification

What
When Sep 18, 2012
from 01:00 PM to 02:00 PM
Add event to calendar vCal
iCal

This talk gives an overview of ongoing work exploring how proof
techniques for problems involving real arithmetic and transcendental
functions can be enhanced and better used in the formal verification
of hybrid systems.  The work focusses on verification in the KeYmaera
hybrid systems theorem prover (http://symbolaris.com/info/KeYmaera.html).
Proofs in KeYmaera make frequent use of calls to auxiliary reasoning
services that prove or refute conjectures involving formulas over
real-valued expressions.  We are investigating how services provided
by tools such as MetiTarski or RAHD could improve over current service
providers.

The work is part of the AutoPolyFun project. See

  http://www.cl.cam.ac.uk/~lp15/Grants/AutoPolyFun/

Collaborators include Andrew Sogokon, Grant Passmore and Larry Paulson. 

Document Actions