Blogs (61) >>
Mon 16 Jul 2018 17:45 - 18:15 at Hanoi - Session 3

Society nowadays relies heavily on software, which makes verifying the correctness of software crucially important. Various verification tools have been proposed for this purpose, each focusing on a limited set of tasks, as there are many different ways to build and reason about software. This paper discusses two case studies from the VerifyThis2018 verification competition, worked out using the VerCors verification toolset. Interestingly, these case studies are sequential, while VerCors specialises in reasoning about parallel and concurrent software. This paper elaborates on our experiences of using VerCors to verify sequential programs. The first case study involves specifying and verifying the behaviour of a gap buffer; a data-structure commonly used in text editors. The second case study involves verifying a combinatorial problem based on Project Euler problem #114. We find that VerCors is well capable of reasoning about sequential software, and that certain techniques to reason about concurrency can help to reason about sequential programs. However, the extra annotations required to reason about concurrency bring some specificational overhead.

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