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.