News
14. April: Die Themen, Paper und weiteres Material wurden ergänzt.
25. März: Der Termin für das Kickoff wurde ergänzt.
16. Februar: Die Informationen auf dieser Seite sind noch vorläufig.
Zeitplan
15.04.2026
Kickoff
um 15 Uhr in IZ 358
05.07.2026
Abgabe der vorläufigen Seminarpaper
per Mail an Natalia Gacek und Jan Grünke
12.07.2026
Abgabe der Reviews
Sie geben das Review zu dem Ihnen zugewiesenen Paper per Mail an Natalia Gacek und Jan Grünke ab und erhalten ein Review für Ihr Paper.
19.07.2026
Finale Abgabe der Seminarpaper
per Mail an Natalia Gacek und Jan Grünke
Organisation
Im Sommersemester 2026 bietet das Institut für Theoretische Informatik ein Seminar an.
- Wöchentliche Talks sind am Mittwoch, um 15:00 Uhr, im Raum IZ 358. Starttermin wird noch bekannt gegeben.
- Das Kickoff-Meeting wird am 15.04.2026 um 15:00 Uhr im Raum IZ 358 stattfinden.
- Beachten Sie das zentrale Anmeldeverfahren für das Seminar.
- Seminarplätze sind begrenzt auf 10 Studenten der Informatik (BA+MA), sowie 10 Studenten des Data Science (MA).
- Um sich vollständig für das Seminar zu registrieren, müssen Sie bis zum 21.04.2026 ein Dokument unterschreiben. Dies können Sie direkt beim Kickoff oder später im Sekretariat (Terminvereinbarung unter a.soleinsky(at)tu-braunschweig.de) tun.
Themen
Die Themen dieses Semesters sind Linearisierbarkeit (Informatik) und Datalog (Data Science).
Folgende Paper stehen zur Wahl:
Manuelle Techniken zum Beweisen von Linearisierbarkeit
- [CAV 2006] Robert Colvin, Lindsay Groves, Victor Luchangco, Mark Moir:
Formal Verification of a Lazy Concurrent List-Based Set Algorithm.
https://doi.org/10.1007/11817963_44 - [POPL 2015] Mike Dodds, Andreas Haas, Christoph M. Kirsch:
A Scalable, Correct Time-Stamped Stack.
https://doi.org/10.1145/2775051.2676963 - [DISC 2018] Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, Sharon Shoham:
Order out of Chaos: Proving Linearizability Using Local Views.
https://doi.org/10.4230/LIPIcs.DISC.2018.23 - [OOPSLA 2020] Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham:
Proving highly-concurrent traversals correct.
https://doi.org/10.1145/3428196 - [PLDI 2013] Hongjin Liang, Xinyu Feng:
Modular verification of linearizability with non-fixed linearization points.
https://doi.org/10.1145/2491956.2462189 - [ESOP 2017] Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew J. Parkinson:
Proving Linearizability Using Partial Orders.
https://doi.org/10.1007/978-3-662-54434-1_24
Automatische Techniken zum Beweisen von Linearisierbarkeit
- [CAV 2007] Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, Eran Yahav:
Comparison Under Abstraction for Verifying Linearizability.
https://doi.org/10.1007/978-3-540-73368-3_49 - [CAV 2010] Viktor Vafeiadis:
Automatically Proving Linearizability.
https://doi.org/10.1007/978-3-642-14295-6_40 - [PLDI 2010] Sebastian Burckhardt, Chris Dern, Madanlal Musuvathi, Roy Tan:
Line-up: a complete and automatic linearizability checker.
https://doi.org/10.1145/1806596.1806634 - [CAV 2013] Cezara Dragoi, Ashutosh Gupta, Thomas A. Henzinger:
Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates.
https://doi.org/10.1007/978-3-642-39799-8_11 - [PLDI 2023] Roland Meyer, Thomas Wies, Sebastian Wolff:
Embedding Hindsight Reasoning in Separation Logic.
https://doi.org/10.1145/3591296
Datalog
Material
Linearisierbarkeit
- Vorlesungsnotizen zu Linearisierbarkeit: Teil 1, Teil 2
- Originalpaper zu Linearisierbarkeit:
Maurice P. Herlihy and Jeannette M. Wing. 1990. Linearizability: a correctness condition for concurrent objects. In TOPLAS. ACM. DOI 10.1145/78969.78972 - Nebenläufige Objekte im Allgemeinen:
Maurice Herlihy and Nir Shavit. 2012. The Art of Multiprocessor Programming, Revised Reprint (1st. ed.). Morgan Kaufmann Publishers Inc., San Francisco, CA, USA. ISBN: 978-0-12-397337-5, Kapitel 3
How to give a Talk
Kickoff
Prüfungs- und Studienleistung
Sie werden in diesem Seminar
- in der Vorlesungszeit einen Talk von 30 Minuten (inklusive Fragen) vorbereiten und halten.
- eine Seminararbeit aus bis zu 10 Seiten in Englisch oder Deutsch verfassen, in der "acmsmall"-Version des acmart LaTeX-Style.
- in einem Peer-Review-Verfahren die Seminararbeit eines anderen Teilnehmers begutachten, während Ihre eigene Arbeit von einem anderen Teilnehmer begutachtet wird.
Wir weisen Sie außerdem darauf hin, dass nach dem Modulhandbuch bei allen Terminen des Seminars eine Anwesenheitspflicht zum Erhalt der Studienleistung besteht.
Zur Erstellung des Seminarpapers und des Seminartalks ist die Nutzung generativer KI nicht gestattet.
Betreuung
Verantwortlich für die Organisation des Seminars sind Natalia Gacek und Jan Grünke.
Mit dem Thema, das Sie sich aussuchen, wird Ihnen auch ein Mitarbeiter des Instituts als Betreuer an die Seite gestellt, mit dem Sie sich idealerweise regelmäßig treffen.
