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 13 of 83 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