Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
CAV
2004
Springer
130views Hardware» more  CAV 2004»
11 years 2 months ago
Global Model-Checking of Infinite-State Systems
Abstract. We extend the automata-theoretic framework for reasoning about infinitestate sequential systems to handle also the global model-checking problem. Our framework is based o...
Nir Piterman, Moshe Y. Vardi
CAV
2004
Springer
126views Hardware» more  CAV 2004»
11 years 2 months ago
An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking
Model checking algorithms can report a property as being true for reasons that may be considered vacuous. Current algorithms for detecting vacuity require either checking a quadrat...
Kedar S. Namjoshi
CAV
2004
Springer
140views Hardware» more  CAV 2004»
11 years 2 months ago
Indexed Predicate Discovery for Unbounded System Verification
Predicate abstraction has been proved effective for verifying several infinite-state systems. In predicate abstraction, an abstract system is automatinstructed given a set of predi...
Shuvendu K. Lahiri, Randal E. Bryant
CAV
2004
Springer
122views Hardware» more  CAV 2004»
11 years 2 months ago
Abstraction-Based Satisfiability Solving of Presburger Arithmetic
Daniel Kroening, Joël Ouaknine, Sanjit A. Ses...
CAV
2004
Springer
121views Hardware» more  CAV 2004»
11 years 2 months ago
CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking
Abstract. CirCUs is a satisfiability solver that works on a combination of AndInverter-Graph, CNF clauses, and BDDs. It has been designed to work well with bounded model checking. ...
HoonSang Jin, Mohammad Awedh, Fabio Somenzi
CAV
2004
Springer
108views Hardware» more  CAV 2004»
11 years 2 months ago
Functional Dependency for Verification Reduction
Abstract. The existence of functional dependency among the state variables of a state transition system was identified as a common cause of inefficient BDD representation in formal...
Jie-Hong Roland Jiang, Robert K. Brayton
CAV
2004
Springer
96views Hardware» more  CAV 2004»
11 years 2 months ago
Verification via Structure Simulation
Neil Immerman, Alexander Moshe Rabinovich, Thomas ...
CAV
2004
Springer
151views Hardware» more  CAV 2004»
11 years 2 months ago
QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings
We study the problem of formally verifying shared memory multiprocessor executions against memory consistency models--an important step during post-silicon verification of multipro...
Ganesh Gopalakrishnan, Yue Yang, Hemanthkumar Siva...
CAV
2004
Springer
136views Hardware» more  CAV 2004»
11 years 2 months ago
JNuke: Efficient Dynamic Analysis for Java
JNuke is a framework for verification and model checking of Java programs. It is a novel combination of run-time verification, explicit-state model checking, and counter-example ex...
Cyrille Artho, Viktor Schuppan, Armin Biere, Pasca...
CAV
2004
Springer
154views Hardware» more  CAV 2004»
11 years 2 months ago
Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values
Sequential consistency is the archetypal correctness condition for the memory protocols of shared-memory multiprocessors. Typically, such protocols are parameterized by the number ...
Jesse D. Bingham, Anne Condon, Alan J. Hu, Shaz Qa...
books