TPLP Special Issue: Specification Analysis and Verification of Reactive Systems
Subject: TPLP Special Issue: Specification Analysis and Verification of Reactive Systems
From: Giorgio Delzanno <email@example.com>
Date: Mon, 28 Apr 2003 15:01:48 +0200
Organization: DISI University of Genova
User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.0.2) Gecko/20021120 Netscape/7.01
TPLP Special Issue on
Specification Analysis and Verification of Reactive Systems
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
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.
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 Type theory
o Abstract interpretation
o Program analysis and transformation
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.
Deadline for submission: November 15, 2003
Notification: May 1, 2004
Revised paper due: October 1, 2004
Authors of submitted papers are encouraged to post their articles at
CoRR, thereby helping timely distribution of the scientific works.
* Giorgio Delzanno, University of Genova, Italy, firstname.lastname@example.org
* Sandro Etalle, University of Twente and CWI Amsterdam, the
* Maurizio Gabbrielli, University of Bologna, Italy, email@example.com