The Second International
Workshop on
Verification and Computational Logic
VCL'2001
Florence, Italy, September 4, 2001
Held at the PLI 2001
Symposium
Overview:
The aim of this workshop is to bring together researchers working on
the interplay between verification techniques (e.g., model checking,
reduction, and abstraction) and logic programming techniques (e.g.,
constraints, abstract interpretation, program transformation).
The workshop will be held
Tuesday 4th of September (whole day) at the
PLI 2001
Symposium in Florence
(September 3 - 7).
This workshop is sponsored by
ACM Sigplan.
The
proceedings are now available.
The programme can be found
here.
Topics:
We did solicit abstracts and extended abstracts (guideline:
2-10 pages)
and selected presentations from these
submissions. We encouraged researches to submit work in
progress, and one does not have to submit a full paper.
(We do not want to prevent researchers from submitting
their work to a conference later on.)
Submissions covering the following topics were invited:
- Techniques
- abstraction techniques for verification of
infinite-state systems
- constraint representations
and constraint processing algorithms
for verification
- logic programming approaches to model checking
- program analysis/abstract interpretation approaches to verification
- program transformation/specialization approaches to verification
- state-space reduction techniques for model checking
- Tools
- Case Studies
Additionally, we invited researchers from core verification
areas (model checking/theorem proving) to present their current work.
Important Dates:
- Deadline for submissions: June 20, 2001 (expired)
- Notification of acceptance/rejection: July 11, 2001
- Final papers due: August 15, 2001
- Deadline for early registration at PLI'2001: July 25,
2001
Accepted Papers
-
Dan Ghica
"A Regular-Language Model for Hoare-Style Correctness Statements"
-
Bill Roscoe
"What can you decide about initialised arrays ?"
-
Carla Piazza and Alberto Policriti
"Ackermann Encoding, Bisimulations, and OBDD's"
-
Ranko Lazic, Tom Newcomb, and Bill Roscoe
"On model checking data-independent systems with arrays"
-
Massimo Franceschet and Angelo Montanari
"Towards an automata-theoretic counterpart of combined temporal logics"
-
Baudouin Le Charlier, Sabina Rossi, and Agostino Cortesi
"A Domain for the Abstract Interpretation of
Logic Programs with Dynamic Scheduling"
-
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
"Verifying CTL Properties of Infinite-State Systems
by Specializing Constraint Logic Programs"
-
Michael Leuschel, Laksono Adhianto, Michael Butler,
Carla Ferreira, and Leonid Mikhailov
"Animation and Model Checking of CSP and B using
Prolog Technology"
Proceedings:
The proceedings containing the
abstracts and extended abstracts are available online
as a
Southampton University Technical Report and
will be made available within the
ACM Digital Library.
There will also be a
special issue
of the journal
"Theory and Practice of Logic Programming"
on "verification and computational logic," covering selected
papers from both VCL'2000 and VCL'2001 but open to other submissions
as well.
Organization:
Workshop Organizers/PC Chairs:
Invited Talks:
- Giorgio
Delzanno:
Constraint-based Verification: Techniques
and Applications
- Stefania
Gniesi:
Finite Approximations for
Model Checking Non-finite State Processes
Program Committee:
- Annalisa Bossi,
University of Venezia, Italy
- Javier Esparza,
TU München, Germany
- Alain
Finkel,
ENS Cachan, France
- Ranko Lazic,
University of Warwick, UK
- Baudouin Le
Charlier,
University of Namur, Belgium
- Michael Leuschel,
University of Southampton, UK
- Andreas Podelski,
Max Planck Institute Saarbrücken, Germany
- Maurizio Proietti,
IASI-CNR, Rome, Italy
- C.R. Ramakrishnan,
SUNY Stony Brook, USA
- Jean-Francois Raskin,
University of Brussels, Belgium
- Ulrich Ultes-Nitsche,
University of Southampton, UK
- Pierre Wolper,
University of Liège, Belgium
Contact Person:
Other Information and Pointers