Institute of Theoretical Computer Science Institute of
Theoretical Computer Science

Carl-Friedrich-Gauß-Fakultät
Technische Universität Braunschweig
TU Braunschweig Home Team Teaching Research Publications Tools

Concurrency Theory 2014

News

  • On Tuesday, July 29th there will be a meeting in which we talk about the exam content. We meet at 11.30 in Room 34/420.
  • There are no more exam dates available in August. If you still need an exam date, please choose a day from the second exam period. We will preferably schedule exams for September 29th and 30th.
  • The oral exams will take place in the last weeks of August and September. In each of these weeks, we will fix two days for the exams. Please send Reiner an E-Mail telling him your preferred dates and times for your exam in the following periods:
    • 25th August - 29th August
    • 29th September - 2nd October.
  • The tutorials scheduled for June 19th (public holiday) will take place on Monday, June 23rd, starting at 15:30 and 17:15 in 13-305.
  • The axiom ConsistentRFdom was missing from the axiomatic TSO model in the lecture notes. It has been added.
  • The tutorials scheduled for May 29th (public holiday) will take place on Monday, June, 2nd, at 08:15 in 11-222
  • and 17:15 in 13-305.
  • Exercise 4.2 had a bug in the definition of the list predicate (emp was missing).
  • There was a bug in exercise 1.2: the first line must read "... and (P*emp)<=>P". The PDF is now correct.
  • There is some more material on separation logic in the Lecture Notes section.
  • The room for the lecture on tuesdays has been changed to 48-210.
  • The tutorials scheduled for May 1st (public holiday) will take place on Monday, May 5th, starting at 15:30 and 17:00 in 13-305.

Organisation

Dates and rooms:

  • Tuesdays 8:15 - 09:45 in 48-210
  • Wednesdays 13:45 - 15:15 in 46-280
  • Tutorials take place on:
    • Thursdays 15:30 - 17:00 in 48-462.
    • Thursdays 17:15 - 18:45 in 48-462.
  • Tutorials start in the second week.
  • The lecture in KIS and in the Module Handbook.

Exams:

We decide in the first two weeks whether there will be written or oral exams. To be admitted, you have to fulfil the following requirements:
  1. 60 percent of your exercises have to be marked by a plus.
  2. You have to present some of your exercise solutions on the board .

Lecture Notes

Lecture notes from the 2011/2012 Concurrency Theory lecture can be found here.

Further material on separation logic:

For full citations, see Literature section below.

Further material on TSO-reachability

Exercises

Organisation:

  • Exercises will be made available here (Wednesday evenings).
  • Solutions are due on Tuesdays at noon.
  • Please hand in solutions in groups of 3 to 4 people.
  • The mailbox is in the staircase between buildings 34 and 36, 4th floor, close to the SofTech AG.

Exercise Sheets:

  • Download Exercise Sheet 1 here.
  • Download Exercise Sheet 2 here.
  • Download Exercise Sheet 3 here.
  • Download Exercise Sheet 4 here.
  • Download Exercise Sheet 5 here.
  • Download Exercise Sheet 6 here.
  • Download Exercise Sheet 7 here.
  • Download Exercise Sheet 8 here.
  • Download Exercise Sheet 9 here.
  • Download Exercise Sheet 10 here.
  • Download Exercise Sheet 11 here.
  • Download Exercise Sheet 12 here.
  • Download Exercise Sheet 13 here.
  • Download Exercise Sheet 14 here.
    • This last sheet is optional. There will be no tutorial and it does not count towards the exam requirements.
If you have questions or encounter problems with the exercises, please contact Reiner.

Content

  • Concurrent program logics (extensions of Hoare logic for concurrency)
    • Concurrent separation logic
    • Rely-guarantee
    • RGSep and further logics
  • Weak memory models
    • Sequential consistency
    • TSO (Sparc, x86)
    • PowerPC/ARM
    • C/C++11
    • DRF-Theorem and extensions for different memory models
  • Multi-threaded programs and Petri nets
  • Petri net specific analyses
    • Karp and Miller coverability graphs
    • Invariants
    • Unfoldings + SAT
  • Static networks and lossy channel systems (lcs)
  • Analysis of well-structured transition systems (wsts), with lcs as an example
    • Wsts and Finkel's finite reachability tree
    • Abdulla's backwards algorithm
    • Geeraerts' EEC algorithm
  • Reconfigurable networks and process algebras
  • Analysability
    • Structural stationarity, depth, and breadth
    • Well-structuredness in bounded depth
    • Turing completeness in bounded breadth
  • Bisimilarity, an alternative correctness notion
  • Analysis and its limits
    • Fixed points in the finite
    • Communication freedom and prime elements in the infinite
    • Undecidability following Jančar

Literature

