Skip to content

Research at St Andrews

Applications of real number theorem proving in PVS

Research output: Contribution to journalArticle

Author(s)

Hanne Gottliebsen, Ruth Hardy, Olga Lightfoot, Ursula Martin

School/Research organisations

Abstract

Real number theorem proving has many uses, particularly for verification of safety critical systems and systems for which design errors may be costly. We discuss a chain of developments building on real number theorem proving in PVS. This leads from the verification of aspects of an air traffic control system, through work on the integration of computer algebra and automated theorem proving to a new tool, NRV, first presented here that builds on the capabilities of Maple and PVS to provide a verified and automatic analysis of Nichols plots. This automates a standard technique used by control engineers and greatly improves assurance compared with the traditional method of visual inspection of the Nichols plots.

Close

Details

Original languageEnglish
Pages (from-to)993-1016
Number of pages24
JournalFormal Aspects of Computing
Volume25
Issue number6
DOIs
Publication statusPublished - Nov 2013

    Research areas

  • Real number theorem proving, PVS, Maple, Control systems, Test suite, Air traffic control, Higher order theorem proving, Mechanically checked proof

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. THE LAVA PROJECT: A SERVICE BASED APPROACH TO SUPPORTING EXPLORATORY LEARNING

    Getchell, K., Miller, A. H. D., Allison, C., Hardy, R., Sweetman, R. & Crook, V., 1 Oct 2006, IADIS International Conference WWW/Internet. Murcia, Spain

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related by journal

  1. Automating Event-B invariant proofs by rippling and proof patching

    Lin, Y., Bundy, A., Grov, G. & Maclean, E., 2 Feb 2019, In : Formal Aspects of Computing. First Online, 35 p.

    Research output: Contribution to journalArticle

  2. Formal verification of a pervasive messaging system

    Konur, S., Fisher, M., Dobson, S. A. & Knox, S., Apr 2014, In : Formal Aspects of Computing. 26, 4, p. 677-694 18 p.

    Research output: Contribution to journalArticle

ID: 136173416