Search results for "CHARME"

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

Publications at "CHARME"( http://dblp.L3S.de/Venues/CHARME )