| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | William D. Young |
Introducing Abstractions via Rewriting.  |
CHARME  |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Oliver Pell, Wayne Luk |
Resolving Quartz Overloading. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Mona Safar, M. Watheq El-Kharashi, Ashraf Salem |
FPGA Based Accelerator for 3-SAT Conflict Analysis in SAT Solvers. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Wolfram Büttner |
Is Formal Verification Bound to Remain a Junior Partner of Simulation? |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Emil Axelsson, Koen Claessen, Mary Sheeran |
Wired: Wire-Aware Circuit Design. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Dominique Borrione, Wolfgang J. Paul (eds.) |
Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005, Proceedings |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Ferdinand, Reinhold Heckmann |
Verifying Timing Behavior by Abstract Interpretation of Executable Code. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Hana Chockler, Kathi Fisler |
Temporal Modalities for Concisely Capturing Timing Diagrams. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Viresh Paruthi, Christian Jacobi 0002, Kai Weber 0001 |
Efficient Symbolic Simulation via Dynamic Scheduling, Don't Caring, and Case Splitting. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Emmanuel Zarpas |
A Case Study: Formal Verification of Processor Critical Properties. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Liang Zhang 0012, Mukul R. Prasad, Michael S. Hsiao |
Interleaved Invariant Checking with Dynamic Abstraction. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Arindam Chakrabarti, Krishnendu Chatterjee, Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar |
Verifying Quantitative Properties Using Bound Functions. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Subramanian K. Iyer, Jawahar Jain, Mukul R. Prasad, Debashis Sahoo, Thomas Sidle |
Error Detection Using BMC in a Parallel Environment. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | David Ward, Fabio Somenzi |
Automatic Generation of Hints for Symbolic Traversal. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Masahiro Fujita |
Behavior-RTL Equivalence Checking Based on Data Transfer Analysis with Virtual Controllers and Datapaths. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Ritwik Bhattacharya, Steven M. German, Ganesh Gopalakrishnan |
Symbolic Partial Order Reduction for Rule Based Transition Systems. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Tsachy Kapschitz, Ran Ginosar |
Formal Verification of Synchronizers. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Doron Bustan, Alon Flaisher, Orna Grumberg, Orna Kupferman, Moshe Y. Vardi |
Regular Vacuity. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | ShengYu Shen, Ying Qin, Sikun Li |
Minimizing Counterexample of ACTL Property. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev |
Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Große, Rolf Drechsler |
Acceleration of SAT-Based Iterative Property Checking. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Jan-Willem Roorda, Koen Claessen |
A New SAT-Based Algorithm for Symbolic Trajectory Evaluation. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Katell Morin-Allory, David Cachera |
Proving Parameterized Systems: The Use of Pseudo-Pipelines in Polyhedral Logic. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill, E. Allen Emerson |
Predictive Reachability Using a Sample-Based Approach. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Panagiotis Manolios, Sudarshan K. Srinivasan |
A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Jason Baumgartner, Hari Mony |
Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization Strategies. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Warren A. Hunt Jr., Erik Reeber |
Formalization of the DE2 Language. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas In der Rieden, Dirk Leinenbach, Wolfgang J. Paul |
Towards the Pervasive Verification of Automotive Systems. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Leslie Lamport |
Real-Time Model Checking Is Really Simple. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Iakov Dalinger, Mark A. Hillebrand, Wolfgang J. Paul |
On the Verification of Memory Management Mechanisms. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Sudhindra Pandav, Konrad Slind, Ganesh Gopalakrishnan |
Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Staber, Barbara Jobstmann, Roderick Bloem |
Finding and Fixing Faults. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Masaharu Imai, Akira Kitajima |
Verification Challenges in Configurable Processor Design with ASIP Meister. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Gianfranco Ciardo, Andy Jinqing Yu |
Saturation-Based Symbolic Reachability Analysis Using Conjunctive and Disjunctive Partitioning. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Biniam Gebremichael, Frits W. Vaandrager, Miaomiao Zhang, Kees Goossens, Edwin Rijpkema, Andrei Radulescu |
Deadlock Prevention in the Æthereal Protocol. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Hari Mony, Jason Baumgartner, Adnan Aziz |
Exploiting Constraints in Transformation-Based Verification. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Alex Tsow, Steven D. Johnson |
Data Refinement for Synchronous System Specification and Construction. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | João Marques-Silva 0001 |
Improvements to the Implementation of Interpolant-Based Model Checking. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Petr Matousek, Ales Smrcka, Tomás Vojnar |
High-Level Modelling, Analysis, and Verification on FPGA-Based Hardware Design. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Ou Wei, Arie Gurfinkel, Marsha Chechik |
Identification and Counter Abstraction for Full Virtual Symmetry. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Arie Gurfinkel, Marsha Chechik |
How Thorough Is Thorough Enough? |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Nina Amla, Xiaoqun Du, Andreas Kuehlmann, Robert P. Kurshan, Kenneth L. McMillan |
An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg, Tamir Heyman, Nili Ifergan, Assaf Schuster |
Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Sagar Chaki, Edmund M. Clarke, Alex Groce, Ofer Strichman |
Predicate Abstraction with Minimum Predicates. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Lennart Beringer |
A Programming Language Based Analysis of Operand Forwarding. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Langberg, Amir Pnueli, Yoav Rodeh |
The ROBDD Size of Simple CNF Formulas. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Panagiotis Manolios |
A Compositional Theory of Refinement for Branching Time. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael J. C. Gordon, Joe Hurd, Konrad Slind |
Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Warren A. Hunt Jr., Robert Bellarmine Krug, J Strother Moore |
Linear and Nonlinear Arithmetic in ACL2. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Mary Sheeran |
Finding Regularity: Describing and Analysing Circuits That Are Not Quite Regular. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | E. Allen Emerson, Thomas Wahl |
On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Wolfgang Roesner |
What Is beyond the RTL Horizon for Microprocessor and System Design? |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, Marisa Venturini Zilli |
Integrating RAM and Disk Based Verification within the Mur-phi Verifier. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Charles Hymans |
Design and Implementation of an Abstract Interpreter for VHDL. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Sebastiani, Stefano Tonetta |
"More Deterministic" vs. "Smaller" Büchi Automata for Efficient LTL Model Checking. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Sharon Barner, Ishai Rabinovitz |
Effcient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Malay K. Ganai, Aarti Gupta, Zijiang Yang 0006, Pranav Ashar |
Efficient Distributed SAT and SAT-Based Distributed Bounded Model Checking. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Rachel Tzoref, Mark Matusevich, Eli Berger, Ilan Beer |
An Optimized Symbolic Bounded Model Checking Engine. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Subramanian K. Iyer, Debashis Sahoo, Christian Stangier, Amit Narayan, Jawahar Jain |
Improved Symbolic Verification Using Partitioning Techniques. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Geist |
The PSL/Sugar Specification Language A Language for all Seasons. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Ghiath Al Sammane, Diana Toma, Julien Schmaltz, Pierre Ostier, Dominique Borrione |
Constrained Symbolic Simulation with Mathematica and ACL2. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabio Somenzi |
The Charme of Abstract Entities. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Enric Pastor, Marco A. Peña |
Efficient Hybrid Reachability Analysis for Asynchronous Concurrent Systems. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, Marisa Venturini Zilli |
Finite Horizon Analysis of Markov Chains with the Mur-phi Verifier. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | E. Allen Emerson, Vineet Kahlon |
Exact and Efficient Verification of Parameterized Cache Coherence Protocols. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Satnam Singh |
Design and Verification of CoreConnectTM IP Using Esterel. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Geist, Enrico Tronci (eds.) |
Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Husam Abu-Haimed, Sergey Berezin, David L. Dill |
Semi-formal Verification of Memory Systems by Symbolic Simulation. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Kathi Fisler |
Towards Diagrammability and Efficiency in Event Sequence Languages. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia |
Convergence Testing in Term-Level Bounded Model Checking. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Sankar Gurumurthy, Orna Kupferman, Fabio Somenzi, Moshe Y. Vardi |
On Complementing Nondeterministic Büchi Automata. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Alan J. Hu, Jeremy Casas, Jin Yang 0006 |
Reasoning about GSTE Assertion Graphs. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Hana Chockler, Orna Kupferman, Moshe Y. Vardi |
Coverage Metrics for Formal Verification. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Mohamed Layouni, Jozef Hooman, Sofiène Tahar |
On the Correctness of an Intrusion-Tolerant Group Communication Protocol. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Sven Beyer, Christian Jacobi 0002, Daniel Kroening, Dirk Leinenbach, Wolfgang J. Paul |
Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, Konrad Slind |
Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Cédric Roux, Emmanuelle Encrenaz |
CTL May Be Ambiguous When Model Checking Moore Machines. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Mark D. Aagaard |
A Hazards-Based Correctness Statement for Pipelined Circuits. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | J Strother Moore |
Inductive Assertions and Operational Semantics. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | François Siewe, Dang Van Hung |
Deriving Real-Time Programs from Duration Calculus Specifications. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
Continuous specification, discrete design, Hoare triples, concurrency, real-time program, shared variables |
| 1 | Roope Kaivola, Katherine R. Kohatsu |
Proof Engineering in the Large: Formal Verification of Pentium® 4 Floating-Point Divider. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Dirk Beyer 0001 |
Efficient Reachability Analysis and Refinement Checking of Timed Automata Using BDDs. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
Real-time systems, Formal verification, Timed Automata |
| 1 | Eric Gascard, Laurence Pierre |
Induction-Oriented Formal Verification in Symmetric Interconnection Networks. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Ricky W. Butler, Victor Carreño, Gilles Dowek, César A. Muñoz |
Formal Verification of Conflict Detection Algorithms. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Gérard Berry, Ellen Sentovich |
Multiclock Esterel. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Richard Sharp, Alan Mycroft |
A Higher-Level Language for Hardware Synthesis. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Steven D. Johnson |
View from the Fringe of the Fringe. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Iskander Kort, Sofiène Tahar, Paul Curzon |
Hierarchical Verification Using an MDG-HOL Hybrid Tool. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Steve McKeever, Wayne Luk |
Towards Provably-Correct Hardware Compilation Tools Based on Pass Separation Techniques. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Tiziana Margaria, Thomas F. Melham (eds.) |
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 |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Tiberiu Seceleanu, Juha Plosila |
Formal Pipeline Design. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Xiaohua Kong, Radu Negulescu, Larry Weidong Ying |
Refinement-Based Formal Verification of Asynchronous Wrappers for Independently Clocked Domains in Systems on Chip. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth J. Turner, Ji He |
Formally-Based Design Evaluation. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Alvin R. Albrecht, Alan J. Hu |
Register Transformations with Multiple Clock Domains. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Xuandong Li, Yu Pei 0001, Jianhua Zhao, Yong Li 0005, Tao Zheng, Guoliang Zheng |
Efficient Verification of a Class of Linear Hybrid Automata Using Linear Programming. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Pankaj Chauhan, Edmund M. Clarke, Somesh Jha, James H. Kukula, Helmut Veith, Dong Wang |
Using Combinatorial Optimization Methods for Quantification Scheduling. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Fady Copty, Amitai Irron, Osnat Weissberg, Nathan P. Kropp, Gila Kamhi |
Efficient Debugging in a Formal Verification Environment. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajesh Radhakrishnan, Elena Teica, Ranga Vemuri |
Verification of Basic Block Schedules Using RTL Transformations. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Anthony Winstanley, Mark R. Greenstreet |
Temporal Properties of Self-Timed Rings. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license