IFIP TC6 Open Digital Library

13. CHARME 2005: Saarbrücken, Germany

Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005, Proceedings

Dominique Borrione, Wolfgang J. Paul

Springer, Lecture Notes in Computer Science 3725, ISBN: 3-540-29105-9


Invited Talks

Is Formal Verification Bound to Remain a Junior Partner of Simulation?

Wolfram Büttner


Verification Challenges in Configurable Processor Design with ASIP Meister.

Masaharu Imai, Akira Kitajima



Towards the Pervasive Verification of Automotive Systems.

Thomas In der Rieden, Dirk Leinenbach, Wolfgang J. Paul


Functional Approaches to Design Description

Wired: Wire-Aware Circuit Design.

Emil Axelsson, Koen Claessen, Mary Sheeran


Formalization of the DE2 Language.

Warren A. Hunt Jr., Erik Reeber


Game Solving Approaches

Finding and Fixing Faults.

Stefan Staber, Barbara Jobstmann, Roderick Bloem


Verifying Quantitative Properties Using Bound Functions.

Arindam Chakrabarti, Krishnendu Chatterjee, Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar



How Thorough Is Thorough Enough?

Arie Gurfinkel, Marsha Chechik


Interleaved Invariant Checking with Dynamic Abstraction.

Liang Zhang, Mukul R. Prasad, Michael S. Hsiao


Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units.

Miroslav N. Velev


Algorithms and Techniques for Speeding (DD-Based) Verification 1

Efficient Symbolic Simulation via Dynamic Scheduling, Don't Caring, and Case Splitting.

Viresh Paruthi, Christian Jacobi 0002, Kai Weber


Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation.

Orna Grumberg, Tamir Heyman, Nili Ifergan, Assaf Schuster


Saturation-Based Symbolic Reachability Analysis Using Conjunctive and Disjunctive Partitioning.

Gianfranco Ciardo, Andy Jinqing Yu


Real Time and LTL Model Checking

Real-Time Model Checking Is Really Simple.

Leslie Lamport


Temporal Modalities for Concisely Capturing Timing Diagrams.

Hana Chockler, Kathi Fisler


Regular Vacuity.

Doron Bustan, Alon Flaisher, Orna Grumberg, Orna Kupferman, Moshe Y. Vardi


Algorithms and Techniques for Speeding Verification 2

Automatic Generation of Hints for Symbolic Traversal.

David Ward, Fabio Somenzi


Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization Strategies.

Jason Baumgartner, Hari Mony


A New SAT-Based Algorithm for Symbolic Trajectory Evaluation.

Jan-Willem Roorda, Koen Claessen


Evaluation of SAT-Based Tools

An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment.

Nina Amla, Xiaoqun Du, Andreas Kuehlmann, Robert P. Kurshan, Kenneth L. McMillan


Model Reduction

Exploiting Constraints in Transformation-Based Verification.

Hari Mony, Jason Baumgartner, Adnan Aziz


Identification and Counter Abstraction for Full Virtual Symmetry.

Ou Wei, Arie Gurfinkel, Marsha Chechik


Verification of Memory Hierarchy Mechanisms

On the Verification of Memory Management Mechanisms.

Iakov Dalinger, Mark A. Hillebrand, Wolfgang J. Paul


Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification.

Sudhindra Pandav, Konrad Slind, Ganesh Gopalakrishnan


Short Papers

Symbolic Partial Order Reduction for Rule Based Transition Systems.

Ritwik Bhattacharya, Steven M. German, Ganesh Gopalakrishnan


Verifying Timing Behavior by Abstract Interpretation of Executable Code.

Christian Ferdinand, Reinhold Heckmann


Behavior-RTL Equivalence Checking Based on Data Transfer Analysis with Virtual Controllers and Datapaths.

Masahiro Fujita


Deadlock Prevention in the Æthereal Protocol.

Biniam Gebremichael, Frits W. Vaandrager, Miaomiao Zhang, Kees Goossens, Edwin Rijpkema, Andrei Radulescu


Acceleration of SAT-Based Iterative Property Checking.

Daniel Große, Rolf Drechsler


Error Detection Using BMC in a Parallel Environment.

Subramanian K. Iyer, Jawahar Jain, Mukul R. Prasad, Debashis Sahoo, Thomas Sidle


Formal Verification of Synchronizers.

Tsachy Kapschitz, Ran Ginosar


A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems.

Panagiotis Manolios, Sudarshan K. Srinivasan


Improvements to the Implementation of Interpolant-Based Model Checking.

João P. Marques Silva


High-Level Modelling, Analysis, and Verification on FPGA-Based Hardware Design.

Petr Matousek, Ales Smrcka, Tomás Vojnar


Proving Parameterized Systems: The Use of Pseudo-Pipelines in Polyhedral Logic.

Katell Morin-Allory, David Cachera


Resolving Quartz Overloading.

Oliver Pell, Wayne Luk


FPGA Based Accelerator for 3-SAT Conflict Analysis in SAT Solvers.

Mona Safar, M. Watheq El-Kharashi, Ashraf Salem


Predictive Reachability Using a Sample-Based Approach.

Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill, E. Allen Emerson


Minimizing Counterexample of ACTL Property.

ShengYu Shen, Ying Qin, Sikun Li


Data Refinement for Synchronous System Specification and Construction.

Alex Tsow, Steven D. Johnson


Introducing Abstractions via Rewriting.

William D. Young


A Case Study: Formal Verification of Processor Critical Properties.

Emmanuel Zarpas