huge increase in interconnectivity we have witnessed in the last decade
has boosted the development of systems which are often large-scale,
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.
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.
addition, computational logic is gaining importance as tool for the
specification of these systems. For instance, one can think at the
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.
first edition of SAVE
2001 took place as a one-day satellite event of ICLP/CP 2001. The
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).
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.
The topics of interest include but are not limited to:
The preferred issues include, but are not limited to:
Specification languages and rapid prototyping:
Logic programming and its extensions
First-order, constructive, modal and temporal logic
Program analysis and transformation
Simulation and testing
Mobility: specification and verification of mobile code.
Security: e.g. specification and verification of security protocols.
Interaction, coordination, negotiation, communication and exchange on the
Open and infinite-state systems.
Workshop Webpage with
more detailed Information
The proceedings of the workshop will be published as
technical report. We are planning a journal special issue: a selection
of the workshop papers will be invited for submitting a full version
Please send your submission as a Postscript or PDF file to:
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.