


default search action
13. CHARME 2005: Saarbrücken, Germany
- Dominique Borrione, Wolfgang J. Paul:

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. Lecture Notes in Computer Science 3725, Springer 2005, ISBN 3-540-29105-9
Invited Talks
- Wolfram Büttner:

Is Formal Verification Bound to Remain a Junior Partner of Simulation? 1 - Masaharu Imai, Akira Kitajima:

Verification Challenges in Configurable Processor Design with ASIP Meister. 2
Tutorial
- Thomas In der Rieden, Dirk Leinenbach, Wolfgang J. Paul:

Towards the Pervasive Verification of Automotive Systems. 3-4
Functional Approaches to Design Description
- Emil Axelsson, Koen Claessen, Mary Sheeran:

Wired: Wire-Aware Circuit Design. 5-19 - Warren A. Hunt Jr., Erik Reeber:

Formalization of the DE2 Language. 20-34
Game Solving Approaches
- Stefan Staber, Barbara Jobstmann, Roderick Bloem

:
Finding and Fixing Faults. 35-49 - Arindam Chakrabarti, Krishnendu Chatterjee, Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar:

Verifying Quantitative Properties Using Bound Functions. 50-64
Abstraction
- Arie Gurfinkel

, Marsha Chechik:
How Thorough Is Thorough Enough? 65-80 - Liang Zhang, Mukul R. Prasad, Michael S. Hsiao:

Interleaved Invariant Checking with Dynamic Abstraction. 81-96 - Miroslav N. Velev

:
Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units. 97-113
Algorithms and Techniques for Speeding (DD-Based) Verification 1
- Viresh Paruthi, Christian Jacobi, Kai Weber:

Efficient Symbolic Simulation via Dynamic Scheduling, Don't Caring, and Case Splitting. 114-128 - Orna Grumberg, Tamir Heyman, Nili Ifergan, Assaf Schuster:

Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation. 129-145 - Gianfranco Ciardo

, Andy Jinqing Yu:
Saturation-Based Symbolic Reachability Analysis Using Conjunctive and Disjunctive Partitioning. 146-161
Real Time and LTL Model Checking
- Leslie Lamport:

Real-Time Model Checking Is Really Simple. 162-175 - Hana Chockler, Kathi Fisler

:
Temporal Modalities for Concisely Capturing Timing Diagrams. 176-190 - Doron Bustan, Alon Flaisher, Orna Grumberg, Orna Kupferman, Moshe Y. Vardi:

Regular Vacuity. 191-206
Algorithms and Techniques for Speeding Verification 2
- David Ward, Fabio Somenzi:

Automatic Generation of Hints for Symbolic Traversal. 207-221 - Jason Baumgartner, Hari Mony:

Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization Strategies. 222-237 - Jan-Willem Roorda

, Koen Claessen:
A New SAT-Based Algorithm for Symbolic Trajectory Evaluation. 238-253
Evaluation of SAT-Based Tools
- Nina Amla, Xiaoqun Du, Andreas Kuehlmann, Robert P. Kurshan, Kenneth L. McMillan:

An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment. 254-268
Model Reduction
- Hari Mony, Jason Baumgartner, Adnan Aziz:

Exploiting Constraints in Transformation-Based Verification. 269-284 - Ou Wei, Arie Gurfinkel

, Marsha Chechik:
Identification and Counter Abstraction for Full Virtual Symmetry. 285-300
Verification of Memory Hierarchy Mechanisms
- Iakov Dalinger, Mark A. Hillebrand, Wolfgang J. Paul:

On the Verification of Memory Management Mechanisms. 301-316 - Sudhindra Pandav, Konrad Slind, Ganesh Gopalakrishnan

:
Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification. 317-331
Short Papers
- Ritwik Bhattacharya, Steven M. German, Ganesh Gopalakrishnan

:
Symbolic Partial Order Reduction for Rule Based Transition Systems. 332-335 - Christian Ferdinand, Reinhold Heckmann:

Verifying Timing Behavior by Abstract Interpretation of Executable Code. 336-339 - Masahiro Fujita:

Behavior-RTL Equivalence Checking Based on Data Transfer Analysis with Virtual Controllers and Datapaths. 340-344 - Biniam Gebremichael, Frits W. Vaandrager, Miaomiao Zhang, Kees Goossens, Edwin Rijpkema, Andrei Radulescu:

Deadlock Prevention in the Æthereal Protocol. 345-348 - Daniel Große

, Rolf Drechsler:
Acceleration of SAT-Based Iterative Property Checking. 349-353 - Subramanian K. Iyer, Jawahar Jain, Mukul R. Prasad, Debashis Sahoo, Thomas Sidle:

Error Detection Using BMC in a Parallel Environment. 354-358 - Tsachy Kapschitz, Ran Ginosar:

Formal Verification of Synchronizers. 359-362 - Panagiotis Manolios

, Sudarshan K. Srinivasan:
A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems. 363-366 - João Marques-Silva

:
Improvements to the Implementation of Interpolant-Based Model Checking. 367-370 - Petr Matousek

, Ales Smrcka, Tomás Vojnar:
High-Level Modelling, Analysis, and Verification on FPGA-Based Hardware Design. 371-375 - Katell Morin-Allory, David Cachera:

Proving Parameterized Systems: The Use of Pseudo-Pipelines in Polyhedral Logic. 376-379 - Oliver Pell, Wayne Luk:

Resolving Quartz Overloading. 380-383 - Mona Safar, M. Watheq El-Kharashi, Ashraf Salem

:
FPGA Based Accelerator for 3-SAT Conflict Analysis in SAT Solvers. 384-387 - Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill, E. Allen Emerson:

Predictive Reachability Using a Sample-Based Approach. 388-392 - ShengYu Shen, Ying Qin, Sikun Li:

Minimizing Counterexample of ACTL Property. 393-397 - Alex Tsow, Steven D. Johnson:

Data Refinement for Synchronous System Specification and Construction. 398-401 - William D. Young:

Introducing Abstractions via Rewriting. 402-405 - Emmanuel Zarpas:

A Case Study: Formal Verification of Processor Critical Properties. 406-409

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














