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 (part) 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.

Extending and shifting slightly from the scope of the predecessors (on verification and logic languages) held in the context of past editions of ICLP, the aim of this workshop is to bring together researchers interested in the use of computational logicas 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.

Topics

• Specification languages and rapid prototyping: Logic programming and its extensions; Constructive, modal and temporal logic; Constraints; Type theory
• Analysis: Abstract interpretation; Static analysis
• Validation: Simulation and testing; Deductive methods; Model checking; Theorem proving

• Mobility: specification and verification of mobile code.
• Security: access rights, information flow, and security protocols.
• Interaction, coordination, negotiation, communication and exchange on the Web.
• Open and infinite-state systems.
• Real-time systems.

• Deadline for submissions: August 25, 2001 Expired
• Notification of acceptance/rejection: September 15, 2001.
• Final papers due: October 5, 2001.
• Early registration: October 10, 2001.
• Special rates for accomodation: September 24, 2001.

Technical Program

9.00-10:00
Invited Talk
Specification and  Verification of Non-Repudiation and Fair Exchange Protocols : Let's Play a Game"
 Jean-Francois Raskin (Universite' Libre de Bruxelles)
Slides

10:00-10:30
Time Limited Model Checking
Moreno Falaschi, Alberto Policriti, and Alicia Villanueva
Paper in gzipped ps format
Slides

 11.00-11:30
A Specification Language for Crypto-Protocols based on Multiset Rewriting Dependent Types and Subsorting
Iliano  Cervesato
Paper in gzipped ps format
Slides in gzipped PowerPoint format

 11.30-12:00
Ensuring Security Through Model Checking in a Logical Environment (Preliminary Results)
Marco Bozzano
Paper in gzipped ps format
Slides in gzipped ps format

 12.00-12.30
Formally validated specification of a micro-payment protocol
Patrice Dargenton, Daniel Hirschoff, Pierre Lescanne, and Eric Pommateau
Paper in gzipped ps format
Slides in gzipped pdf format

 14.00-14.30
Combining two approaches for the formal verification of cryptographic protocols
Frederic Oehl, and David Sinclair
Paper in gzipped ps format
Slides

 14.30-15.00
Pi-calculus as a rapid prototyping language for performance evaluation
Francesco Logozzo
Paper in gzipped ps format
Slides in gzipped Corel format

15:00-15:30
Simulation Reduction as Constraint
R Gentilini, Carla Piazza, and Alberto Policriti
Paper in gzipped ps format
Slides in gzipped ps format
 

Instruction for the Authors:

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.
The camera ready version of the paper (LaTex sources, style files, and postscript file) must be sent to
the address giorgio@disi.unige.it by October 5, 2001.
The proceedings will be published in electronic format.
A printed version will be distributed to all participants of the workshop.
 

Registration and Accomodation

Workshop Organizers/PC Chairs:

• Giorgio Delzanno - Dipartimento di Informatica e Scienze dell'Informazione - Universita'  di Genova

e-mail: giorgio@disi.unige.it
 
• Sandro Etalle -  Department of Computer Science- University of Twente and CWI

e-mail: etalle@cs.utwente.nl
 
• Maurizio Gabbrielli - Dipartimento di Matematica ed Informatica - Universita' di Udine

e-mail: gabbri@dimi.uniud.it

• Radhia Cousot, CNRS & École Polytechnique, France
• Giorgio Delzanno, University of Genova, Italy
• Sandro Etalle, University of Twente and CWI, The Netherlands
• Maurizio Gabbrielli, University of Udine, Italy
• Thierry Massart, University of Brussels, Belgium
• Frank Pfenning, Carnegie Mellon University, USA
• Andreas Podelski, Max Planck Institute, Germany
• Sriram Rajamani, Microsoft Research, USA
• Jean-Francois Raskin, University of Brussels, Belgium