------------------------------------------------------------------------
Our apologies if you receive multiple copies.
-------------------------------------------------------------------------
CALL for PAPERS
-------------------------------------------------------------------------
2nd International Workshop on Verification, Model Checking and
Abstract Interpretation
(In association with SAS'98 and PLILP/ALP'98 .)
---------------------------------------------------------------------------
The 2nd Workshop on Verification, Model Checking and Abstract
Interpretation follows the successful ILPS post-conference workshop held
in Port Jefferson, NY, USA, October 1997.
Motivations and Goals
-------------------
Program verification aims at proving that programs meet their
specifications, i.e., that the actual program behaviour coincides with the
desired one. Model checking is a specific approach to the verification of
temporal properties of reactive and concurrent systems, which has proven
successful in the area of finite-state programs. Abstract interpretation is
a method for designing and comparing semantics of programs, expressing
various types of programs properties. In particular, it has been
successfully used to infer run-time program properties that can be valuable
to optimize programs.
Clearly, among these three methods, there are similarities concerning their
goals and their domains of applications.
Furthermore, while much research has been performed in the area of abstract
interpretation of logic programs, connections between model checking and
logic programming have hardly been investigated as yet; at the same time it
seems that there may be interesting directions in this area. Besides model
checking of (concurrent) logic programs, one may also think of the use of
specialized constraint (logic) solvers to tackle the model checking problem.
The main goal of the workshop is that of enhancing cross-fertilization
among these areas and in this way to clarify their relationships.
Papers are solicited, reporting on the use of techniques for deriving or
proving properties of programs and more generally of finite dynamic systems.
Contributions examining the relations among the different techniques in the
field of (constraint) logic programming and other programming paradigms,
will be considered particularly interesting. Description of work in
progress is also welcome.
Topics include but are not limited to:
* verification
* model checking
* static analysis
* optimization
* debugging
* tools
At least one author of each accepted abstract is expected to attend the
workshop.
IMPORTANT DATES:
Papers Submission Deadline: 15 June 1998
Notification of acceptance: 15 July 1998
Workshop : 18 September 1998
SUBMISSIONS: Authors are invited to submit an abstract (up to 7 pages) by
e-mail in PostScript format to [EMAIL PROTECTED]
PROCEEDINGS: The proceedings will be available at the conference as a
technical report of the University Ca' Foscari of Venice, Italy.
Selected papers will be published in a special issue of the journal
Computer Languages.
INFORMATION: http://www.dsi.unive.it/~bossi/VMCAI2.html
or mail to: [EMAIL PROTECTED]
Workshop Organizers
Annalisa Bossi (Coordinator) [EMAIL PROTECTED]
University Ca' Foscari di Venezia, Italy.
Agostino Cortesi [EMAIL PROTECTED]
University Ca' Foscari di Venezia, Italy.
Francesca Levi [EMAIL PROTECTED]
University of Pisa, Italy
Program Committee
Krzysztof R. Apt (CWI Amsterdam)
Annalisa Bossi (University Ca' Foscari di Venezia)
Agostino Cortesi (University Ca' Foscari di Venezia)
Yves Deville (Universite Catholique de Louvain)
Gilberto File' (University of Padova)
Gopal Gupta (New Mexico State University)
Francesca Levi (University of Pisa)
Jan Maluszynski (Linkoping University)
Jens Palsberg (Purdue University)
I.V. Ramakrishnan (SUNY Stony Brook)
David Schmidt (Kansas State University)
---------------------------------------------------------------------------
