Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Workshop: Verification and Computational Logic
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.
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.