# Paul Jackson: Better real arithmetic provers for hybrid systems verification

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.