Sciweavers

Share
CAV
2003
Springer
127views Hardware» more  CAV 2003»
9 years 3 months ago
Dense Counter Machines and Verification Problems
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...
Gaoyan Xie, Zhe Dang, Oscar H. Ibarra, Pierluigi S...
CAV
2003
Springer
188views Hardware» more  CAV 2003»
9 years 3 months ago
Thread-Modular Abstraction Refinement
odular Abstraction Refinement Thomas A. Henzinger1 , Ranjit Jhala1 , Rupak Majumdar1 , and Shaz Qadeer2 1 University of California, Berkeley 2 Microsoft Research, Redmond Abstract....
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar,...
CAV
2003
Springer
155views Hardware» more  CAV 2003»
9 years 3 months ago
An Improved On-The-Fly Tableau Construction for a Real-Time Temporal Logic
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...
Marc Geilen
CAV
2003
Springer
106views Hardware» more  CAV 2003»
9 years 3 months ago
Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates
redicate Abstraction Efficient: How to eliminate redundant predicates Edmund Clarke
Edmund M. Clarke, Orna Grumberg, Muralidhar Talupu...
CAV
2003
Springer
140views Hardware» more  CAV 2003»
9 years 3 months ago
Rabbit: A Tool for BDD-Based Verification of Real-Time Systems
Thispapergivesashort overviewofa model checking tool forreal-time systems. The modeling language are timed automata extended with concepts for modular modeling. The tool provides r...
Dirk Beyer, Claus Lewerentz, Andreas Noack
CAV
2003
Springer
140views Hardware» more  CAV 2003»
9 years 5 months ago
Certifying Optimality of State Estimation Programs
Abstract. The theme of this paper is certifying software for state estimation of dynamic systems, which is an important problem found in spacecraft, aircraft, geophysical, and in m...
Grigore Rosu, Ram Prasad Venkatesan, Jon Whittle, ...
CAV
2003
Springer
160views Hardware» more  CAV 2003»
9 years 5 months ago
Fast Mu-Calculus Model Checking when Tree-Width Is Bounded
We show that the model checking problem for µ-calculus on graphs of bounded tree-width can be solved in time linear in the size of the system. The result is presented by first sh...
Jan Obdrzálek
CAV
2003
Springer
153views Hardware» more  CAV 2003»
9 years 5 months ago
Interpolation and SAT-Based Model Checking
Abstract. We consider a fully SAT-based method of unbounded symbolic model checking based on computing Craig interpolants. In benchmark studies using a set of large industrial circ...
Kenneth L. McMillan
books