Decision Procedure and Verification Tool
UCLID is a tool for verifying models of computer systems. It started out primarily focused on infinite-state systems (i.e., systems that, in addition to Boolean state variables, have state variables that are integer-valued or functions from integers to integers or Booleans), but now is equipped with techniques to also reason about word-level descriptions of systems (those with finite-precision types). The key component of UCLID is a decision procedure for a decidable fragment of first-order logic, including uninterpreted functions and equality, integer linear arithmetic, finite-precision bit-vector arithmetic, and constrained lambda expressions (for modeling arrays, memories, etc.). The decision procedure operates by translating the input formula to an equi-satisfiable Boolean formula on which it invokes a Boolean satisfiability (SAT) solver.
Applications of UCLID include microprocessor verification, protocol analysis, analyzing software for security vulnerabilities, and verifying models of hybrid systems. The decision procedure can also be used as a stand-alone theorem prover, or within other first-order or higher-order logic theorem provers.
Read more about this topic: Uclid
Famous quotes containing the words decision, verification and/or tool:
“Once the decision has been reached, close your ears even to the best counter-argument: a sign of strong character. Thus an occasional will to stupidity.”
—Friedrich Nietzsche (1844–1900)
“A fact is a proposition of which the verification by an appeal to the primary sources of our knowledge or to experience is direct and simple. A theory, on the other hand, if true, has all the characteristics of a fact except that its verification is possible only by indirect, remote, and difficult means.”
—Chauncey Wright (1830–1875)
“And if thou wilt make me an altar of stone, thou shalt not build it of hewn stone: for if thou lift up thy tool upon it, thou hast polluted it.”
—Bible: Hebrew Exodus 20:25.