*************** APOLOGIES FOR MULTIPLE POSTING ************** **** FINAL CALL FOR PAPERS: JULY 10 DEADLINE **** 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@babel.ls.fi.upm.es 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) 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