Paper Info
Title
Reasoning about Infinite State Systems Using Boolean Methods
Abstract
The logic of Counters, Lambdas, and Uninterpreted functions (CLU) is a subset of first-order logic satisfying the twin properties that 1) the validity of a CLU formula can be decided by generating a Boolean formula and using a Boolean satisfiability (SAT) checker to show the formula is unsatisfiable, and 2) it has sufficient expressive power to construct models of a variety of interesting software and hardware systems. We describe this logic and show its modeling capabilities.
Year
DOI
Venue
2003
10.1007/978-3-540-24597-1_34
LECTURE NOTES IN COMPUTER SCIENCE
Keywords
Field
DocType
boolean satisfiability,satisfiability,first order logic,expressive power
Maximum satisfiability problem,Boolean function,Discrete mathematics,Boolean circuit,Computer science,Boolean satisfiability problem,Product term,Boolean algebra,True quantified Boolean formula,Boolean expression
Conference
Volume
ISSN
Citations 
2914
0302-9743
0
PageRank 
References 
Authors
0.34
15
1
Name
Order
Citations
PageRank
Randal E. Bryant192041194.64