Skip to main content
Pages and Files
CS department homepage
CS faculty meetings
CS talks and visitors
From Communities of Practice to Community Based Decision Making — Case Ericsson
Artificial General Intelligence and AI in Games
Cryptography Reading Group
Cybersecurity Breakfast Talks
Data Systems Group
DeIC offer Sep 2017
Former members of the department (partial list)
Jean Melo PhD
PhD Defense of Jean Melo
Remotely controlled drug delivery with chemical micro-robots.
State of Low-power Wireless Protocols for IoT
Talk Alan Mycroft 9 June 2017
Talk by Alexander Serebrenik on Aug 31, 2017
TALK by Rohit Gheyi on Aug 31, 2017
Add "All Pages"
Talk Marieke Huisman 9 Jun 2017
A Verification Technique for Deterministic Parallel Programs
(University of Twente, Netherlands)
Time: June 9, 10:00
A commonly used approach to develop parallel programs is to augment a sequential program with compiler directives that indicate which program blocks may potentially be executed in parallel. This paper develops a verification technique to prove correctness of compiler directives combined with functional correctness of the program. We propose syntax and semantics for a simple core language, capturing the main forms of deterministic parallel programs. This language distinguishes three kinds of basic blocks: parallel, vectorized and sequential blocks, which can be composed using three different composition operators: sequential, parallel and fusion composition. We show that it is sufficient to have contracts for the basic blocks to prove correctness of the compiler directives, and moreover that functional correctness of the sequential program implies correctness of the parallelized program. We formally prove correctness of our approach. In addition, we define a widely-used subset of OpenMP that can be encoded into our core language, thus effectively enabling the verification of OpenMP compiler directives, and we discuss automated tool support for this verification process.
Joint work with Saeed Darabi and Stefan Blom
talk by Alan Mycroft
will follow directly)
(At 1pm in Auditorium 1 a
PhD defence of Iago Abal
on finding bugs using effect systems will take place.)
help on how to format text
Turn off "Getting Started"