Quick links:
My publications and some talks.
UCLID |
UCLID is a tool for verifying models of computer systems. Its key component 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, and analyzing software for security vulnerabilities. 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... |
V4R |
V4R is short for "Verification for Resilience". This project is investigating the use of formal and semi-formal verification in the construction of systems resilient to device errors including those arising from soft errors, aging, environmental and parameter variations, and aggressive deployment of techniques to reduce resource consumption (e.g., power). This project is very new, and there is a lot yet to be done! Click here to read about the results we've obtained so far. |
TMV |
TMV is a model checker for timed systems, e.g., timed automata, which have real-valued clocks or timer variables in addition to Boolean state variables. The key theoretical contribution in TMV is a translation of quantified separation logic to quantified Boolean logic. Applications include the design and verification of circuits that operate under timing assumptions. read more... |
Calvin |
Calvin is a tool for checking safety properties of multithreaded Java programs. To handle realistic programs, Calvin performs modular checking of each procedure called by a thread using specifications of other procedures and other threads. The checker leverages off existing sequential program verification techniques based on automatic theorem proving. The Java programs we have applied Calvin to include the Apprentice challenge problem, the Mercator web crawler, and some Java libraries. read more... |
Miscellaneous |
Some of the other areas I've worked in: |
Back to my home page.