Reliably Secure Software Systems (RS3) –
DFG Priority Programme 1496
The second annual meeting of RS3 took place from 9th to 12th of October 2012. It was the first annual meeting in the second funding period. On October 9th and 10th the projects presented their current status and the next steps of RS3 were planned. This part of the meeting was directly followed by a two-day staff meeting on October 11th and 12th. The staff meeting was intended for work on RS3-wide, common topics . The meeting took place in Munich.
Members of the scientific advisory board were invited to attend:
09.10.2012 (9.00am) -10.10.2012 (5.00pm).
Members of the Friends of RS3 (FoRS3) were invited to attend:
09.10.2012 (9.00am) -10.10.2012 (5.00pm).
Principal investigators of RS3 projects were invited to attend:
09.10.2012 (9.00am) -10.10.2012 (6.00pm).
Doctoral and post-doctoral researchers in RS3 projects were invited to attend:
09.10.2012 (9.00am) - 12.10.2012 (6.00pm).
The meeting took place at:
Technische Universität München
Fakultät für Informatik
Boltzmannstr. 3
85748 Garching
You can find details how to reach the location on this page.
During the annual meeting the projects presented their progress. The discussion sessions revealed possibilities for further collaborations. During the staff meeting the doctoral and post-doctoral researchers identified and worked on common topics in the reference scenarios and project clusters.
The schedule gives an overview of the meeting.
Abstract:
In earlier work, we developed a variant of permission-based separation logic that is particularly suited to reason about multithreaded Java programs with dynamic thread creation and termination, and reentrant locks. This talk discusses how within the context of the VerCors project, we extend this approach to make it suitable to specify and verify concurrent data structures. In particular, we will discuss the following topics:
- a natural generalisation of the lock specification approach to other synchronisation primitives;
- the use of histories to describe functional behaviour of concurrent data structures; and
- specification and verification of lock-free data structures. We will also discuss the architecture of the tool set supporting our approach. Finally, we will sketch our initial ideas how the approach also can be used in a software security context.
The RS3 dinner took place on Tuesday evening at the Hacker Haus. It was generously sponsored by Siemens AG.
We met at the subway station Garching Forschungszentrum to go to the Hacker Haus together by subway. In order to prevent jams at the vending machine you could already buy a "Tageskarte München XXL" earlier on that day. This should also be cheaper than buying individual tickets for that day.
IMPORTANT: In Munich will be the Expo-Real fair at the same time as our annual meeting. Please book your Hotels well in advance!
We reserved a quota in the following three Hotels:
For more information (especially passwords to book a room from the quota) have a look at our Wiki (login required) or send an email to assistant at spp-rs3.de.
If you have further questions regarding the annual meeting, please do not hesitate to contactassistant at spp-rs3.de.