[PT] MoVeLog'05: workshop on Computational logic, Mobile Code Safety, Program Verification

*************** APOLOGIES FOR MULTIPLE POSTING **************

************ SUBMISSION DEADLINE EXTENDED TO JUL 10 ********

                           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 reasoning about 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
     * Verification Condition Generation
     * Type Systems for mobile calculi and verification
     * Proof Checking
     * Applications to Mobile Code Safety and Program Verification using
       the following tools:
           o Static Analysis
           o Model Checking
           o Theorem Proving
           o Constraint Systems
     * New formal systems for verification
     * Algorithms and Cryptography Questions related to the above topics


SUBMISSIONS:

Submitted papers must be in PostScript or PDF, no longer than 10 pages
in LNCS format, to be presented in ~20 minutes. 
They must consist of original, relevant and 
previously unpublished 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 commits one 
of the authors to its presentation at the 
conference.

To submit a paper, please send the paper in PS or PDF format to the
email address:
           
movelog05-submissions-fc2yyuIZbynPvaDv0MAzMN7lo5+wdyHW@xxxxxxxxxxxxxxxx
You should receive a confirmation mail.

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


IMPORTANT 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 and UPM, Spain)
  Julio Mariño (UPM, Spain)
  Dale Miller (École Polytechnique, INRIA Futurs, France)
  Gopalan Nadathur (University of Minnesota, USA)
  *Alwen Tiu (LORIA, Nancy, France)
  Mike Whalen (University of Minnesota, USA)

  (*)Program co-chairs

WORKSHOP ORGANIZING COMMITTEE:

   James Lipton, (workshop coordinator)
   Wesleyan University

   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