Adaptive Eager Boolean Encoding for Arithmetic Reasoning in Verification

Sanjit A. Seshia. Adaptive Eager Boolean Encoding for Arithmetic Reasoning in Verification. Ph.D. Thesis, Carnegie Mellon University, 2005.
Co-winner, 2005 SCS Distinguished Dissertation Award.

Download

[pdf]  [HTML] 

Abstract

Decision procedures for first-order logics are widely applicable in design verification and static program analysis. However, existing procedures rarely scale to large systems, especially for verifying properties that depend on data or timing, in addition to control.This thesis presents a new approach for building efficient, automated decision procedures for first-order logics involving arithmetic. In this approach, decision problems involving arithmetic are transformed to problems in the Boolean domain, such as Boolean satisfiability solving, thereby leveraging recent advances in that area. The transformation automatically detects and exploits problem structure based on new theoretical results and machine learning. The results of experimental evaluations show that our decision procedures can outperform other state-of-the-art procedures by several orders of magnitude.The decision procedures form the computational engines for two verification systems, UCLID and TMV. These systems have been applied to problems in computer security, electronic design automation, and software engineering that require efficient and precise analysis of system functionality and timing. This thesis describes two such applications: finding format-string exploits in software, and verifying circuits that operate under timing assumptions.

BibTeX

@PhdThesis{seshia-thesis05,
  author = 	 "Sanjit A. Seshia",
  title = 	 "Adaptive Eager Boolean Encoding for Arithmetic Reasoning in Verification",
  school = 	 "Carnegie Mellon University",
  year = 	 "2005",
  month = {May},
  abstract = {
Decision procedures for first-order logics are widely applicable in design verification and static program analysis. However, existing procedures rarely scale to large systems, especially for verifying properties that depend on data or timing, in addition to control.
This thesis presents a new approach for building efficient, automated decision procedures for first-order logics involving arithmetic. In this approach, decision problems involving arithmetic are transformed to problems in the Boolean domain, such as Boolean satisfiability solving, thereby leveraging recent advances in that area. The transformation automatically detects and exploits problem structure based on new theoretical results and machine learning. The results of experimental evaluations show that our decision procedures can outperform other state-of-the-art procedures by several orders of magnitude.
The decision procedures form the computational engines for two verification systems, UCLID and TMV. These systems have been applied to problems in computer security, electronic design automation, and software engineering that require efficient and precise analysis of system functionality and timing. This thesis describes two such applications: finding format-string exploits in software, and verifying circuits that operate under timing assumptions.},
}