[Prev][Next][Index][Thread]

TPLP Special Issue: Specification Analysis and Verification of Reactive Systems

TPLP Special Issue on

Specification Analysis and Verification of Reactive Systems

http://wwwhome.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 homonymous ICLP workshops 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:
          o Logic programming and its extensions
          o First-order, constructive, modal and temporal logic
          o Constraints
          o Type theory
    * Analysis:
          o Abstract interpretation
          o Program analysis and transformation
    * Validation:
          o Simulation and testing
          o Deductive methods
          o Model checking
          o 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.


Dates:

Deadline for submission: November 15, 2003
Notification: May 1, 2004
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, giorgio@disi.unige.it
    * Sandro Etalle, University of Twente and CWI Amsterdam, the
      Netherlands, etalle@cs.utwente.nl
    * Maurizio Gabbrielli, University of Bologna, Italy, gabbri@cs.unibo.it