Verifying Hybrid Systems Involving Transcendental Functions

Paul Jackson, Andrew Sogokon, James Bridge, Lawrence Paulson

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)peer-review

Abstract

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 languageEnglish
Title of host publicationNASA Formal Methods
Subtitle of host publication6th International Symposium, NFM 2014, Proceedings
EditorsJulia Badger, Kristin Rozier
PublisherSpringer
Pages188-202
Number of pages15
ISBN (Electronic)978-3-319-06200-6
ISBN (Print)978-3-319-06199-3
DOIs
Publication statusPublished - 2014

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume8430
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'Verifying Hybrid Systems Involving Transcendental Functions'. Together they form a unique fingerprint.

Cite this