Master and PhD students
Informatik der Systeme / Angewandte Informatik
Offering for participants from other disciplines
Master or PhD studies
This seminar will discuss recent research results obtained by Master and PhD students related to the software engineering group. External guest speakers will also be invited from time to time.
Will be announced.
- Christoph Scheben: Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs
Time: 16:00 (c.t.), Jun 29, 2010
Currently, no approaches are known that allow for non-termination proofs of concurrent programs which account for asynchronous communication via FIFO message queues. Those programs may be written in high-level languages such as Java or Promela. We present a ﬁrst approach to prove non- termination for such programs. In addition to integers, the programs that we consider may contain queues as data structures. We present a representation of queues and the operations on them in the domain of integers, and generate invariants that help us prove non-termination of selected control ﬂow loops using a theorem proving approach. We illustrate this approach by applying a prototype tool implementation to a number of case studies.