Verification and Computational Logic
VCL'2000
London, UK, July 27 - 28, 2000
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
Thursday 27th of July (afternoon) and
Friday 28th of July (whole day) in conjunction with
CL'2000 in London
(July 24 - 29).
You can register for the workshop either by registering for the entire
CL'2000 conference
or by sending an e-mail to the contact person
(mal@ecs.soton.ac.uk).
Topics:
We did solicit (extended) abstracts
and selected presentations from these
submissions. Abstracts in 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: May 20, 2000 (EXTENDED !)
- Notification of acceptance/rejection: June 6, 2000
- Final papers due: July 17, 2000
Proceedings:
We will bring out a proceedings containing the extended abstracts
as a Southampton University Technical Report. We will also maintain
a web site with the text of the extended abstracts, and links to
authors' web pages and the full papers.
Currently we do not plan to bring out a formal proceedings.
If there is sufficient interest at the workshop, we will invite
full papers to be published as a volume in ENTCS or LNCS.
Organization:
Workshop Organizers:
Contact Person:
Invited Speakers:
Program Committee:
- Julian Bradfield,
University of Edinburgh, UK
- Saumya Debray,
University of Arizona, USA
- Javier Esparza,
TU München, Germany
- Laurent
Fribourg,
ENS Cachan, France
- Michael Leuschel,
University of Southampton, UK
- Francesca Levi,
University of Pisa, Italy
- Thierry Massart,
University of Brussels, Belgium
- Faron Moller,
Uppsala University, Sweden
- Andreas Podelski,
Max Planck Institute Saarbrücken, Germany
- C.R. Ramakrishnan,
SUNY Stony Brook, USA
- Ulrich Ultes-Nitsche,
University of Southampton, UK
- Pierre Wolper,
University of Liège, Belgium
Accepted Papers
- Verification of Communicating Processes in the Event of Interface
Difference
Jonatha Burton, Maciej Koutny
- Well-Typed Programs are not Wrong
Pierre Derensart, Jan-Georg Smaus
- On-the-fly optimized model checking under the symbolic approch
Khalil Ajami
- Fair Model Checking of Abstractions
Dennis Dams, Rob Gerth, Orna Grumberg
- A Rewriting Prolog Semantics
M. Kulas
- Verification of Petri net properties in CLP
Guy A. Narboni
- Weakly Continuation-Closed Abstraction can be Defined on Trace Reductions
Ulrich Ultes-Nitsche, Simon St-James
- A Finite Covering Tree for Analysing Entropic Broadcast Protocols
Alain Finkel, Jerome Leroux
- LTL Model Checking of CSP by Refinement
Andrew Currie, Michael Leuschel, Thierry Massart
The
workshop programme
can be found here and
he
online proceedings
can be found here.
Other Information and Pointers