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. 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 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, Hybrid Systems, Real-Time and Distributed systems etc.

• SAVE accepted papers
• SAVE program
• Participant list for SAVE

Topics

• 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

• 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 infinite-state systems.
• Real-time systems.

Workshop Webpage with more detailed Information

Publication

Instructions for authors

Please send your submission as a Postscript or PDF file to: giorgio@disi.unige.it

The paper must not exceed 15 pages, and must contain a cover page with: title, name and addresses of the authors, abstract and keywords. Please prepare the manuscript using LaTex article style, single column, 12.2cm x 19.3cm text area.

Invited speakers

• Alessandro Armando, U Genova, Italy
  An overview of the AVISS project
• Joost-Pieter Katoen, U Twente, The Netherlands
  Model checking birth and death

Organizers

• Giorgio Delzanno <giorgio@disi.unige.it>, U Genova, Italy
• Sandro Etalle <etalle@cwi.nl>, U Twente, The Netherlands
• Maurizio Gabbrielli <gabbri@cs.unibo.it>, U Bologna, Italy