You are in : Home » Results & submissions » Select UOA » 11 - Computer Science and Informatics » View submission: Queen Mary University of London » Outputs » Detail

Output details

11 - Computer Science and Informatics

Queen Mary University of London

Return to search Previous output Next output

Output 0 of 0 in the submission

Article title

Applications of real number theorem proving in PVS

Type

D - Journal article

DOI

10.1007/s00165-012-0232-9

Title of journal

Formal Aspects of Computing: applicable formal methods

Article number

Volume number

Issue number

First page of article

993

ISSN of journal

0934-5043

Year of publication

2013

URL

http://link.springer.com/article/10.1007/s00165-012-0232-9

Number of additional authors

Additional information

<07>A new application of verification to automating and generalising the Nichols plots used in practical control engineering. It is implemented in a novel way, solving decision problems by combining the automatic theorem prover PVS and the computer algebra system Maple. This solves a challenge posed by Qinetiq (Colin O'Halloran <colin_o_halloran@hotmail.com>), who funded a pilot, and were partners on a subsequent EPSRC grant. Led to a collaboration between Martin's group and Intel (John Harrison <johnh@ecsmtp.pdx.intel.com>), in which the decision procedure were extended in papers by Arthan, Harrison and Solovay.

Interdisciplinary

Cross-referral requested

Research group

None

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract