Consistency analysis of decision-making programs

Swarat Chaudhuri, Azadeh Farzan, Zachary Kincaid

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

3 Scopus citations


Applications in many areas of computing make discrete decisions under uncertainty, for reasons such as limited numerical precision in calculations and errors in sensor-derived inputs. As a result, individual decisions made by such programs may be nondeterministic, and lead to contradictory decisions at different points of an execution. This means that an otherwise correct program may execute along paths, that it would not follow under its ideal semantics, violating essential program invariants on the way. A program is said to be consistent if it does not suffer from this problem despite uncertainty in decisions. In this paper, we present a sound, automatic program analysis for verifying that a program is consistent in this sense. Our analysis proves that each decision made along a program execution is consistent with the decisions made earlier in the execution. The proof is done by generating an invariant that abstracts the set of all decisions made along executions that end at a program location l, then verifying, using a fixpoint constraint-solver, that no contradiction can be derived when these decisions are combined with new decisions made at l. We evaluate our analysis on a collection of programs implementing algorithms in computational geometry. Consistency is known to be a critical, frequently-violated, and thoroughly studied correctness property in geometry, but ours is the first attempt at automated verification of consistency of geometric algorithms. Our benchmark suite consists of implementations of convex hull computation, triangulation, and point location algorithms. On almost all examples that are not consistent (with two exceptions), our analysis is able to verify consistency within a few minutes.

Original languageEnglish (US)
Title of host publicationPOPL 2014 - Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Number of pages13
StatePublished - 2014
Externally publishedYes
Event41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014 - San Diego, CA, United States
Duration: Jan 22 2014Jan 24 2014

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566


Other41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014
Country/TerritoryUnited States
CitySan Diego, CA

All Science Journal Classification (ASJC) codes

  • Software


  • consistency
  • geometry
  • program analysis
  • robustness
  • uncertainty


Dive into the research topics of 'Consistency analysis of decision-making programs'. Together they form a unique fingerprint.

Cite this