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 (Q1416837)

The articles of this volume will be reviewed individually. The preceding conference has been reviewed (see Zbl 0971.00031). Indexed articles: \textit{Sheeran, Mary}, Finding regularity: Describing and analysing circuits that are not quite regular, 4-18 [Zbl 1179.68011] \textit{Chaki, Sagar; Clarke, Edmund; Groce, Alex; Strichman, Ofer}, Predicate abstraction with minimum predicates, 19-34 [Zbl 1179.68033] \textit{Barner, Sharon; Rabinovitz, Ishai}, Efficient symbolic model checking of software using partial disjunctive partitioning, 35-50 [Zbl 1179.68077] \textit{Beyer, Sven; Jacobi, Chris; Kröning, Daniel; Leinenbach, Dirk; Paul, Wolfgang J.}, Instantiating uninterpreted functional units and memory system: Functional verification of the VAMP, 51-65 [Zbl 1179.68009] \textit{Aagaard, Mark D.}, A hazards-based correctness statement for pipelined circuits, 66-80 [Zbl 1179.68008] \textit{Gurumurthy, Sankar; Kupferman, Orna; Somenzi, Fabio; Vardi, Moshe Y.}, On complementing nondeterministic Büchi automata, 96-110 [Zbl 1179.68070] \textit{Chockler, Hana; Kupferman, Orna; Vardi, Moshe Y.}, Coverage metrics for formal verification, 111-125 [Zbl 1179.68080] \textit{Sebastiani, Roberto; Tonetta, Stefano}, ``More deterministic'' vs. ``smaller'' Büchi automata for efficient LTL model checking, 126-140 [Zbl 1179.68095] \textit{Tzoref, Rachel; Matusevich, Mark; Berger, Eli; Beer, Ilan}, An optimized symbolic bounded model checking engine, 141-149 [Zbl 1179.68096] \textit{Sammane, Ghiath Al; Toma, Diana; Schmaltz, Julien; Ostier, Pierre; Borrione, Dominique}, Constrained symbolic simulation with Mathematica and ACL2, 150-157 [Zbl 1179.68094] \textit{Abu-Haimed, Husam; Berezin, Sergey; Dill, David L.}, Semi-formal verification of memory systems by symbolic simulation, 158-163 [Zbl 1179.68075] \textit{Roux, Cédric; Encrenaz, Emmanuelle}, CTL may be ambiguous when model checking Moore machines, 164-169 [Zbl 1179.68093] \textit{Hu, Alan J.; Casas, Jeremy; Yang, Jin}, Reasoning about GSTE assertion graphs, 170-184 [Zbl 1179.68086] \textit{Fisler, Kathi}, Towards diagrammability and efficiency in event sequence languages, 185-199 [Zbl 1179.68083] \textit{Gordon, Mike; Hurd, Joe; Slind, Konrad}, Executing the formal semantics of the Accellera property specification language by mechanised theorem proving, 200-215 [Zbl 1179.68085] \textit{Emerson, E. Allen; Wahl, Thomas}, On combining symmetry reduction and symbolic representation for efficient model checking, 216-230 [Zbl 1179.68082] \textit{Layouni, Mohamed; Hooman, Jozef; Tahar, Sofiène}, On the correctness of an intrusion-tolerant group communication protocol, 231-246 [Zbl 1179.68014] \textit{Emerson, E. Allen; Kahlon, Vineet}, Exact and efficient verification of parameterized cache coherence protocols, 247-262 [Zbl 1179.68013] \textit{Hymans, Charles}, Design and implementation of an abstract interpreter for VHDL, 263-269 [Zbl 1179.68010] \textit{Penna, Giuseppe Della; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Zilli, Marisa Venturini}, Integrating RAM and disk based verification within the Mur\(\varphi\) verifier, 277-282 [Zbl 1179.68091] \textit{Moore, J. Strother}, Inductive assertions and operational semantics, 289-303 [Zbl 1179.68089] \textit{Manolios, Panagiotis}, A compositional theory of refinement for branching time, 304-318 [Zbl 1179.68088] \textit{Hunt, Warren A. jun.; Krug, Robert Bellarmine; Moore, J. Strother}, Linear and nonlinear arithmetic in ACL2, 319-333 [Zbl 1179.68136] \textit{Ganai, Malay K; Gupta, Aarti; Yang, Zijiang; Ashar, Pranav}, Efficient distributed SAT and SAT-based distributed bounded model checking, 334-347 [Zbl 1179.68084] \textit{Bryant, Randal E.; Lahiri, Shuvendu K.; Seshia, Sanjit A.}, Convergence testing in term-level bounded model checking, 348-362 [Zbl 1179.68079] \textit{Langberg, Michael; Pnueli, Amir; Rodeh, Yoav}, The ROBDD size of simple CNF formulas, 363-377 [Zbl 1179.68137] \textit{Pastor, Enric; Peña, Marco A.}, Efficient hybrid reachability analysis for asynchronous concurrent systems, 378-393 [Zbl 1179.68103] \textit{Penna, Giuseppe Della; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Zilli, Marisa Venturini}, Finite horizon analysis of Markov chains with the Mur\(\varphi \) verifier, 394-409 [Zbl 1179.68092] \textit{Iyer, Subramanian; Sahoo, Debashis; Stangier, Christian; Narayan, Amit; Jain, Jawahar}, Improved symbolic verification using partitioning techniques, 410-424 [Zbl 1179.68087]