A theorem proving framework for the formal verification of Web Services Composition
We present a rigorous framework for the composition of Web Services within a higher order logic theorem prover. Our approach is based on the proofs-as-processes paradigm that enables inference rules of Classical Linear Logic (CLL) to be translated into pi-calculus processes. In this setting, composi...
Main Authors: | Petros Papapanagiotou, Jacques D. Fleuriot |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2011-08-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1108.2348v1 |
Similar Items
-
A combination of geometry theorem proving and nonstandard analysis, with application to Newton's Principia
by: Fleuriot, Jacques Désiré
Published: (1999) -
Formal verification of Matrix based MATLAB models using interactive theorem proving
by: Ayesha Gauhar, et al.
Published: (2021-03-01) -
A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving
by: Yassmeen Elderhalli, et al.
Published: (2019-01-01) -
Formal probabilistic analysis using theorem proving
by: Hasan, Osman
Published: (2008) -
Formal Analysis of Soft Errors using Theorem Proving
by: Sofiène Tahar, et al.
Published: (2013-07-01)