CHARME
2003
Springer
14 years 9 days ago
2003
Springer
Abstract. We propose new, tractably (in some cases provably) efficient algorithmic methods for exact (sound and complete) parameterized reasoning about cache coherence protocols. F...
CHARME
2003
Springer
14 years 9 days ago
2003
Springer
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...
CHARME
2003
Springer
14 years 9 days ago
2003
Springer
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 ...
CAV
2003
Springer
14 years 9 days ago
2003
Springer
We generalize the traditional definition of a multicounter machine (where the counters, which can only assume nonnegative integer values, can be incremented/decremented by 1 and te...
CAV
2003
Springer
14 years 9 days ago
2003
Springer
odular Abstraction Refinement Thomas A. Henzinger1 , Ranjit Jhala1 , Rupak Majumdar1 , and Shaz Qadeer2 1 University of California, Berkeley 2 Microsoft Research, Redmond Abstract....
CAV
2003
Springer
14 years 9 days ago
2003
Springer
Abstract. Temporal logic is popular for specifying correctness properties of reactive systems. Real-time temporal logics add the ability to express quantitative timing aspects. Tab...
CAV
2003
Springer
14 years 9 days ago
2003
Springer
redicate Abstraction Efficient: How to eliminate redundant predicates Edmund Clarke
CAV
2003
Springer
14 years 9 days ago
2003
Springer
Thispapergivesashort overviewofa model checking tool forreal-time systems. The modeling language are timed automata extended with concepts for modular modeling. The tool provides r...
CHARME
2001
Springer
14 years 9 days ago
2001
Springer
CHARME
2001
Springer
14 years 9 days ago
2001
Springer
In this paper we present a syntactical approach for deriving real-time programs from a formal specification of the requirements of real-time systems. The main idea of our approach ...