Projects per year
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 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 | Springer |
Pages | 188-202 |
Number of pages | 15 |
ISBN (Electronic) | 978-3-319-06200-6 |
ISBN (Print) | 978-3-319-06199-3 |
DOIs | |
Publication status | Published - 2014 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 8430 |
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.Projects
- 1 Finished
-
Automatic proof procedures for polynomials and special functions
Jackson, P. (Principal Investigator)
1/11/10 → 28/02/15
Project: Research
Profiles
-
Paul Jackson
- School of Informatics - Senior Lecturer, Director of Institute
- Laboratory for Foundations of Computer Science
- Foundations of Computation
Person: Academic: Research Active