TPLP Special Issue on Verification

[Sandro.Etalle at cwi.nl]

			TPLP Special Issue on

     Specification, Analysis and Verification of Reactive Systems
	  http://www.cs.utwente.nl/~etalle/specialissue.html

			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 specification,
analysis and verification.

In this respect, computational logic plays an increasingly important
role. Concerning the specification aspect, one can think for instance
at the specification, in 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. In
addition, Computational logic plays a fundamental role by providing
formal methods for proving system's correctness and tools - e.g. using
techniques like constraint programming and theorem proving - for
verifying their properties.

This special issue is inspired to the ICLP workshops on
"Specification, Analysis and Verification of Emerging technologies
(SAVE)" that took place during iclp 2001 and iclp 2002. Nevertheless,
submission is open to everyone.

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:

    * Security: e.g. specification and verification of security protocols.
    * Mobility: specification and verification of mobile code.
    * Interaction, coordination, negotiation, communication and exchange on the Web.
    * Open and Parametrized Systems.

SUBMISSIONS:

Only electronic submission can be accepted. Please send your
contribution in pdf or PostScript format to giorgio at disi.unige.it.

DATES:

Deadline for submission: November 15, 2003
Notification: May 1, 2003
Revised paper due: October 1, 2004
Publication: 2005

Authors of submitted papers are encouraged to post their articles at
CoRR, thereby helping timely distribution of the scientific works.


EDITORS
	
- Giorgio Delzanno, University of Genova, Italy, 
  http://www.disi.unige.it/person/DelzannoG/

- Sandro Etalle, University of Twente and CWI Amsterdam, the
  Netherlands, http://www.cs.utwente.nl/~etalle/

- Maurizio Gabbrielli, University of Bologna, Italy,
  http://www.cs.unibo.it/~gabbri/

ABOUT TPLP

Theory and Practice of Logic Programming (TPLP, see
http://uk.cambridge.org/journals/tlp/ and
http://www.cwi.nl/projects/alp/TPLP/index.html) is published by the
Cambridge University Press (http://uk.cambridge.org/), and is the sole
official journal of the Association for Logic Programming
(http://www.cwi.nl/projects/alp).