AOSD
2012
ACM
12 years 7 months ago
2012
ACM
In this work we consider specification and compositional verification for interference detection when several aspects are woven together under joint-weaving semantics without re...
IJAIT
2006
13 years 11 months ago
2006
We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligatio...
FMSD
2006
13 years 11 months ago
2006
We define a cones and foci proof method, which rephrases the question whether two system specifications are branching bisimilar in terms of proof obligations on relations between ...
CORR
2008
Springer
13 years 11 months ago
2008
Springer
We describe an extension to the TLA+ specification language with constructs for writing proofs and a proof environment, called the Proof Manager (PM), to checks those proofs. The ...
ASM
2008
ASM
14 years 1 months ago
2008
ASM
The ingredients of typical model based development via refinement are re-examined, and some well known frameworks are reviewed in that light, drawing out commonalities and differen...
ASM
2008
ASM
14 years 1 months ago
2008
ASM
Event-B is a formal modelling method which is claimed to be suitable for diverse modelling domains, such as reactive systems and sequential program development. This claim hinges o...
ASM
2010
ASM
14 years 2 months ago
2010
ASM
Abstract. Software development in B and Event-B generates proof obligations that have to be discharged using theorem provers. The cost of such developments therefore depends direct...
MPC
1995
Springer
14 years 3 months ago
1995
Springer
We want to prove \automatically" that a program is correct with respect to a set of given properties that is a speci cation. Proofs of speci cations contain logical parts and ...
CAV
1993
Springer
14 years 3 months ago
1993
Springer
Abstract. This paper presents a scalable approach to reasoning formally about distributed algorithms. It uses results about I O automata to extract a set of proof obligations for s...
ESOP
2010
Springer
14 years 4 months ago
2010
Springer
Abstract. The hiding of internal invariants creates a mismatch between procedure specifications in an interface and proof obligations on the implementations of those procedures. T...