Traditional specification languages usually describe individual
execution traces. In security-critical applications, this is often
insufficient: attackers may compare several executions to infer
information that should remain secret. Hyperproperties address this
problem by specifying permitted sets of traces.
The seminar covers logics for describing hyperproperties and algorithms
for checking whether systems satisfy them, with a focus on HyperLTL and
automata-based model checking. For motivation, see this
article on Spectre, Meltdown, and information-flow security
.
Paper preferences
Skim the abstracts and introductions of the
research papers,
then email your ranked list by
12:30 on .
Groups and papers will be announced the same day.
Organizer contact details.
Email your research-paper preferences in decreasing order of interest. Groups and papers will be announced the same day.
14:00–16:00
Group presentations
Foundational presentations followed by discussion.
Room 5609.EG.038 (00.09.038)
14:00–18:00
Individual presentations
Individual research-paper talks followed by discussion.
Room 5609.EG.038 (00.09.038)
Submit by email
Written summaries
Submit your approximately five-page summary, placing your paper in the context of the seminar.
Format and grading
Group phase
Two groups of 3-4 students read their group's readings and prepare one coherent joint presentation, using examples to explain the definitions and main ideas.
Present for approximately 60 minutes, then lead a 30-minute discussion using exercises and quiz questions prepared in advance.
Participate in both group discussions.
Individual phase
Read one research paper and prepare a presentation explaining its problem and contribution with an example, as well as its assumptions, evidence, and limitations.
Present for approximately 30 minutes, then lead a 15-minute discussion. Participate in all individual discussions.
Write an approximately five-page summary in your own words, connecting your paper to the foundations and other talks.
Group presentation
40%
Individual presentation
40%
Individual summary
20%
Listen actively, ask questions, contribute to discussions, give
constructive feedback to your peers, and seek feedback from the
organizers and your peers.
The seminar is open to Bachelor's and Master's students and has no
formal prerequisites. An interest in logic is helpful; courses such as
Functional Programming and Verification,
Diskrete Strukturen, or
Einführung in die theoretische Informatik provide relevant
background, but none is required.
Use of generative AI
You may use AI as a study aid in ways that deepen your understanding.
Do the readings yourself and double-check AI's answers.
Prepare your presentation and summary yourself.
State how you used AI tools in your slides and summary.
Ask the organizers if you are unsure whether a use is allowed.