Sciweavers

AOSD
2012
ACM
12 years 1 months ago
A closer look at aspect interference and cooperation
In this work we consider specification and compositional verification for interference detection when several aspects are woven together under joint-weaving semantics without re...
Cynthia Disenfeld, Shmuel Katz
IJAIT
2006
106views more  IJAIT 2006»
13 years 5 months ago
An Empirical Evaluation of Automated Theorem Provers in Software Certification
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...
Ewen Denney, Bernd Fischer 0002, Johann Schumann
FMSD
2006
103views more  FMSD 2006»
13 years 5 months ago
Cones and foci: A mechanical framework for protocol verification
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 ...
Wan Fokkink, Jun Pang, Jaco van de Pol
CORR
2008
Springer
126views Education» more  CORR 2008»
13 years 5 months ago
A TLA+ Proof System
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 ...
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport,...
ASM
2008
ASM
13 years 7 months ago
Model Based Refinement and the Tools of Tomorrow
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...
Richard Banach
ASM
2008
ASM
13 years 7 months ago
On the Purpose of Event-B Proof Obligations
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...
Stefan Hallerstede
ASM
2010
ASM
13 years 8 months ago
Automatic Verification for a Class of Proof Obligations with SMT-Solvers
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...
David Déharbe
MPC
1995
Springer
125views Mathematics» more  MPC 1995»
13 years 9 months ago
Synthesizing Proofs from Programs in the Calculus of Inductive Constructions
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 ...
Catherine Parent
CAV
1993
Springer
108views Hardware» more  CAV 1993»
13 years 9 months ago
Computer-Assisted Simulation Proofs
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...
Jørgen F. Søgaard-Andersen, Stephen ...
ESOP
2010
Springer
13 years 10 months ago
Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions
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...
David A. Naumann, Anindya Banerjee