Semesterside for IN5630 - V?r 2024

Dear all,

We are all coming to the end of the course and next week will be the final one. The plan is as follows.

Tuesday 21.
Deadline for Home exam 2. Inspera should be open now

Wednesday 22.

• Q/A. You can here ask about the course and the exam. We will Monday post the exam questions and how the exam will be conducted. Next week we will also fix the schedule for the exam.
• Guest lecture: Tobias Reinhard will give an introduction to seperation logic.

You are all invited to this guest lecture.

Title: Completeness Thresholds for Memory Safety: Unbounded Guarantees via Bounded Proofs
Speaker: Tobias Reinhard, TU Darmstadt, Germany
Time: Tue 21 May @ 11:05
Place: Seminarrom Perl

Abstract:
We present the first study of completeness thresholds (CTs) for infinite state systems.
Any bounded proof reaching its CT is sound. Thereby, CTs allow us to reduce unbounded proofs to bounded ones.
Specifically, we focus on memory safety proofs for programs that iterate over arbitrarily large data structures in a memory-layout-preserving way. Meanwhile, many of the results straightforwardly apply to arbitrary correctness properties.
We present a generic approach to extract CTs from a program's verification condition and show that it scales. Moreover, we demonstrate that we can characterise CTs for interesting classes of array traversing programs.
 

Hello students!

Sorry for the late message. But just to avoid any confusion; given that the deadline for Home Exam 2 is approaching, today will be another Q&A session. Feel free to work on some of the exercises from the previous weeks if you please --- you can ask questions about those as well.

See you at 10:15!