VERIFICATION -- THEORY & PRACTICE
Festschrift celebrating Zohar Manna's 64th
Birthday
Proceedings of Symposium
Taormina, Italy
June 29-July 4, 2003
Contents
(Drafts---Not for Distribution)
- Martín Abadi, K. Rustan
M. Leino: A Logic of Object-Oriented Programs
- Rajeev Alur: Formal Analysis of
Hierarchical State Machines
- Saddek Bensalem, Susanne Graf, Yassine Lakhnech: Abstraction as the Key for Invariant Verification
- Dines Bjørner: Domain
Engineering: A "Radical Innovation" for Software and Systems
Engineering? A Biased Account
- Egon Börger: The ASM Ground
Model Method as a Foundation of Requirements Engineering
- Manfred Broy: A Functional Calculus for Specification
and Verification of Nondeterministic Interactive Systems
- Domenico Cantone, Eugenio G. Omodeo, Jacob T. Schwartz,
Pietro Ursino: Notes from the Logbook of a
Proof-Checker's Project
- Edmund Clarke, Helmut Veith: Counterexamples
Revisited: Principles, Algorithms, Applications
- Hubert Comon-Lundh, Ralf Treinen: Easy
Intruder Deductions
- Patrick Cousot: Verification by Abstract Interpretation
- Luca de Alfaro: Games and
mu-Calculus: From Discrete to Quantitative Solutions
- Nachum Dershowitz, Jay
Jayasimha, Seunjoon Park: Bounded Fairness
- Alfredo Ferro, Rosalba Guigno, Alfredo Pulvirenti: Efficient Boundary Values Generation in General
Metric Spaces for Software Component Testing
- Thomas A. Henzinger,
Ranjit Jhala, Rupak Majumdar, Marco
A. A. Sanvido: Extreme Model Checking
- Gérard Huet: Automata Mista
- Shmuel Katz, Marcelo Sihman: Aspect
Validation Using Model Checking
- Vijay Chandru, Jean-Louis Lassez: Qualitative
Theorem Proving in Linear Constraints
- Nazareno Aguirre, Tom Maibaum: Some
Institutional Requirements for Temporal Reasoning on Dynamic
Reconfiguration of Component Based Systems
- R. De Nicola, G. Ferrari, Ugo Montanari, R. Pugliese, E.
Tuosto: A Formal Basis for Reasoning on
Programmable QoS
- Ben C. Moszkowski: A
Hierarchical Completeness Proof for Propositional Temporal Logic
- Krishna Palem: Proof as Experiment:
Probabilistic Computation from a Thermodynamic Perspective
- Elsa Gunter, Doron Peled: Unit
Checking: Symbolic Model Checking for a Unit of Code
- Dusko Pavlovic, Peter Pepper, Doug Smith: Colimits for Concurrent Collectors
- Amir Pnueli, Tamarah Arons: TLPVS:
A PVS-Based LTL Verification System
- Enrico Marzano, Angelo Montanari, Alberto Policriti: Binary Extensions of S1S and the Composition
Method
- Erika Ábrahám, Frank S. de Boer, Willem-Paul
de Roever, Martin Steffen: A Compositional
Operational Semantics for JavaMT
- Bill Scherlis, J. Reif
- Sriram Sankaranarayanan, Henny
Sipma, Zohar Manna: Petri-net Analysis
using
Invariant Generation
- Orna Kupferman, Nir Piterman, Moshe
Y. Vardi: Fair Equivalence Relations
- Jean Vuillemin: Digital Algebra and Circuits
- Richard Waldinger, Peter Jarvis, Jennifer Dungan: Program Synthesis for Multi-Agent Question
Answering
- Calogero G. Zarba: Combining Sets
with Elements