default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID12. CHARME 2003: L'Aquila, Italy
- Daniel Geist, Enrico Tronci:
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. Lecture Notes in Computer Science 2860, Springer 2003, ISBN 3-540-20363-X
Invited Talks
- Wolfgang Roesner:
What Is beyond the RTL Horizon for Microprocessor and System Design? 1 - Fabio Somenzi:
The Charme of Abstract Entities. 2
Tutorial
- Daniel Geist:
The PSL/Sugar Specification Language A Language for all Seasons. 3
Software Verification
- Mary Sheeran:
Finding Regularity: Describing and Analysing Circuits That Are Not Quite Regular. 4-18 - Sagar Chaki, Edmund M. Clarke, Alex Groce, Ofer Strichman
:
Predicate Abstraction with Minimum Predicates. 19-34 - Sharon Barner, Ishai Rabinovitz:
Effcient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning. 35-50
Processor Verification
- Sven Beyer, Christian Jacobi, Daniel Kroening, Dirk Leinenbach, Wolfgang J. Paul:
Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP. 51-65 - Mark D. Aagaard:
A Hazards-Based Correctness Statement for Pipelined Circuits. 66-80 - Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, Konrad Slind:
Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT. 81-95
Automata Based Methods
- Sankar Gurumurthy, Orna Kupferman, Fabio Somenzi, Moshe Y. Vardi:
On Complementing Nondeterministic Büchi Automata. 96-110 - Hana Chockler, Orna Kupferman, Moshe Y. Vardi:
Coverage Metrics for Formal Verification. 111-125 - Roberto Sebastiani, Stefano Tonetta:
"More Deterministic" vs. "Smaller" Büchi Automata for Efficient LTL Model Checking. 126-140
Short Papers 1
- Rachel Tzoref, Mark Matusevich, Eli Berger, Ilan Beer:
An Optimized Symbolic Bounded Model Checking Engine. 141-149 - Ghiath Al Sammane, Diana Toma, Julien Schmaltz, Pierre Ostier, Dominique Borrione:
Constrained Symbolic Simulation with Mathematica and ACL2. 150-157 - Husam Abu-Haimed, Sergey Berezin, David L. Dill:
Semi-formal Verification of Memory Systems by Symbolic Simulation. 158-163 - Cédric Roux, Emmanuelle Encrenaz:
CTL May Be Ambiguous When Model Checking Moore Machines. 164-169
Specification Methods
- Alan J. Hu, Jeremy Casas, Jin Yang:
Reasoning about GSTE Assertion Graphs. 170-184 - Kathi Fisler:
Towards Diagrammability and Efficiency in Event Sequence Languages. 185-199 - Michael J. C. Gordon, Joe Hurd, Konrad Slind:
Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving. 200-215
Protocol Verification
- E. Allen Emerson, Thomas Wahl:
On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking. 216-230 - Mohamed Layouni, Jozef Hooman, Sofiène Tahar:
On the Correctness of an Intrusion-Tolerant Group Communication Protocol. 231-246 - E. Allen Emerson, Vineet Kahlon:
Exact and Efficient Verification of Parameterized Cache Coherence Protocols. 247-262
Short Papers 2
- Charles Hymans:
Design and Implementation of an Abstract Interpreter for VHDL. 263-269 - Lennart Beringer:
A Programming Language Based Analysis of Operand Forwarding. 270-276 - Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, Marisa Venturini Zilli:
Integrating RAM and Disk Based Verification within the Mur-phi Verifier. 277-282 - Satnam Singh:
Design and Verification of CoreConnectTM IP Using Esterel. 283-288
Theorem Proving
- J Strother Moore:
Inductive Assertions and Operational Semantics. 289-303 - Panagiotis Manolios:
A Compositional Theory of Refinement for Branching Time. 304-318 - Warren A. Hunt Jr., Robert Bellarmine Krug, J Strother Moore:
Linear and Nonlinear Arithmetic in ACL2. 319-333
Bounded Model Checking
- Malay K. Ganai, Aarti Gupta, Zijiang Yang, Pranav Ashar:
Efficient Distributed SAT and SAT-Based Distributed Bounded Model Checking. 334-347 - Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia:
Convergence Testing in Term-Level Bounded Model Checking. 348-362 - Michael Langberg, Amir Pnueli, Yoav Rodeh:
The ROBDD Size of Simple CNF Formulas. 363-377
Model Checking and Application
- Enric Pastor, Marco A. Peña:
Efficient Hybrid Reachability Analysis for Asynchronous Concurrent Systems. 378-393 - Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, Marisa Venturini Zilli:
Finite Horizon Analysis of Markov Chains with the Mur-phi Verifier. 394-409 - Subramanian K. Iyer, Debashis Sahoo, Christian Stangier, Amit Narayan, Jawahar Jain:
Improved Symbolic Verification Using Partitioning Techniques. 410-424
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 2025-02-24 21:37 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:
