June 22, Maribor (Slovenia)

12th Workshop on
Formal Techniques for Java-like Programs

Overview

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:

• formal techniques for Java, C#, Scala or similar languages
• specification techniques and interface specification languages
• specification of software components and library packages
• automated checking and verification of program properties,
• verification logics,
• language semantics,
• type systems,
• dynamic linking and loading,
• security.

Draft workshop programme

Tue, June 22, 2010

8:30 - 9:00 Registration

9:00 - 10:30 Session 1: Types (Chair: Adriaan Moors)

• Davide Ancona and Giovanni Lagorio. Complete coinductive subtyping for abstract compilation of object-oriented languages.
• Alexander Summers, Nicholas Cameron, Mariangiola Dezani-Ciancaglini and Sophia Drossopoulou. Towards a Semantic Model for Java Wildcards.
• Marco Servetto and Giovanni Lagorio. Strong exception-safety for Java-like languages.

10:30 - 11:00 Coffee break

11:00 - 12:30 Session 2: Verification (Chair: Frank Piessens)

• Jonas B. Jensen, Lars Birkedal and Peter Sestoft. Modular Verification of Linked Lists with Views via Separation Logic.
• Siavash Soleimanifard, Dilian Gurov and Marieke Huisman. Procedure-Modular Verification of Control Flow Safety Properties.
• Stijn de Gouw, Jurgen Vinju and Frank de Boer. Prototyping a tool environment for run-time assertion checking in JML with Communication Histories.

12:30 - 14:00 Lunch

14:00 - 15:30 Session 3: Aliasing control (chair: Lars Birkedal)

• Filipe Militao, Jonathan Aldrich and Luis Caires. Aliasing control with view-based typestate.
• Leila Silva, David Naumann and Augusto Sampaio. Refactoring and representation independence for class hierarchies.
• Darpan Saini, Joshua Sunshine and Jonathan Aldrich. A Theory of Typestate-Oriented Programming.

15:30 - 16:00 Coffee break

16:00 - 17:00 Invited talk

• Shriram Krishnamurthi, Brown University. Electrifying JavaScript: Static Types for a Dynamic Language
  
  Building a static type system for JavaScript poses interesting challenges. The language has very few dynamic errors that a type system can statically prevent. Programmers make extensive use of control-flow-based typed reasoning. The language's object system is peculiar. Overloading is rampant. Experts feel compelled to write books teaching programmers "the Good Parts".

  I will discuss the design, implementation and evaluation of our static type system for JavaScript. The system features a novel and modular combination of type- and flow-based reasoning that handles idiomatic JavaScript code. It permits the interoperation of typed and untyped code, and enables the use of existing tools such as debuggers. To reduce the annotation burden, we offer a simple yet effective type inference technique. The resulting checker is sound, fast, and runs on JavaScript programs in the wild.

  Joint work with Arjun Guha and Claudiu Saftoiu.

Important dates

Program Committee

Organization