This site uses cookies to deliver our services and to ensure you get the best experience. By continuing to use this site, you consent to our use of cookies and acknowledge that you have read and understand our Privacy Policy, Cookie Policy, and Terms
Industrial verification teams are actively developing suitable event sequence languages for hardware verification. Such languages must be expressive, designer friendly, and hardwar...
Abstract. We propose new, tractably (in some cases provably) efficient algorithmic methods for exact (sound and complete) parameterized reasoning about cache coherence protocols. F...
Abstract. I develop a compositional theory of refinement for the branching time framework based on stuttering simulation and prove that if one system refines another, then a refine...
In formal verification, we verify that a system is correct with respect to a specification. Even when the system is proven to be correct, there is still a question of how complete ...
We present a non-operational approach to specifying and analyzing shared memory consistency models. The method uses higher order logic to capture a complete set of ordering constra...
Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, K...
Intrusion-tolerance is the technique of using fault-tolerance to achieve security properties. Assuming that faults, both benign and Byzantine, are unavoidable, the main goal of Int...