Organizers  Giorgio Delzanno  DISI, University of Genova, Italy Sandro Etalle  U. Twente, The Netherlands Maurizio Gabbrielli  DSI, University of  Bologna, Italy   Program Committee Alessandro Armando  DIST, University of  Genova, Italy Radhia Cousot École Polytecnique, France Thierry Massart  U. Libre de Brussels, Belgium Catuscia Palamidessi Penn State University, USA Frank Pfenning  Carnegie Mellon University, USA Andreas Podelski Max-Planck-Institut, Germany Sriram Rajamani  Microsoft Research, USA Jean-Francois Raskin U. Libre Brussels, Belgium Important Dates Deadline for submissions:        May 15, 2002 Notification:        June 4, 2002 Final papers due:         June 24, 2002 Workshop date:         July 27, 2002

Motivations and Goals The huge increase in interconnectivity we have witnessed in the last decade has boosted the development of systems which are often large-scale, distributed, time-critical, and possibly acting in an unreliable or malicious environment. Furthermore, software and hardware components are often mobile, and have to interact with a potentially arbitrary number of other entities. These systems require solid formal techniques for their verification and analysis. In this respect, computational logic plays an increasingly important role, both providing formal methods for proving system's correctness and tools - e.g. using techniques like constraint programming and theorem proving - for verifying their properties. In addition, computational logic is gaining importance as tool for the specification of these systems. For instance, one can think at the specification, in a form of temporal logic, of a communication protocol. Such specification offers the advantage that one can reason about it using formal methods, and at the same time it is often easily executable by rewriting it into a logic-based programming language. The first edition of SAVE 2001 took place as a one-day satellite event of ICLP/CP 2001 in Paphos, Cyprus.  The technical program constisted of an invited talk and seven paper presentations covering problems related to security, real time systems, simulation and performance evaluation, and general purpose verification techiques (all papers are available on line in the here). The aim of this new edition is to bring together researchers interested in the use of computational logic as a tool for the specification, analysis and validation of systems, with particular emphasis on (but not restricted to) emerging technologies like World Wide Web and e-commerce, (protocols for) smart cards and mobile telephony, wireless technology, control and real-time systems, open and distributed systems. Topics The topics of interest include but are not limited to: Specification languages and rapid prototyping: Logic programming and its extensions First-order, constructive, modal and temporal logic Constraints Type theory Analysis: Abstract interpretation Program analysis and transformation Validation: Simulation and testing Deductive methods Model checking Theorem proving The preferred issues include, but are not limited to: Mobility: specification and verification of mobile code. Security: e.g. specification and verification of security protocols. Interaction, coordination, negotiation, communication and exchange on the Web. Open and Parameterized Systems. Publication The proceedings of the workshop will be published a technical report.  We are planning a journal special issue  of the two editions of SAVE (01 and 02): a selection of the workshops papers will be invited for submitting a full version to it. Program All sessions take place in auditorium 8. SAVE's program is also available with abstracts or side by side with other meetings. 09:00-10:30  Session 1 09:00   Joost-Pieter Katoen, U Twente, The Netherlands Invited talk: Model checking birth and death 09:45   Natasha Sharygina and James C. Browne, U Texas-Austin, USA Model checking large-scale software via abstraction of loop transitions 10:30-11:00  Refreshments 11:00-12:30  Session 2 11:00   Alessandro Armando and Pasquale De Lucia, U Genova, Italy Symbolic model-checking of linear programs 11:45   Pierluigi Ammirati, U Genova, Italy; Giorgio Delzanno, U Genova, Italy; Pierre Ganty, U Brussels (Libre), Belgium; Gilles Geeraerts, U Brussels (Libre), Belgium; Jean-François Raskin, U Brussels (Libre), Belgium; and Laurent Van Begin, U Brussels (Libre), Belgium Babylon: An integrated toolkit for the specification and verification of parameterized systems 12:30-14:00  Lunch 14:00-15:30  Session 3 14:00   Alessandro Armando, U Genova, Italy Invited talk: An overview of the AVISS project 14:45   B. Aziz and G. W. Hamilton, Dublin City U, Ireland A privacy analysis for the π-calculus: The denotational approach 15:30-16:00  Refreshments 16:00-17:30  Session 4 16:00   Fabio Martinelli, CNR Pisa, Italy Symbolic partial model checking for security analysis 16:45   R. Corin and Sandro Etalle, U Twente, The Netherlands An improved constraint-based system for the verification of security protocols