Paper Info
Title
Decision procedures customized for formal verification
Abstract
The uclid verifier models a hardware or software system as an abstract state machine, where the state variables can be Boolean or integer values, or functions mapping integers to integers or Booleans. The core of the verifier consists of a decision procedure that checks the validity of formulas over the combined theories of uninterpreted functions with equality and linear integer arithmetic. It operates by transforming a formula into an equisatisfiable Boolean formula and then invoking a SAT solver. This approach has worked well for the class of logic and the types of formulas encountered in verification.
Year
DOI
Venue
2005
10.1007/11532231_19
CADE
Keywords
Field
DocType
software system,linear integer arithmetic,decision procedure,state variable,combined theory,sat solver,integer value,equisatisfiable boolean formula,abstract state machine,uclid verifier model,formal verification,software systems
Uclid,Computer science,Boolean satisfiability problem,Algorithm,Propositional calculus,Disjunctive normal form,Boolean algebra,True quantified Boolean formula,Boolean data type,Formal verification
Conference
Volume
ISSN
ISBN
3632
0302-9743
3-540-28005-7
Citations 
PageRank 
References 
0
0.34
13
Authors
2
Name
Order
Citations
PageRank
Randal E. Bryant192041194.64
Sanjit A. Seshia22226168.09