The Second International
Verification and Computational Logic
Florence, Italy, September 4, 2001
Held at the PLI 2001
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
Symposium in Florence
(September 3 - 7).
This workshop is sponsored by
proceedings are now available.
The programme can be found
We did solicit abstracts and extended abstracts (guideline:
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:
Additionally, we invited researchers from core verification
areas (model checking/theorem proving) to present their current work.
- abstraction techniques for verification of
- constraint representations
and constraint processing algorithms
- 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
- Case Studies
- 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,
"A Regular-Language Model for Hoare-Style Correctness Statements"
"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
The proceedings containing the
abstracts and extended abstracts are available online
Southampton University Technical Report and
will be made available within the
ACM Digital Library.
There will also be a
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
Workshop Organizers/PC Chairs:
Constraint-based Verification: Techniques
Finite Approximations for
Model Checking Non-finite State Processes
- Annalisa Bossi,
University of Venezia, Italy
- Javier Esparza,
TU München, Germany
ENS Cachan, France
- Ranko Lazic,
University of Warwick, UK
- Baudouin Le
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
Other Information and Pointers