ECOOP 2015
Sun 5 - Fri 10 July 2015 Prague, Czech Republic

Welcome to the 17th Workshop on Formal Techniques for Java-like Programs

Formal techniques can help analyse programs, precisely describe program behaviour, and verify program properties. 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 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:

  • Language Semantics
  • Specification techniques and languages
  • Verification of program properties
  • Verification logics
  • Dynamic program analysis
  • Static program analysis
  • Type systems
  • Challenge problems and solutions
  • Security

For details of previous workshops, visit http://www.cs.ru.nl/ftfjp/.

You're viewing the program in a time zone which is different from your device's time zone change time zone

Tue 7 Jul

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:05 - 10:15
WelcomeFTfJP at Hluboka I
Chair(s): Rosemary Monahan Maynooth University
10:05
10m
Day opening
Opening
FTfJP

10:15 - 12:15
Session 1FTfJP at Hluboka I
Chair(s): Rosemary Monahan Maynooth University
10:15
30m
Talk
A three-valued type system for true positives detection in Java-like languages
FTfJP
Davide Ancona University of Genova, Federico Frassetto
10:45
30m
Talk
Imperative Objects with Dependent Types
FTfJP
Joana Campos Lasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. Vasconcelos Lasige / Faculty of Sciences, Universidade de Lisboa
11:15
30m
Talk
Foo: A minimal Modern OO Calculus
FTfJP
Prodromos Gerakios National Technical University of Athens, George Fourtounis University of Athens, Yannis Smaragdakis University of Athens
11:45
30m
Talk
Delegation vs Inheritance for Typestate Analysis
FTfJP
Du Li Carnegie Mellon University, Alex Potanin Victoria University of Wellington, Jonathan Aldrich Carnegie Mellon University
12:15 - 12:35
Tool Demonstration 1FTfJP at Hluboka I
Chair(s): Rosemary Monahan Maynooth University
12:15
20m
Other
Why3
FTfJP
Léon Gondelman LRI, Université Paris-Sud
13:45 - 14:45
Session 2FTfJP at Hluboka I
Chair(s): Rosemary Monahan Maynooth University
13:45
30m
Talk
Provably Live Exception Handling
FTfJP
Bart Jacobs iMinds - Distrinet, KU Leuven
14:15
30m
Talk
Run-time Assertion Checking of JML Annotations in Multithreaded Applications with e-OpenJML
FTfJP
Jorne Kandziora University of Twente, Marieke Huisman University of Twente, Christoph Bockisch University of Twente, Marina Zaharieva-Stojanovski University of Twente
14:45 - 15:35
Invited TalkFTfJP at Hluboka I
Chair(s): Rosemary Monahan Maynooth University
14:45
50m
Talk
Verification of Concurrent Software: Java and OpenCL
FTfJP
Marieke Huisman University of Twente
16:00 - 17:30
Session 3FTfJP at Hluboka I
Chair(s): Rosemary Monahan Maynooth University
16:00
30m
Talk
Automatic Verification of Dafny Programs with Traits
FTfJP
Reza Ahmadi University of Tampere, K. Rustan M. Leino Microsoft Research, Jyrki Nummenmaa University of Tampere
16:30
30m
Talk
Conditional Effects in Fine-grained Region Logic
FTfJP
Yuyan Bao University of Central Florida, Gary T. Leavens Central Florida University, Gidon Ernst Augsburg University
17:00
30m
Talk
Regression Verification for Java Using a Secure Information Flow Calculus
FTfJP
Bernhard Beckert Karlsruhe Institute of Technology, Vladimir Klebanov Karlsruhe Institute of Technology, Mattias Ulbrich Karlsruhe Institute of Technology
17:30 - 17:50
Tool Demonstration 2FTfJP at Hluboka I
Chair(s): Rosemary Monahan Maynooth University
17:30
20m
Other
Viper (Verification Infrastructure for Permission-based Reasoning)
FTfJP
Malte Schwerhoff ETH Zurich, Switzerland
17:50 - 18:00
ClosingFTfJP at Hluboka I
Chair(s): Rosemary Monahan Maynooth University
17:50
10m
Day closing
Closing
FTfJP

Call for Papers

Contributions (of up to 6 pages in the ACM 2-column style) are sought on open questions, new developments, or interesting new applications of formal techniques in the context of Java or similar languages. Contributions should not merely present completely finished work, but also raise challenging open problems or propose speculative new approaches. We particularly welcome contributions that simply present suitable topics for discussion at the workshop, or raise issues that you feel deserve the attention of the research community. Examples include future work identified from existing research, potential PhD proposals, and experience reports from case studies/competitions. Contributions will be formally reviewed, for originality, relevance, and the potential to generate interesting discussions.

The workshop will be organized into sessions, each focused on a specific topic, and initiated by a presentation of few related position papers by the respective participants, or the introduction of the specific topic by a single speaker, and followed by discussion. These discussions aim to share common experiences, provide constructive feedback, and build potential research collaborations.

Accepted papers will have the option of being published in the ACM Digital Library. In addition, depending on the nature of the contributions, we may be organizing a special journal issue as a follow-up to the workshop, as has been done for some of the previous FTfJP workshops. Contributions must be in English, in PDF format, and are limited to 6 pages in ACM 2-column style. Papers must be submitted electronically via Easy Chair. All deadlines are at 23:59 American Samoa time (that is, UTC-11).

Submission site: https://easychair.org/conferences/?conf=ftfjp2015 Any PC member, other than the chair, may be an author or co-author on any paper submitted for consideration but will be excluded from any evaluation or discussion of the paper.

Speaker: Marieke Huisman (University of Twente, Netherlands)

Title: Verification of Concurrent Software: Java and OpenCL

Abstract:

This talk presents the VerCors approach to verification of concurrent software. First we discuss why verification of concurrent software is important, but also challenging, and we show how permission-based separation logic allows one to reason about concurrent programs in a thread-modular way. We show how we extend the logic to reason about functional properties of Java programs in a concurrent setting. Further, we also show how the approach is used to reason about kernel programs using the Single Instruction Multiple Data paradigm. Concretely, we illustrate how permission-based separation logic is used to verify functional correctness properties of OpenCL kernels.

Biography:

Marieke Huisman (F) is an Adjoint Professor in the Formal Methods and Tools group at the University of Twente in the Netherlands. She obtained her PhD in 2001 from the University of Nijmegen, Netherlands. Her thesis was about the semantics and verification of sequential Java programs. She spent almost eight years at INRIA Sophia Antipolis, France as a Charg’e de Recherche, working on verification of (in particular concurrent) programs, application-specific security, compositionality and concurrency. In 2008 she joined the University of Twente.

In 2010 she received a personal ERC Starting Grant for the VerCors project on Verification of Concurrent Data Structures. In 2013 she received the Dutch ICT Research award, a unique prize for a scientist, aged 40 years or younger, who carries out innovative research or is responsible for a scientific breakthrough in ICT. In addition, she has been involved in several EU projects, such as CARP, Mobius, VerifiCard.

Registration fees increase on June 6th and again on July 4th. See https://2015.ecoop.org/attending/registration for details.