Projects per year
Abstract / Description of output
We explore uses of a link we have constructed between the KeYmaera hybrid systems theorem prover and the MetiTarski proof en gine for problems involving special functions such as sin, cos, exp, etc. Transcendental functions arise in the specification of hybrid systems and often occur in the solutions of the differential equations that govern how the states of hybrid systems evolve over time. To date, formulas ex changed between KeYmaera and external tools have involved polynomi als over the reals, but not transcendental functions, chiefly because of the lack of tools capable of proving such goals.
Original language  English 

Title of host publication  NASA Formal Methods 
Subtitle of host publication  6th International Symposium, NFM 2014, Proceedings 
Editors  Julia Badger, Kristin Rozier 
Publisher  SpringerVerlag GmbH 
Pages  188202 
Number of pages  15 
ISBN (Electronic)  9783319062006 
ISBN (Print)  9783319061993 
DOIs  
Publication status  Published  2014 
Publication series
Name  Lecture Notes in Computer Science 

Publisher  Springer 
Volume  8430 
ISSN (Print)  03029743 
ISSN (Electronic)  16113349 
Fingerprint
Dive into the research topics of 'Verifying Hybrid Systems Involving Transcendental Functions'. Together they form a unique fingerprint.Projects
 1 Finished
Profiles

Paul Jackson
 School of Informatics  Senior Lecturer, Director of Institute
 Laboratory for Foundations of Computer Science
 Foundations of Computation
Person: Academic: Research Active