A Constraint Oriented Proof Methodology based on Modal Transition Systems
AbstractIn this paper, we present a constraint-oriented state-based proof methodology for concurrent software systems which exploits compositionality and abstraction for the reduction of the verification problem under investigation. Formal basis for this methodology are Modal Transition Systems allowing loose state-based specifications, which can be refined by successively adding constraints. Key concepts of our method are projective views, separation of proof obligations, Skolemization and abstraction. The method is even applicable to real time systems
How to Cite
Larsen, K. G. (1994). A Constraint Oriented Proof Methodology based on Modal Transition Systems. BRICS Report Series, 1(47). https://doi.org/10.7146/brics.v1i47.21595
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.