Proving Liveness of Parameterized Programs

Azadeh Farzan, Zachary Kincaid, Andreas Podelski

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Scopus citations

Abstract

Correctness of multi-threaded programs typically requires that they satisfy liveness properties. For example, a program may require that no thread is starved of a shared resource, or that all threads eventually agree on a single value. This paper presents a method for proving that such liveness properties hold. Two particular challenges which are addressed in this work are that (1) the correctness argument may rely on global behaviour of the system (e.g., the correctness argument may require that all threads collectively progress towards "the good thing" rather than one thread progressing while the others do not interfere), and (2) such programs are often designed to be executed by any number of threads, and the desired liveness properties must hold no matter how many threads are active in the system.

Original languageEnglish (US)
Title of host publicationProceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages185-196
Number of pages12
ISBN (Electronic)9781450343916
DOIs
StatePublished - Jul 5 2016
Event31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 - New York, United States
Duration: Jul 5 2016Jul 8 2016

Publication series

NameProceedings - Symposium on Logic in Computer Science
Volume05-08-July-2016
ISSN (Print)1043-6871

Other

Other31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016
CountryUnited States
CityNew York
Period7/5/167/8/16

All Science Journal Classification (ASJC) codes

  • Software
  • Mathematics(all)

Fingerprint Dive into the research topics of 'Proving Liveness of Parameterized Programs'. Together they form a unique fingerprint.

  • Cite this

    Farzan, A., Kincaid, Z., & Podelski, A. (2016). Proving Liveness of Parameterized Programs. In Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016 (pp. 185-196). (Proceedings - Symposium on Logic in Computer Science; Vol. 05-08-July-2016). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1145/2933575.2935310