Blogs (61) >>
Mon 16 Jul 2018 16:00 - 16:25 at Hanoi - Session 3

Verification projects on industrial code have required reasoning about functional programming constructs in Java 8. In our experience so far, verification of functional programming in practice has needed only simple techniques such as inlining. However, in general functional programming will require reasoning about how the specifications of function objects that are inputs to a method combine to produce output function objects. This paper describes our in-progress experience in adapting prior work (Kassios & Müller) to Java 8, JML, and OpenJML.

Mon 16 Jul

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

16:00 - 18:15
Session 3FTfJP at Hanoi
16:00
25m
Short-paper
Reasoning about Functional Programming in Java and C++
FTfJP
David Cok CEA, LIST, Software Safety and Security Laboratory
Pre-print
16:25
25m
Short-paper
A Formalism for Specification of Java API Interfaces
FTfJP
Davide Ancona University of Genova, Francesco Dagnino DIBRIS, University of Genova, Italy, Luca Franceschini DIBRIS, University of Genova
Pre-print
16:50
25m
Short-paper
Static Latency Tracking with Placement Types
FTfJP
Pascal Weisenburger Technische Universität Darmstadt, Tobias Reinhard Technische Universität Darmstadt, Guido Salvaneschi TU Darmstadt
Pre-print
17:15
30m
Demonstration
Tool demonstration: The VerCors Verification Toolset
FTfJP
Wytse Oortwijn University of Twente, The Netherlands
Pre-print
17:45
30m
Full-paper
An Exercise in Verifying Sequential Programs with VerCors
FTfJP
Sebastiaan Joosten , Wytse Oortwijn University of Twente, The Netherlands, Mohsen Safari University of Twente, The Netherlands, Marieke Huisman University of Twente
Pre-print