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
Contents
Invited Talks
Verification Challenges in Configurable Processor Design with ASIP Meister.
Masaharu Imai, Akira Kitajima
2
Tutorial
Towards the Pervasive Verification of Automotive Systems.
Thomas In der Rieden, Dirk Leinenbach, Wolfgang J. Paul
3-4
Functional Approaches to Design Description
Game Solving Approaches
Verifying Quantitative Properties Using Bound Functions.
Arindam Chakrabarti, Krishnendu Chatterjee, Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar
50-64
Abstraction
Interleaved Invariant Checking with Dynamic Abstraction.
Liang Zhang, Mukul R. Prasad, Michael S. Hsiao
81-96
Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units.
Miroslav N. Velev
97-113
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
114-128
Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation.
Orna Grumberg, Tamir Heyman, Nili Ifergan, Assaf Schuster
129-145
Saturation-Based Symbolic Reachability Analysis Using Conjunctive and Disjunctive Partitioning.
Gianfranco Ciardo, Andy Jinqing Yu
146-161
Real Time and LTL Model Checking
Algorithms and Techniques for Speeding Verification 2
Jason Baumgartner, Hari Mony
222-237
A New SAT-Based Algorithm for Symbolic Trajectory Evaluation.
Jan-Willem Roorda, Koen Claessen
238-253
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
254-268
Model Reduction
Exploiting Constraints in Transformation-Based Verification.
Hari Mony, Jason Baumgartner, Adnan Aziz
269-284
Identification and Counter Abstraction for Full Virtual Symmetry.
Ou Wei, Arie Gurfinkel, Marsha Chechik
285-300
Verification of Memory Hierarchy Mechanisms
On the Verification of Memory Management Mechanisms.
Iakov Dalinger, Mark A. Hillebrand, Wolfgang J. Paul
301-316
Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification.
Sudhindra Pandav, Konrad Slind, Ganesh Gopalakrishnan
317-331
Short Papers
Symbolic Partial Order Reduction for Rule Based Transition Systems.
Ritwik Bhattacharya, Steven M. German, Ganesh Gopalakrishnan
332-335
Verifying Timing Behavior by Abstract Interpretation of Executable Code.
Christian Ferdinand, Reinhold Heckmann
336-339
Masahiro Fujita
340-344
Deadlock Prevention in the Æthereal Protocol.
Biniam Gebremichael, Frits W. Vaandrager, Miaomiao Zhang, Kees Goossens, Edwin Rijpkema, Andrei Radulescu
345-348
Error Detection Using BMC in a Parallel Environment.
Subramanian K. Iyer, Jawahar Jain, Mukul R. Prasad, Debashis Sahoo, Thomas Sidle
354-358
A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems.
Panagiotis Manolios, Sudarshan K. Srinivasan
363-366
Improvements to the Implementation of Interpolant-Based Model Checking.
João P. Marques Silva
367-370
High-Level Modelling, Analysis, and Verification on FPGA-Based Hardware Design.
Petr Matousek, Ales Smrcka, Tomás Vojnar
371-375
Proving Parameterized Systems: The Use of Pseudo-Pipelines in Polyhedral Logic.
Katell Morin-Allory, David Cachera
376-379
FPGA Based Accelerator for 3-SAT Conflict Analysis in SAT Solvers.
Mona Safar, M. Watheq El-Kharashi, Ashraf Salem
384-387
Predictive Reachability Using a Sample-Based Approach.
Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill, E. Allen Emerson
388-392
Data Refinement for Synchronous System Specification and Construction.
Alex Tsow, Steven D. Johnson
398-401