The lectures will be based upon the following books and articles. Most of them are available online, the remaining ones can be found in the library.
  • J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Logic in Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on (pp. 55-74). IEEE, 2002. Free version can be found here.
  • P. W. O’hearn. A Primer on Separation Logic (and Automatic Program Verification and Analysis). In Software Safety and Security: Tools for Analysis and Verification 33: 286, 2012 Free version can be found here.
  • L. Priese and H. Wimmel. Petri-Netze. Springer-Verlag, 2003.
  • W. Reisig. Petri nets: An Introduction. Monographs in Theoretical Computer Science. An EATCS Series. Springer-Verlag, 1985.
  • P. H. Starke. Analyse von Petri-Netz-Modellen. Leitfäden und Monographien der Informatik. Teubner, 1990.
  • J. Esparza and M. Nielsen. Decibility issues for Petri nets-a survey. Journal of Information Processing and Cybernetics EIK, 30(3):143-160, 1994. Free version can be found here.
  • J. Esparza. Decidability and complexity of Petri net problems - an introduction. In Lectures on Petri Nets I: Basic Models. Advances in Petri Nets, volume 1491 of LNCS, pages 374-428, Springer-Verlag, 1998. Free version can be found here.
  • J. Esparza and S. Melzer. Verification of safety properties using integer programming: Beyond the state equation. Formal Methods in System Design, 16:159-189, 2000. Free version can be found here.
  • J. Esparza and K. Heljanko. Unfoldings. Monographs in Theoretical Computer Science. An EATCS Series. Springer-Verlag, 2008. Free version can be found here.
  • A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1-2):63-92, 2001. Free version can be found here.
  • G. Geeraerts, J.-F. Raskin, L. Van Begin. Expand, Enlarge and Check: new algorithms for the coverability problem of WSTS. Journal of Computer and System Sciences, 72(1):180-203, 2005. Free version can be found here.
  • P. Abdulla, A. Bouajjani, B. Jonsson. On-the-Fly Analysis of Systems with Unbounded, Lossy Fifo Channels. In Proc. of the 10th International Conference on Computer Aided Verification, CAV, volume 1427 of LNCS, pages 305-318, Springer-Verlag, 1998. Free version can be found here.
  • R. Meyer. Structural Stationarity in the pi-Calculus. PhD thesis, Department of Computing Science, University of Oldenburg, 2008. Free version can be found here.

News

GI-Fachgruppe.
Roland Meyer has been elected as the spokesperson of the GI-Fachgruppe Concurrency Theory.

NETYS 2017.
Locality and Singularity for Store-Atomic Memory Models.  publications

Klausur Theoretische Informatik II.
Die Klausur am 23.03.2017 wird von Herrn Urbat erstellt und umfasst die Inhalte der Vorlesung 2016.

MFCS 2017.
Roland Meyer is a member of the programme committee.

ATVA 2017.
Roland Meyer is a member of the programme committee.

TMPA 2017.
Roland Meyer is a member of the programme committee.

Dr.-Ing. Georgel Calin.
Congratulations on your successful defense!

BCS/CHPC Distinguished Dissertation Award.
The thesis “Verification of Message Passing Concurrent Systems” (by Emanuele D'Osualdo) received the BCS/CHPC Distinguished Dissertation Award in 2016.  PDF

NWPT 2016.
Thread Summaries for Lock-Free Data Structures.  publications

ACSD 2017.
Roland Meyer is a member of the programme committee.

FSTTCS 2016.
Summaries for Context-Free Games.  publications

D-CON 2017.
Roland Meyer will speak at the D-CON workshop.

EATCS Distinguished Dissertation Award.
The thesis “Monoids as Storage Mechanisms” (by Georg Zetzsche) received the EATCS Distinguished Dissertation Award in 2016.  PDF

Marktoberdorf 2016.
Sebastian Wolff was accepted to the Marktoberdorf Summer School.

MEMICS 2016.
Roland Meyer will speak at the MEMICS workshop.

Carl Zeiss.
Our project ArchiV: Architecture-aware Verification has been granted.  research

LICS 2016.
Complexity of Regular Abstractions of One-Counter Languages.  publications

LICS 2016.
First-Order Logic with Reachability for Infinite-State Systems.  publications

UPMARC 2016.
Roland Meyer will speak at the UPMARC summer school.

CONCUR 2017.
Roland Meyer is a co-chair of the conference.

ESOP 2016.
On Hierarchical Communication Topologies in the π-calculus.  publications

FoSSaCS 2017.
Roland Meyer is a member of the programme committee.

Best teaching award SoSe 2015.
Our Bachelor's course Logik received the best teaching award.

ACSD 2016.
Roland Meyer is a member of the programme committee.

VMCAI 2016.
Pointer Race Freedom.  publications

FSTTCS 2015.
What's Decidable about Availability Languages?.  publications

NETYS 2016.
Roland Meyer is a member of the programme committee.

RP 2015.
The Emptiness Problem for Valence Automata or: Another Decidable Extension of Petri Nets.  publications

Best student paper at ICALP 2015.
An approach to computing downward closures.  publications

ACM TECS.
Memory-Model-Aware Testing - a Unified Complexity Analysis.  publications

NETYS 2015.
Antichains for Recursive Program Verification.  publications

CCDP 2015.
Roland Meyer will give an invited talk. More about the workshop can be found  here

FSTTCS 2015.
Roland Meyer is a member of the programme committee.

SKILL 2015.
Roland Meyer is a member of the programme committee. More about the conference can be found  here

MM 2015.
Roland Meyer will give an invited talk. More about the workshop can be found  here

TACAS 2016.
Roland Meyer is a member of the programme committee.

STACS 2015.
Computing downward closures for stacked counter automata.  publications

CONCUR 2015.
Roland Meyer is a member of the programme committee. More about the conference can be found  here

ACSD 2015.
Roland Meyer is a co-chair of the programme committee. More about the conference can be found  here

FASE 2015.
Lazy TSO Reachability.  publications