Sciweavers

VSTTE
2005
Springer
13 years 10 months ago
An Overview of Separation Logic
After some general remarks about program verification, we introduce separation logic, a novel extension of Hoare logic that can strengthen the applicability and scalability of pro...
John C. Reynolds
VSTTE
2005
Springer
13 years 10 months ago
Decision Procedures for the Grand Challenge
Abstract. The Verifying Compiler checks the correctness of the program it compiles. The workhorse of such a tool is the reasoning engine, which decides validity of formulae in a su...
Daniel Kroening
VSTTE
2005
Springer
13 years 10 months ago
Abstraction of Graph Transformation Systems by Temporal Logic and Its Verification
Mitsuharu Yamamoto, Yoshinori Tanabe, Koichi Takah...
VSTTE
2005
Springer
13 years 10 months ago
Verifying Design with Proof Scores
: Verifying design instead of code can be an effective and practical approach to obtaining verified software. This paper argues that proof scores are an attractive method for ver...
Kokichi Futatsugi, Joseph A. Goguen, Kazuhiro Ogat...
VSTTE
2005
Springer
13 years 10 months ago
Reasoning about Object Structures Using Ownership
Abstract. Many well-established concepts of object-oriented programming work for individual objects, but do not support object structures. The development of a verifying compiler r...
Peter Müller
VSTTE
2005
Springer
13 years 10 months ago
Automatic Verification of Strongly Dynamic Software Systems
Nurit Dor, John Field, Denis Gopan, Tal Lev-Ami, A...