Formal Techniques for Java-like Programs (FTfJP)

Date:12 June.
Room: Conference 9.

Organizers:

  • Wei-Ngan Chin (co-Chair and primary contact), National U Singapore
  • Aquinas Hobor (co-Chair), National U Singapore
  • Sophia Drossopoulou, Imperial College, UK
  • Susan Eisenbach, Imperial College, UK
  • Gary T. Leavens, U Central Florida, USA
  • Peter Müller, ETH Zürich, Switzerland
  • Arnd Poetzsch-Heffter, U Kaiserslautern, Germany
  • Erik Poll, Radboud U Nijmegen, The Netherlands

Website: http://www.comp.nus.edu.sg/~ftfjp

Formal techniques can help analyze programs, precisely describe program be- havior, and verify program properties. Newer languages such as Java, C# and Scala provide good platforms to bridge the gap between formal techniques and practical program development, because of their reasonably clear semantics and standardised 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 object-oriented 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

FTfJP Program

Tuesday, 12 June
10:00–11:00 Invited Tutorial: Tom Van Cutsem - AmbientTalk: Modern Actors for Modern Networks - (slides)
11:00–11:15 Break
11:15–12:15 Session 1

Corecursive Featherweight Java
Davide Ancona, Elena Zucca
University of Genova

Encoding Featherweight Java with Assignment and Immutability using The Coq Proof Assistant
Julian Mackay1, Hannes Mehnert2, Alex Potanin1, Lindsay Groves1, Nicholas Cameron3
1Victoria University of Wellington, 2Denmark IT University of Copenhagen, 3New Zealand, Mozilla Corporation

12:15–13:30 Lunch
13:30–14:30 Keynote: Jens Palsberg - Featherweight X10: a core calculus for async-finish parallelism
14:30–14:45 Tea Break
14:45–15:45 Session 2

A type system for regular expressions
Eric Spishak, Werner Dietl, Michael D. Ernst
University of Washington

Verifying the reflective visitor pattern
Ben Horsfall, Nathaniel Charlton, Bernhard Reus
University of Sussex
15:45–16:00 Break
16:00–17:00 Session 3

Verifying Backwards Compatibility of Object-Oriented Libraries Using Boogie
Yannick Welsch, Arnd Poetzsch-Heffter
University of Kaiserslautern

Verification Games: Making Verification Fun!
Werner Dietl, Stephanie Dietzel, Michael D. Ernst, Nat Mote, Brian Walker, Seth Cooper, Timothy Pavlik, Zoran Popovic
University of Washington

Workshop Keynotes

AmbientTalk: Modern Actors for Modern Networks

Tom Van Cutsem

Dawn's picture

We introduce AmbientTalk, a dynamic, object-oriented, distributed programming language.AmbientTalk focuses primarily on the domain of mobile peer-to-peer applications, which are becoming more and more widespread in the wake of smartphone platforms such as iOS and Android. AmbientTalk runs on Android, and can be thought of as a scripting language for that platform. We will discuss AmbientTalk~Rs roots and devote special attention to its concurrent and distributed language features, which are founded on the actor model. Next, we will showcase the language by explaining a peer-to-peer application. We show how resilient mobile applications can be constructed with familiar building blocks like objects and messages, but also in what way these building blocks have to be adapted to fit the characteristics of mobile networks.

FTfJP
Time: June 12
Room: Conference 9

Tom Van Cutsem is a researcher at the Vrije Universiteit Brussel, Belgium. He finished his PhD in 2008 on the topic of AmbientTalk, a distributed object-oriented scripting language for mobile phones. Since 2010, he serves on the ECMAScript standardization committee, where he designed the Javascript Proxy API in close collaboration with Mark S. Miller (Google).

Featherweight X10: a core calculus for async-finish parallelism

Jens Palsberg

Dawn's picture

We present a core calculus with two of X10's key constructs for parallelism, namely async and finish. Our calculus forms a convenient basis for type systems and static analyses for languages with async-finish parallelism. For example, we present a type system for context-sensitive may-happen-in-parallel analysis, along with experimental results of performing type inference on 13,000 lines of X10 code. Our analysis runs in polynomial time and produces a low number of false positives, which suggests that our analysis is a good basis for other analyses such as race detectors. Our calculus is also a good basis for tractable proofs of correctness. For example, we give a one-page proof of the deadlock-freedom theorem of Saraswat and Jagadeesan, and we prove the correctness of our type system.

FTfJP
Time:  June 12
Room:  Conference 9

Jens Palsberg is Professor and Chair of Computer Science at the University of California, Los Angeles. He is the editor-in-chief of ACM Transactions of Programming Languages and Systems and a member of the editorial board of Information and Computation.