Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID11. CHARME 2001: Livingston, Scotland, UK
- Tiziana Margaria
, Thomas F. Melham:
Correct Hardware Design and Verification Methods, 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, September 4-7, 2001, Proceedings. Lecture Notes in Computer Science 2144, Springer 2001, ISBN 3-540-42541-1
Invited Contributions
- Steven D. Johnson:
View from the Fringe of the Fringe. 1-12 - Alan Mycroft, Richard Sharp:
Hardware Synthesis Using SAFL and Application to Processor Design. 13-39
FMCAD 2000
- Robert Beers, Rajnish Ghughal, Mark D. Aagaard:
Applications of Hierarchical Verification in Model Checking. 40-57
Model Checking 1
- Ofer Strichman:
Pruning Techniques for the SAT-Based Bounded Model Checking Problem. 58-70 - M. Oliver Möller, Rajeev Alur:
Heuristics for Hierarchical Partitioning with Application to Model Checking. 71-85
Short Papers 1
- Dirk Beyer:
Efficient Reachability Analysis and Refinement Checking of Timed Automata Using BDDs. 86-91 - François Siewe, Dang Van Hung:
Deriving Real-Time Programs from Duration Calculus Specifications. 92-97 - Karen Yorav, Sagi Katz, Ron Kiper:
Reproducing Synchronization Bugs with Model Checking. 98-103 - Kenneth J. Turner, Ji He:
Formally-Based Design Evaluation. 104-109
Clocking Issues
- Gérard Berry, Ellen Sentovich:
Multiclock Esterel. 110-125 - Alvin R. Albrecht, Alan J. Hu:
Register Transformations with Multiple Clock Domains. 126-139 - Anthony Winstanley, Mark R. Greenstreet:
Temporal Properties of Self-Timed Rings. 140-154
Short Papers 2
- Gil Ratsaby, Shmuel Ur, Yaron Wolfsthal:
Coverability Analysis Using Symbolic Model Checking. 155-160 - Ji He, Kenneth J. Turner:
Specifying Hardware Timing with ET-L OTOS. 161-166 - Tiberiu Seceleanu, Juha Plosila:
Formal Pipeline Design. 167-172 - Rajesh Radhakrishnan, Elena Teica, Ranga Vemuri:
Verification of Basic Block Schedules Using RTL Transformations. 173-178
Joint Session with TPHOLs
- Kenneth L. McMillan:
Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. 179-195 - Roope Kaivola, Katherine R. Kohatsu:
Proof Engineering in the Large: Formal Verification of Pentium® 4 Floating-Point Divider. 196-211
Hardware Compilation
- Steve McKeever, Wayne Luk:
Towards Provably-Correct Hardware Compilation Tools Based on Pass Separation Techniques. 212-227 - Richard Sharp, Alan Mycroft:
A Higher-Level Language for Hardware Synthesis. 228-243
Tools
- Iskander Kort, Sofiène Tahar, Paul Curzon:
Hierarchical Verification Using an MDG-HOL Hybrid Tool. 244-258 - Enrico Tronci, Giuseppe Della Penna, Benedetto Intrigila, Marisa Venturini Zilli:
Exploiting Transition Locality in Automatic Verification. 259-274 - Fady Copty, Amitai Irron, Osnat Weissberg, Nathan P. Kropp, Gila Kamhi:
Efficient Debugging in a Formal Verification Environment. 275-292
Model Checking 2
- Pankaj Chauhan, Edmund M. Clarke, Somesh Jha, James H. Kukula, Helmut Veith, Dong Wang:
Using Combinatorial Optimization Methods for Quantification Scheduling. 293-309 - Javier Esparza, Claus Schröter:
Net Reductions for LTL Model-Checking. 310-324
Component Verification
- Christoph Berg, Christian Jacobi:
Formal Verification of the VAMP Floating Point Unit. 325-339 - Kanna Shimizu, David L. Dill, Ching-Tsun Chou:
A Specification Methodology by a Collection of Compact Properties as Applied to the Intel® ItaniumTM Processor Bus Protocol. 340-354 - Koen Claessen, Mary Sheeran, Satnam Singh:
The Design and Verification of a Sorter Core. 355-369
Case Studies
- Xiaohua Kong, Radu Negulescu, Larry Weidong Ying:
Refinement-Based Formal Verification of Asynchronous Wrappers for Independently Clocked Domains in Systems on Chip. 370-385 - Jayanta Bhadra, Andrew K. Martin, Jacob A. Abraham, Magdy S. Abadir:
Using Abstract Specifications to Verify PowerPCTM Custom Memories by Symbolic Trajectory Evaluation. 386-402
Algorithm Verification
- Ricky W. Butler, Victor Carreño, Gilles Dowek, César A. Muñoz:
Formal Verification of Conflict Detection Algorithms. 403-417 - Eric Gascard, Laurence Pierre:
Induction-Oriented Formal Verification in Symmetric Interconnection Networks. 418-432 - Mark D. Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones:
A Framework for Microprocessor Correctness Statements. 433-448
Duration Calculus
- Huibiao Zhu, Jonathan P. Bowen, Jifeng He:
From Operational Semantics to Denotational Semantics for Verilog. 449-466 - Xuandong Li, Yu Pei, Jianhua Zhao, Yong Li, Tao Zheng, Guoliang Zheng:
Efficient Verification of a Class of Linear Hybrid Automata Using Linear Programming. 465-480
a service of 
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-05-13 21:24 CEST 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:
