Sciweavers

APLAS
2010
ACM
13 years 9 months ago
Metric Spaces and Termination Analyses
We present a framework for defining abstract interpreters for liveness properties, in particular program termination. The framework makes use of the theory of metric spaces to defi...
Aziem Chawdhary, Hongseok Yang
IC3
2009
13 years 9 months ago
Verification of Liveness Properties in Distributed Systems
Abstract. This paper presents liveness properties that need to be preserved by Event-B models of distributed systems. Event-B is a formal technique for development of models of dis...
Divakar Yadav, Michael Butler
AMAST
2008
Springer
14 years 1 months ago
Evolving Specification Engineering
Abstract. The motivation for this work is to support a natural separation of concerns during formal system development. In a developmentby-refinement context, we would like to be a...
Dusko Pavlovic, Peter Pepper, Douglas R. Smith
ESEC
1997
Springer
14 years 3 months ago
Verification of Liveness Properties Using Compositional Reachability Analysis
The software architecture of a distributed program can be represented by a hierarchical composition of subsystems, with interacting processes at the leaves of the hierarchy. Compo...
Shing-Chi Cheung, Dimitra Giannakopoulou, Jeff Kra...
PODC
1999
ACM
14 years 3 months ago
Liveness-Preserving Simulation Relations
We present a new approach for reasoning about liveness properties of distributed systems, represented as automata. Our approach is based on simulation relations, and requires reas...
Paul C. Attie
DSN
2000
IEEE
14 years 3 months ago
An Automatic SPIN Validation of a Safety Critical Railway Control System
This paper describes an experiment in formal specification and validation performed in the context of an industrial joint project. The project involved an Italian company working...
Stefania Gnesi, Diego Latella, Gabriele Lenzini, C...
VMCAI
2004
Springer
14 years 4 months ago
Liveness with Invisible Ranking
The method of Invisible Invariants was developed originally in order to verify safety properties of parameterized systems fully automatically. Roughly speaking, the method is based...
Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck
ICICS
2005
Springer
14 years 5 months ago
On the Quest for Impartiality: Design and Analysis of a Fair Non-repudiation Protocol
We design and analyze a simple optimistic fair non-repudiation protocol. Our protocol is considerably simpler and more efficient than current proposals, due mainly to the avoidanc...
J. G. Cederquist, Ricardo Corin, Muhammad Torabi D...
MEMOCODE
2005
IEEE
14 years 5 months ago
Three-valued logic in bounded model checking
In principle, bounded model checking (BMC) leads to semidecision procedures that can be used to verify liveness properties and to falsify safety properties. If the procedures fail...
Tobias Schüle, Klaus Schneider
POPL
2007
ACM
14 years 11 months ago
Proving that programs eventually do something good
In recent years we have seen great progress made in the area of automatic source-level static analysis tools. However, most of today's program verification tools are limited ...
Byron Cook, Alexey Gotsman, Andreas Podelski, Andr...