Verification of Concurrent Programs SS2012

Today, almost every computer we buy has more than a single processor. Consequently, software running on our computers is becoming increasingly concurrent, i.e., it consists of several execution threads that process several tasks in parallel and interact with each other during the operation.

However, it is extremely difficult to develop concurrent programs that are free of bugs, as evidenced by various vulnerabilities found in open-source software like Mozilla suite or Apache web server.

This seminar will cover topics related to verifying various properties of concurrent programs. We will also discuss about tools used in practice for verification and finding bugs.

Introductory slides to verification of concurrent programs

• Slides (pdf)

List of topics

1. KISS: Keep it simple and sequential (pdf)
2. Asserting and checking determinism for multithreaded programs (pdf)
3. Efficient Algorithms for pre* and post* on Interprocedural Parallel Flow Graphs (pdf)
4. Scalable synchronous queues (pdf)
5. Abstraction-guided synthesis of synchronization (pdf)

List of summary papers and presentation slides

1. KISS: Keep it simple and sequential - assigned to Steffen Smolka (summary), (slides)
2. Asserting and checking determinism for multithreaded programs - assigned to Jennifer Reinelt (summary), (slides)
3. Efficient Algorithms for pre* and post* on Interprocedural Parallel Flow Graphs - assigned to Yutaka Nagashima (summary), (slides)
4. Scalable synchronous queues - assigned to Nakul Chaudhari (summary), (slides)
5. Abstraction-guided synthesis of synchronization - assigned to Sergey Grebenshchikov (summary), (slides)