Reasoning about nondeterminism in programs

Byron Cook, Eric Koskinen

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

26 Scopus citations

Abstract

Branching-time temporal logics (e.g. CTL, CTL*, modal μ-calculus) allow us to ask sophisticated questions about the nonde-terminism that appears in systems. Applications of this type of reasoning include planning, games, security analysis, disproving, precondition synthesis, environment synthesis, etc. Unfortunately, existing automatic branching-time verification tools have limitations that have traditionally restricted their applicability (e.g. push-down systems only, universal path quantifiers only, etc). In this paper we introduce an automation strategy that lifts many of these previous restrictions. Our method works reliably for properties with non-trivial mixtures of universal and existential modal operators. Furthermore, our approach is designed to support (possibly infinite-state) programs. The basis of our approach is the observation that existential reasoning can be reduced to universal reasoning if the system's statespace is appropriately restricted. This restriction on the state-space must meet a constraint derived from recent work on proving non-termination. The observation leads to a new route for implementation based on existing tools. To demonstrate the practical viability of our approach, we report on the results applying our preliminary implementation to a set of benchmarks drawn from the Windows operating system, the PostgreSQL database server, Soft-Updates patching system, as well as other hand-crafted examples.

Original languageEnglish
Title of host publicationPLDI 2013 - Proceedings of the 2013 ACM SIGPLAN Conference on Programming Language Design and Implementation
Pages219-229
Number of pages11
DOIs
StatePublished - 2013
Event34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013 - Seattle, WA, United States
Duration: 16 Jun 201319 Jun 2013

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Conference

Conference34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013
Country/TerritoryUnited States
CitySeattle, WA
Period16/06/1319/06/13

Keywords

  • CTL
  • Formal verification
  • Model checking
  • Program analysis
  • Temporal logic
  • Termination

Fingerprint

Dive into the research topics of 'Reasoning about nondeterminism in programs'. Together they form a unique fingerprint.

Cite this