================ DEADLINE EXTENSION: JULY 10! ===============

LAST CALL FOR PAPERS

MoVeLog'05

Mobile Code Safety and Program Verification Using Computational Logic Tools

An ICLP Workshop, Sitges, Spain, Oct. 5, 2005

http://babel.ls.fi.upm.es/movelog05

Computational logic and logic programming in particular can support rich reasoning about programs, proofs, types, and specifications.

Recent breakthroughs in mobile code safety and program verification have brought even more relevance to these tools, especially in the areas of meta-logic proof theory, proof search, static analysis and abstract interpretation, and model checking, even when the object code involved is very far from declarative. Components are needed that can perform such reasoning and the logic programming community is well positioned to provide such components.

Especially promising has been ground-breaking work with proof-carrying-code, a development that shows signs of having widespread applications, and has brought a surprising number of new challenges where computational logic can potentially contribute. It is worth pointing out that the earliest papers in the field made explicit mention of the possible relevance of such formalisms as lambda-prolog and ELF for all phases of the enterprise: generation of verification conditions, formalization of proofs, manipulation of proofs and certificate checking. Since then there have been proposals to combine these approaches with other logic programming frameworks equipped with tools for static analysis and abstract interpretation. While other programming paradigms may also be relevant here, logic programming may have an important edge among other reasons because its basis in declarative principles has led to the development of sophisticated static analysis and abstract interpretation tools."

This workshop is aimed at using computational logic in general and logic programming in particular to support dealing with security, safety, correctness, and mobile code. It aims to bring together researchers in logic programming working in mobile code safety, security, program analysis, and correctness as well as those in related areas of automated deduction (HOL, COQ, NuPRL, ISABELLE etc). Relevant topics include (but are not limited to) the following:

- Protocol analysis and verification - Proof Carrying Code - Logical Frameworks - Type Systems - Static Analysis - Model Checking - Theorem Proving - Proof Checking - Verification Condition Generation - Constraint Systems - New formal systems for verification - Algorithms and Cryptography Questions related to the above topics

Submissions:

Submitted papers must no be longer than 10 pages, to be presented in ~20 minutes. They must consist of original, relevant and previously unpublished sound research results related to any of the topics of the conference.

We also invite submissions of brief expositions of work in progress for a poster session. The length of these papers should be no longer than 4 pages.

At least one author of each paper must register for the conference before the early registration deadline. The acceptance of the paper implies its oral presentation at the conference.

To submit a paper, send an electronic mail to

movelog05-submissions(a)babel.ls.fi.upm.es

You should receive a confirmation mail.

If there is sufficient interest, post-workshop proceedings will be considered.

Dates:

- Paper Submission: July 10. - Notification of Acceptance/Rejection: July 28.

Program Committee:

Bruno Blanchet (ENS, Paris) Gopal Gupta (Univ, of Texas, Dallas, USA) Manuel Hermenegildo (UPM, Spain and Univ. of New Mexico, USA) Danny Krizanc (Wesleyan University, USA) Jim Lipton (Wesleyan University, USA) Julio Mariño (UPM, Spain) Dale Miller (cole Polytechnique, INRIA Futurs, France) Gopalan Nadathur (University of Minnesota, USA) Mike Whalen (University of Minnesota, USA) Alwen Tiu (LORIA, Nancy, France)

Workshop Organizing Committee:

James Lipton, (program co-chair) Wesleyan University

Alwen Tiu, (program co-chair) LORIA, Nancy

Julio Mariño Carballo Technical University of Madrid

Dale Miller Laboratoire d'Informatique, LIX

Manuel Hermenegildo Technical University of Madrid and The University of New Mexico