14 citations · 23 across the 8 of their papers we have counts for
4 papers · 1 filter
Object-Level Reasoning with Logics Encoded in HOL Light
Petros Papapanagiotou, Jacques Fleuriot
We present a generic framework that facilitates object level reasoning with logics that are encoded within the Higher Order Logic theorem proving environment of HOL Light. This inv…
The Boyer-Moore Waterfall Model Revisited
Petros Papapanagiotou, Jacques Fleuriot
In this paper, we investigate the potential of the Boyer-Moore waterfall model for the automation of inductive proofs within a modern proof assistant. We analyze the basic concepts…
Correct by Construction Resource-based Process Composition
Petros Papapanagiotou, Jacques Fleuriot
The need for rigorous process composition is encountered in many situations pertaining to the development and analysis of complex systems. We discuss the use of Classical Linear Lo…
A theorem proving framework for the formal verification of Web Services Composition
Petros Papapanagiotou, Jacques D. Fleuriot
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 enabl…