|
[ PDF Version ]
Sunday, Oct 2
| 18:00 |
|
Welcome Reception in the Hotel Lobby
|
Monday, Oct 3
| 08:30 |
|
Tutorial: Towards the Pervasive Verification of Automotive Systems (Part I)
Thomas In der Rieden, Dirk Leinenbach, and Wolfgang Paul (Saarland University)
[ Abstract ]
|
| 10:00 |
|
Coffee Break |
| 10:30 |
|
Tutorial: Towards the Pervasive Verification of Automotive Systems (Part II)
Thomas In der Rieden, Dirk Leinenbach, and Wolfgang Paul (Saarland University)
[ Abstract ]
|
| 12:00 |
|
Lunch Break |
| 13:30 |
|
Tools and Demos |
| 16:00 |
|
Coffee Break |
| 16:30 |
|
Tools and Demos |
| 17:30 |
|
End |
Tuesday, Oct 4
| 08:30 |
|
Invited Talk: Is Formal Verification Bound to Remain a Junior Partner of Simulation?
Wolfram Büttner (OneSpin Solutions)
[ Abstract ]
|
| Functional Approaches to Design Description |
| 09:30 |
|
Wired: Wire-aware circuit design
Emil Axelsson, Koen Claessen, Mary Sheeran
|
| 10:00 |
|
Formalization of the DE2 Language
Warren A. Hunt, Jr. and Erik Reeber
|
| 10:30 |
|
Coffee Break |
| Game Solving Approaches |
| 11:00 |
|
Finding and Fixing Faults
Stefan Staber, Barbara Jobstmann, Roderick Bloem
|
| 11:30 |
|
Verifying Quantitative Properties Using Bound Functions
Arindam Chakrabarti, Krishnendu Chatterjee, Thomas A. Henzinger, Orna Kupferman, and Rupak Majumdar
|
| 12:00 |
|
Lunch Break |
| Abstraction |
| 13:30 |
|
How Thorough is Thorough Enough?
Arie Gurfinkel and Marsha Chechik
|
| 14:00 |
|
Interleaved Invariant Checking with Dynamic Abstraction
Liang Zhang, Mukul R Prasad, Michael Hsiao
|
| 14:30 |
|
Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units
Miroslav N. Velev
|
| 15:00 |
|
Coffee Break |
| Algorithms and Techniques for Speeding (DD-based) Verification I |
| 15:30 |
|
Efficient Symbolic Simulation via Dynamic Scheduling, Don't Caring, and Case Splitting
Viresh Paruthi, Christian Jacobi and Kai Weber
|
| 16:00 |
|
Achieving Speedups in Distributed Symbolic Reachability Analysis through Asynchronous Computation
Orna Grumberg, Tamir Heyman, Nili Ifergan, and Assaf Schuster |
| 16:30 |
|
Saturation-based Symbolic Reachability Analysis Using Conjunctive and Disjunctive Partitioning
Gianfranco Ciardo and Jinqing Yu
|
| 17:00 |
|
Poster Session I |
| 19:00 |
|
End |
Wednesday, Oct 5
| Real time and LTL model checking |
| 08:30 |
|
Real-Time Model Checking is Really Simple
Leslie Lamport
|
| 09:00 |
|
Temporal Modalities for Concisely Capturing Timing Diagrams
Hana Chockler and Kathi Fisler
|
| 09:30 |
|
Regular Vacuity
Doron Bustan, Alon Flaisher, Orna Grumberg, Orna Kupferman, and Moshe Y. Vardi
|
| 10:00 |
|
Coffee Break |
| Algorithms and techniques for speeding verification II |
| 10:30 |
|
Automatic Generation of Hints For Symbolic Traversal
David Ward, Fabio Somenzi
|
| 11:00 |
|
Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization Strategies
Jason Baumgartner, Hari Mony
|
| 11:30 |
|
A new SAT-based Algorithm for Symbolic Trajectory Evaluation
Jan-Willem Roorda and Koen Claessen
|
| 12:00 |
|
Lunch Break |
| 13:30 |
|
Conference Trip
UNESCO World Cultural Heritage Völklinger Hütte
|
| 19:00 |
|
Conference Dinner
Restaurant Quack im Haus Weismüller |
Thursday, Oct 6
Evaluation of SAT-based tools
|
| 08:30 |
|
An Analysis of SAT-based Model Checking Techniques in an Industrial Environment
Nina Amla, Xiaoqun Du, Andreas Kuehlmann, Robert P.Kurshan and Kenneth, L. McMillan
|
| 09:00 |
|
Round Table Discussion: Verification challenges in very large designs and their automation
Initiating presentation: Verification Challenges in Configurable Processor Design with ASIP Meister
Masaharu Imai and Akira Kitajima (Osaka University)
[ Abstract ]
Responders: David Hardin (Rockwell Collins), Wolf Zimmermann (Universität Halle), Roope Kaivola (Intel)
|
| 10:30 |
|
Coffee Break |
| 11:00 |
|
Poster Session II |
| 12:00 |
|
Lunch Break |
Model Reduction |
| 13:30 |
|
Exploiting Constraints in Transformation-Based Verification
Hari Mony, Jason Baumgartner, Adnan Aziz
|
| 14:00 |
|
Identification and Counter Abstraction for Full Virtual Symmetry
Ou Wei, Arie Gurfinkel and Marsha Chechik
|
| 14:30 |
|
Coffee Break |
| Verification of Memory Hierarchy Mechanisms |
| 15:00 |
|
On the Verification of Memory Management Mechanisms
Iakov Dalinger, Mark Hillebrand, Wolfgang Paul
|
| 15:30 |
|
Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification
Sudhindra Pandav, Konrad Slind and Ganesh Gopalakrishnan
|
| 16:00 |
|
End |
|
AUTHOR'S SCHEDULE
for the CHARME2005 paper submission:
March 29:
Deadline for paper registration (title, authors, email, abstract)
Apr 8:
Deadline for paper submission
May 23:
Notification of acceptance
June 30:
Deadline for final version
At least ...
one author for each accepted paper will be
requested to register when submitting the final version
of their paper, to guarantee lower registration
fees and publication of their contribution.
|
