Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs Article Swipe

PDF

Related Concepts

Computer science Mathematical proof Asynchronous communication Programming language FIFO (computing and electronics) Java Theoretical computer science Domain (mathematical analysis) Model checking Queue Promela Representation (politics) Mathematics Computer network Mathematical analysis Geometry Politics Political science Law

M. Küntz , Stefan Leue , Christoph Scheben ·

YOU? · · 2018 · Open Access · · DOI: https://doi.org/10.29007/c7v2 · OA: W100096145

Currently, there are no approaches 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.