Output details
11 - Computer Science and Informatics
University of Edinburgh
Output title
Formal Verification of Web Services Composition Using Linear Logic and the pi-calculus
Type
E - Conference contribution
Name of conference/published proceedings
2011 IEEE Ninth European Conference on Web Services
Volume number
-
Issue number
-
First page of article
31
ISSN of proceedings
-
Year of publication
2011
Number of additional authors
1
Additional information
<11> Originality: This is the first mechanization of various aspects of the proof-as-processes paradigm in a proof-assistant.
Significance: This is a general framework for the systematic verification of web-services composition. The end result is not only a formally verified proof of the composition, with an associated guarantee of correctness, but also an 'executable' pi-calculus statement describing the composition in process-algebraic terms.
Rigour: The framework is rigorously formalised within the HOL Light theorem prover. The paper was published in a leading peer-reviewed conference on web-services, with an acceptance rate of 24%.
Interdisciplinary
-
Cross-referral requested
-
Research group
A - Centre for Intelligent Systems & their Applications
Citation count
3
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
