default search action
10. CHARME 1999: Bad Herrenalp, Germany
- Laurence Pierre, Thomas Kropf:
Correct Hardware Design and Verification Methods, 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME '99, Bad Herrenalb, Germany, September 27-29, 1999, Proceedings. Lecture Notes in Computer Science 1703, Springer 1999, ISBN 3-540-66559-5
Invited Talks
- Gérard Berry:
Esterel and Jazz: Two Synchronous Languages for Circuit Design (Abstract). 1 - Peter Jansen:
Design Process of Embedded Automotive Systems - Using Model Checking for Correct Specification. 2-7
Proof of Microprocessors
- Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam K. Srivas:
A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm without a Reorder Buffer. 8-22 - Byron Cook, John Launchbury, John Matthews, Richard B. Kieburtz:
Formal Verification of Explicitly Parallel Microprocessors. 23-36 - Miroslav N. Velev
, Randal E. Bryant:
Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic. 37-53
Model Checking
- Yuan Yu, Panagiotis Manolios
Model Checking TLA+ Specifications. 54-66 - Nina Amla, E. Allen Emerson, Kedar S. Namjoshi:
Efficient Decompositional Model Checking for Regular Timing Diagrams. 67-81 - Orna Kupferman, Moshe Y. Vardi:
Vacuity Detection in Temporal Model Checking. 82-96
Formal Methiods and Industrial Applications
- Cindy Eisner:
Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard. 97-109 - Ying Xu, Eduard Cerny, Allan Silburt, A. Coady, Ying Liu, Philip Pownall:
Practical Application of Formal Verification Techniques on a Frame Mux/Demux Chip from Nortel Semiconductors. 110-124 - Marius Bozga, Oded Maler, Stavros Tripakis
Efficient Verification of Timed Automata Using Dense and Discrete Time Semantics. 125-141
Abstraction and Compositional Techniques
- E. Allen Emerson, Richard J. Trefler:
From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking. 142-156 - Dirk W. Hoffmann, Thomas Kropf:
Automatic Error Correction of Large Circuits Using Boolean Decomposition and Abstraction. 157-171 - Edmund M. Clarke, Somesh Jha, Yuan Lu, Dong Wang:
Abstract BDDs: A Technique for Using Abstraction in Model Checking. 172-186
Theorem Proving Related Approaches
- Christian Blumenröhr, Viktor K. Sabelfeld:
Formal Synthesis at the Algorithmic Level. 187-201 - Mark D. Aagaard, Thomas F. Melham, John W. O'Leary:
Xs are for Trajectory Evaluation, Booleans are for Theorem Proving. 202-218 - Kenneth L. McMillan:
Verification of Infinite State Systems by Compositional Model Checking. 219-234
Symbolic Simulation/Symbolic Traversal
- Gerd Ritter, Hans Eveking, Holger Hinrichsen:
Formal Verification of Designs with Complex Control by Symbolic Simulation. 234-249 - Kavita Ravi, Fabio Somenzi:
Hints to accelerate Symbolic Traversal. 250-264
Specification Languages and Methodologies
- Jürgen Ruf, Thomas Kropf:
Modleing and Checking Networks of Communicating Real-Time Process. 265-279 - Sagi Katz, Orna Grumberg, Daniel Geist:
"Have I written enough Properties?" - A Method of Comparison between Specification and Implementation. 280-297 - Edmund M. Clarke, Masahiro Fujita, Sreeranga P. Rajan, Thomas W. Reps, Subash Shankar, Tim Teitelbaum:
Program Slicing of Hardware Description Languages. 298-312
Posters
- Jun Sawada, Warren A. Hunt Jr.:
Results of the Verification of a Complex Pipelined Machine Model. 313-316 - Hüsnü Yenigün, Vladimir Levin, Doron A. Peled, Peter A. Beerel:
Hazard-Freedom Checking in Speed-Independent Systems. 317-320 - Klaus Schneider
Yet another Look at the LTL Model Checking. 321-325 - Stefan Hendricx, Luc J. M. Claesen:
Verification of Finite-State-Machine Refinements Using a Symbolic Methodology. 326-329 - George Economakos, George K. Papakonstantinou:
Refinement and Property Checking in High-Level Synthesis using Attribute Grammars. 330-333 - Steven D. Johnson, Yanhong A. Liu, Yuchen Zhang:
A Systematic Incrementalization Technique and Its Application to Hardware Design. 334-337 - Kathi Fisler
Bisimulation and Model Checking. 338-341 - Kenneth L. McMillan:
Circular Compositional Reasoning about Liveness. 342-345 - Nancy A. Day, Jeffrey R. Lewis, Byron Cook:
Symbolic Simulation of Microprocessor Models using Type Classes in Haskell. 346-349 - Aarti Gupta, Pranav Ashar, Sharad Malik:
Exploiting Retiming in a Guided Simulation Based Validation Methodology. 350-353 - Jens Chr. Godesken:
Fault Models for Embedded Systems (Extended Abstract). 354-359 - Klaus Schneider
Validation of Object-Oriented Concurrent Designs by Model Checking. 360-364
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 2024-11-20 21:06 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: