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
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
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
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
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
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
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.
last updated on 2025-01-13 01:12 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: