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

Output details

11 - Computer Science and Informatics

University of York

Return to search Previous output Next output

Output 11 of 139 in the submission

Article title

A UTP semantics for Circus

Type

D - Journal article

DOI

10.1007/s00165-007-0052-5

Title of journal

Formal Aspects of Computing

Article number

Volume number

Issue number

1-2

First page of article

ISSN of journal

0934-5043

Year of publication

2009

URL

http://link.springer.com/article/10.1007%2Fs00165-007-0052-5

Number of additional authors

Additional information

<08>Originality: The first mechanisation of a major UTP language semantics in a theorem prover, showing that the UTP approach does scale up to cope with sophisticated modelling languages. Rigour: Mechanisation carried out in ProofPower, an industrial-strength HOL theorem prover with very high levels of assurance of soundness. Significance: Central paper in the definition of Circus: with many citations. There are more than 100 Circus papers with collectively more than 2,000 citations and 20 doctorates. The EU FP7 COMPASS project is based partly on the results of this paper, with a budget of more than 4M euros and 40 researchers.

Interdisciplinary

Cross-referral requested

Research group

A - High Integrity Systems Engineering

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract