Reasoning about nondeterminism in programs

Byron Cook, Eric Koskinen

Research output: Contribution to journalArticlepeer-review

10 Scopus citations

Abstract

Branching-time temporal logics (e.g. CTL, CTL, modal μ- calculus) allow us to ask sophisticated questions about the nondeterminism 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 nontermination. 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
Pages (from-to)219-229
Number of pages11
JournalACM SIGPLAN Notices
Volume48
Issue number6
DOIs
StatePublished - Jun 2013

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