10th Workshop on
|Program Verification (Session chair: Tobias Wrigstad)|
|9:00 - 9:30||Jan Smans, Bart Jacobs and Frank Piessens. Implicit Dynamic Frames|
|9:30 - 10:00||Romain Bardou. Ownership, Pointer Arithmetic and Memory Separation|
|10:00 - 10:30||Dave Cunningham, Susan Eisenbach and Sophia Drossopoulou. Lock Inference Proven Correct|
|Types (Session chair: Atsushi Igarashi)|
|10:30 - 11:00||Alexander Summers, Peter Müller and Sophia Drossopoulou. A Universe-Type-Based Verification Technique for Mutable Static Fields and Methods|
|11:00 - 11:30||Stefan Wehr and Peter Thiemann. Subtyping Existential Types|
|11:30 - 12:00||Coffee break|
|Formal Models and extensions of Java-like languages (Session chair: Elvira Albert)|
|12:00 - 12:30||John Boyland. An Operational Semantics including ``Volatile'' for Safe Concurrency|
|12:30 - 13:00||Massimo Bartoletti, Pierpaolo Degano, Roberto Zunino, Gabriele Costa and Fabio Martinelli. Securing Java with Local Policies|
|13:00 - 13:30||Tetsuo Kamina and Tetsuo Tamai. Flexible Object Adaptation for Java-like Languages|
|13:30 - 15:30||Lunch break|
|Program Analysis (Session chair: Anindya Banerjee)|
|15:30 - 16:00||Elvira Albert, Puri Arenas, Samir Genaim and German Puebla. Dealing with Numeric Fields in Termination Analysis of Java-like Languages|
|16:00 - 16:30||Rok Strniša. Fixing the Java Module System, in Theory and in Practice|
|16:30 - 17:00||Samir Genaim and Fausto Spoto. Constancy Analysis|
Formal techniques can help analyze programs, precisely describe program behavior, and verify program properties. Newer languages such as Java and C# provide good platforms to bridge the gap between formal techniques and practical program development, because of their reasonably clear semantics and standardized libraries. Moreover, these languages are interesting targets for formal techniques, because the novel paradigm for program deployment introduced with Java, with its improved portability and mobility, opens up new possibilities for abuse and causes concern about security.
Work on formal techniques and tools for programs and work on the formal underpinnings of programming languages themselves naturally complement each other. This workshop aims to bring together people working in both these fields, on topics such as:
Submissions must be in English and are limited to 10 pages using LNCS style (excluding bibliography). Notice that we explicitly also encourage the submission of short papers (of 4 - 6 pages, especially for the ``exciting ideas'' session). Papers must be submitted electronically via Easy Chair.
A PC member, other than the chair(s), may be an author or co-author on any paper under consideration but will be excluded from any evaluation or discussion of the paper, and will get access to reviews of the paper(s) only in the same manner and time as other authors.
If you wish to attend the workshop, but are not an author, PC member or organizer, please ask the organizers via an email to Marieke Huisman.
Informal proceedings will be made available to workshop participants. There will be no formal publication of papers.
We intend to invite selected papers for a special journal issue as a follow-up to the workshop, as has been done for some previous FTfJP workshops.
Last modified: June 17th, 2008Marieke.Huisman@sophia.inria.fr