Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Gil Ratsaby, Shmuel Ur, Yaron Wolfsthal |
Coverability Analysis Using Symbolic Model Checking. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Javier Esparza, Claus Schröter |
Net Reductions for LTL Model-Checking. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
1 | 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. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Huibiao Zhu, Jonathan P. Bowen, Jifeng He 0001 |
From Operational Semantics to Denotational Semantics for Verilog. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Berg, Christian Jacobi 0002 |
Formal Verification of the VAMP Floating Point Unit. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Mark D. Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones |
A Framework for Microprocessor Correctness Statements. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Karen Yorav, Sagi Katz, Ron Kiper |
Reproducing Synchronization Bugs with Model Checking. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Robert Beers, Rajnish Ghughal, Mark D. Aagaard |
Applications of Hierarchical Verification in Model Checking. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Alan Mycroft, Richard Sharp |
Hardware Synthesis Using SAFL and Application to Processor Design. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Ofer Strichman |
Pruning Techniques for the SAT-Based Bounded Model Checking Problem. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Ji He, Kenneth J. Turner |
Specifying Hardware Timing with ET-L OTOS. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Koen Claessen, Mary Sheeran, Satnam Singh |
The Design and Verification of a Sorter Core. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Enrico Tronci, Giuseppe Della Penna, Benedetto Intrigila, Marisa Venturini Zilli |
Exploiting Transition Locality in Automatic Verification. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Jayanta Bhadra, Andrew K. Martin, Jacob A. Abraham, Magdy S. Abadir |
Using Abstract Specifications to Verify PowerPCTM Custom Memories by Symbolic Trajectory Evaluation. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
1 | M. Oliver Möller, Rajeev Alur |
Heuristics for Hierarchical Partitioning with Application to Model Checking. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Mark D. Aagaard, Thomas F. Melham, John W. O'Leary |
Xs are for Trajectory Evaluation, Booleans are for Theorem Proving. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Sagi Katz, Orna Grumberg, Daniel Geist |
"Have I written enough Properties?" - A Method of Comparison between Specification and Implementation. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Edmund M. Clarke, Somesh Jha, Yuan Lu 0004, Dong Wang |
Abstract BDDs: A Technique for Using Abstraction in Model Checking. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
Abstract BDDs, Model checking and abstraction |
1 | Klaus Schneider 0001 |
Yet another Look at the LTL Model Checking. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Jens Chr. Godesken |
Fault Models for Embedded Systems (Extended Abstract). |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Byron Cook, John Launchbury, John Matthews, Richard B. Kieburtz |
Formal Verification of Explicitly Parallel Microprocessors. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Gerd Ritter, Hans Eveking, Holger Hinrichsen |
Formal Verification of Designs with Complex Control by Symbolic Simulation. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Dirk W. Hoffmann, Thomas Kropf |
Automatic Error Correction of Large Circuits Using Boolean Decomposition and Abstraction. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
Automatic error correction, design error diagnosis, formal methods, equivalence checking |
1 | Gérard Berry |
Esterel and Jazz: Two Synchronous Languages for Circuit Design (Abstract). |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Kenneth L. McMillan |
Verification of Infinite State Systems by Compositional Model Checking. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Kenneth L. McMillan |
Circular Compositional Reasoning about Liveness. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Yuan Yu, Panagiotis Manolios, Leslie Lamport |
Model Checking TLA+ Specifications. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | 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. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Aarti Gupta, Pranav Ashar, Sharad Malik |
Exploiting Retiming in a Guided Simulation Based Validation Methodology. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | E. Allen Emerson, Richard J. Trefler |
From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Peter Jansen 0003 |
Design Process of Embedded Automotive Systems - Using Model Checking for Correct Specification. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | George Economakos, George K. Papakonstantinou |
Refinement and Property Checking in High-Level Synthesis using Attribute Grammars. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Nina Amla, E. Allen Emerson, Kedar S. Namjoshi |
Efficient Decompositional Model Checking for Regular Timing Diagrams. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Marius Bozga, Oded Maler, Stavros Tripakis |
Efficient Verification of Timed Automata Using Dense and Discrete Time Semantics. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Orna Kupferman, Moshe Y. Vardi |
Vacuity Detection in Temporal Model Checking. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Cindy Eisner |
Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Nancy A. Day, Jeffrey R. Lewis, Byron Cook |
Symbolic Simulation of Microprocessor Models using Type Classes in Haskell. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Edmund M. Clarke, Masahiro Fujita, Sreeranga P. Rajan, Thomas W. Reps, Subash Shankar, Tim Teitelbaum |
Program Slicing of Hardware Description Languages. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Hüsnü Yenigün, Vladimir Levin, Doron A. Peled, Peter A. Beerel |
Hazard-Freedom Checking in Speed-Independent Systems. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Jürgen Ruf, Thomas Kropf |
Modleing and Checking Networks of Communicating Real-Time Process. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Miroslav N. Velev, Randal E. Bryant |
Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Steven D. Johnson, Yanhong A. Liu, Yuchen Zhang |
A Systematic Incrementalization Technique and Its Application to Hardware Design. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
design derivation, floating point operations, Formal methods, hardware verification, formal synthesis, transformational programming |
1 | Klaus Schneider 0001, Michaela Huhn, George Logothetis |
Validation of Object-Oriented Concurrent Designs by Model Checking. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Jun Sawada, Warren A. Hunt Jr. |
Results of the Verification of a Complex Pipelined Machine Model. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Stefan Hendricx, Luc J. M. Claesen |
Verification of Finite-State-Machine Refinements Using a Symbolic Methodology. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Kathi Fisler, Moshe Y. Vardi |
Bisimulation and Model Checking. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam K. Srivas |
A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm without a Reorder Buffer. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Kavita Ravi, Fabio Somenzi |
Hints to accelerate Symbolic Traversal. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Laurence Pierre, Thomas Kropf (eds.) |
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 |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Christian Blumenröhr, Viktor K. Sabelfeld |
Formal Synthesis at the Algorithmic Level. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Ganesh Gopalakrishnan, Rajnish Ghughal, Ravi Hosabettu, Abdelillah Mokkedem, Ratan Nalumasu |
Formal modeling and validation applied to a commercial coherent bus: a case study. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Xiaoshan Li, Antonio Cau, Ben C. Moszkowski, Nick Coleman, Hussein Zedan |
Proving the correctness of the interlock mechanism in processor design. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Willem Visser, Howard Barringer, Donal Fellows, Graham Gough, Alan R. Williams |
Efficient CTL* model checking for analysis of rainbow designs. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Steven D. Johnson, Paul S. Miner |
Integrated reasoning support in system design: design derivation and theorem proving. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | George Economakos, George K. Papakonstantinou, Kiamal Z. Pekmestzi, Panayotis Tsanakas |
Hardware compilation using attribute grammars. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Jürgen Ruf, Thomas Kropf |
Symbolic model checking for a discrete clocked temporal logic with intervals. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Mario Baldi, Fulvio Corno, Maurizio Rebaudengo, Paolo Prinetto, Matteo Sonza Reorda, Giovanni Squillero |
Simulation-based verification of network protocols performance. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Carlos M. Roman |
Is there a crisis in hardware verification? |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Otmane Aït Mohamed, Xiaoyu Song, Eduard Cerny |
On the non-termination of MDGs-based abstract state enumeration. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | David Déharbe, Anamaria Martins Moreira |
Using induction and BDDs to model check invariants. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Matthias Mutz |
Automatic post-synthesis verification support for a high level synthesis step by using the HOL theorem proving system. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Natividad Martínez Madrid, Peter T. Breuer, Carlos Delgado Kloos |
A semantic model for VHDL-AMS. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Hon Fung Li, David K. Probst (eds.) |
Advances in Hardware Design and Verification, IFIP WG 10.5 International Conference on Correct Hardware Design and Verification Methods, 16-18 October 1997, Montréal, Québec, Canada |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Gianpiero Cabodi, Paolo Camurati, Antonio Lioy, Massimo Poncino, Stefano Quer |
A parallel approach to symbolic traversal based on set partitioning. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Werner Damm, Amir Pnueli |
Verifying out-of-order executions. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Allan Silburt |
ASIC/system hardware verification at Nortel: a view from the trenches. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Stefan Höreth |
Implementation of a multiple-domain decision diagram package. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Carlos M. Roman, Gary De Palma, Robert P. Kurshan |
Model checking without hardware drivers. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Subash Shankar, James R. Slagle |
A polymodal semantics for VHDL. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Roger B. Hughes |
CheckOff-M: model checking and its role in IP. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Dominique Borrione, F. Vestman, H. Bouamama |
An approach to Verilog-VHDL interoperability for synchronous designs. |
CHARME |
1997 |
DBLP BibTeX RDF |
|
1 | Serdar Tasiran, Ramin Hojati, Robert K. Brayton |
Language containment of non-deterministic omega-automata. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Oded Maler, Amir Pnueli |
Timing analysis of asynchronous circuits using timed automata. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Emmanuelle Encrenaz |
A Symbolic Relation for a Subset of VHDL'87 Descriptions and its Application to Symbolic Model Checking. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Ulrich Stern, David L. Dill |
Improved probabilistic verification by hash compaction. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Michael C. McFarland, Thaddeus J. Kowalski |
Symbolic analysis and verification of CPA descriptions. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Ulrich Stern, David L. Dill |
Automatic verification of the SCI cache coherence protocol. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Paolo Camurati, Hans Eveking (eds.) |
Correct Hardware Design and Verification Methods, IFIP WG 10.5 Advanced Research Working Conference, CHARME '95, Frankfurt/Main, Germany, October 2-4, 1995, Proceedings |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Ayman M. Wahba, Dominique Borrione |
Design error diagnosis in sequential circuits. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Francisco Corella, Michel Langevin, Eduard Cerny, Zijian Zhou 0001, Xiaoyu Song |
State enumeration with abstract descriptions of state machines. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Ana Cristina Vieira de Melo, Howard Barringer |
A foundation for formal reuse of hardware. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Laurence Pierre |
Describing and verifying synchronous circuits with the Boyer-Moore theorem prover. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Paul Curzon |
Problems encountered in the machine-assisted proof of hardware. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Howard Barringer, Graham Gough, Brian Monahan, Alan R. Williams |
Formal support for the ELLA hardwar description language. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | David Déharbe, Dominique Borrione |
Semantics of a verification-oriented subset of VHDL. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Hardi Hungar, Orna Grumberg, Werner Damm |
What if model checking must be truly symbolic. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Dirk Eisenbiegler, Ramayya Kumar |
Formally embedding existing high level synthesis algorithms. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Dominique Bolignano |
A partial-order approach to the verification of concurrent systems: checking liveness properties. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Kees G. W. Goossens |
Reasoning about VHDL using operational and observational semantics. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Rocco De Nicola, Alessandro Fantechi, Stefania Gnesi, Salvatore Larosa, Gioia Ristori |
Verifying hardware components within JACK. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Li-Guo Wang, Michael Mendler |
Formal design of a class of computers. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Gianpiero Cabodi, Stefano Quer, Paolo Camurati |
Transforming boolean relations by symbolic encoding. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Bhaskar Bose, Steven D. Johnson |
DDD-FM9001: Derivation of a Verified Microprocessor. |
CHARME |
1993 |
DBLP DOI BibTeX RDF |
|
1 | Per Bojsen |
An Approach to Formalization of Data Flow Graphs. |
CHARME |
1993 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Kropf, Ramayya Kumar, Klaus Schneider 0001 |
Embedding Hardware Verification Within a Commercial Design Framework. |
CHARME |
1993 |
DBLP DOI BibTeX RDF |
|
1 | Viktor Cingel |
A Graph-Based Method for Timing Diagrams Representation and Verification. |
CHARME |
1993 |
DBLP DOI BibTeX RDF |
|
1 | Andrew M. Bailey |
Automatic Verification of Speed-Independent Circuit Designs Using the Circal System. |
CHARME |
1993 |
DBLP DOI BibTeX RDF |
|
1 | Gianpiero Cabodi, Paolo Camurati |
Advancements in Symbolic Traversal Technique. |
CHARME |
1993 |
DBLP DOI BibTeX RDF |
|
1 | P. A. Subrahmanyam |
Towards Verifying Large(r) Systems: A Strategy and an Experiment. |
CHARME |
1993 |
DBLP DOI BibTeX RDF |
|
1 | George J. Milne, Laurence Pierre (eds.) |
Correct Hardware Design and Verification Methods, IFIP WG 10.5 Advanced Research Working Conference, CHARME '93, Arles, France, May 24-26, 1993, Proceedings |
CHARME |
1993 |
DBLP DOI BibTeX RDF |
|