Sciweavers

CHARME
2005
Springer
145views Hardware» more  CHARME 2005»
13 years 7 months ago
Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization Strategies
Abstract. Automatic formal verification techniques generally require exponential resources with respect to the number of primary inputs of a netlist. In this paper, we present sev...
Jason Baumgartner, Hari Mony
CHARME
2005
Springer
124views Hardware» more  CHARME 2005»
13 years 11 months ago
Finding and Fixing Faults
Stefan Staber, Barbara Jobstmann, Roderick Bloem
CHARME
2005
Springer
120views Hardware» more  CHARME 2005»
13 years 11 months ago
Minimizing Counterexample of ACTL Property
ShengYu Shen, Ying Qin, Sikun Li
CHARME
2005
Springer
136views Hardware» more  CHARME 2005»
13 years 11 months ago
Predictive Reachability Using a Sample-Based Approach
Abstract. Unbounded model checking of invariant properties is typically solved using symbolic reachability. However, BDD based reachability methods suffer from lack of robustness ...
Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer,...
CHARME
2005
Springer
170views Hardware» more  CHARME 2005»
13 years 11 months ago
Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification
Sudhindra Pandav, Konrad Slind, Ganesh Gopalakrish...
CHARME
2005
Springer
119views Hardware» more  CHARME 2005»
13 years 11 months ago
High-Level Modelling, Analysis, and Verification on FPGA-Based Hardware Design
Petr Matousek, Ales Smrcka, Tomás Vojnar
CHARME
2005
Springer
130views Hardware» more  CHARME 2005»
13 years 11 months ago
Improvements to the Implementation of Interpolant-Based Model Checking
The evolution of SAT technology over the last decade has motivated its application in model checking, initially through the utilization of SAT in bounded model checking (BMC) and, ...
João P. Marques Silva
CHARME
2005
Springer
124views Hardware» more  CHARME 2005»
13 years 11 months ago
A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems
Panagiotis Manolios, Sudarshan K. Srinivasan
CHARME
2005
Springer
128views Hardware» more  CHARME 2005»
13 years 11 months ago
Real-Time Model Checking Is Really Simple
Leslie Lamport
CHARME
2005
Springer
143views Hardware» more  CHARME 2005»
13 years 11 months ago
Saturation-Based Symbolic Reachability Analysis Using Conjunctive and Disjunctive Partitioning
Abstract. We propose a new saturation-based symbolic state-space generation algorithm for finite discrete-state systems. Based on the structure of the high-level model specificat...
Gianfranco Ciardo, Andy Jinqing Yu