Formal methods in computer-aided design. 5th international conference, FMCAD 2004, Austin, Texas, USA, November 15--17, 2004. Proceedings. (Q1780835)

The articles of this volume will be reviewed individually. The preceding conference has been reviewed (see Zbl 1007.00055). Indexed articles: \textit{Sheeran, Mary}, Generating fast multipliers using clever circuits, 6-20 [Zbl 1117.68305] \textit{Dang, Thao; Donzé, Alexandre; Maler, Oded}, Verification of analog and mixed-signal circuits using hybrid system techniques, 21-36 [Zbl 1117.68303] \textit{Akbarpour, Behzad; Tahar, Sofiène}, A methodology for the formal verification of FFT algorithms in HOL, 37-51 [Zbl 1117.68484] \textit{Schmaltz, Julien; Borrione, Dominique}, A functional approach to the formal specification of networks on chip, 52-66 [Zbl 1117.68304] \textit{Ray, Sandip; Moore, J. Strother}, Proof styles in operational semantics, 67-81 [Zbl 1117.68419] \textit{Manolios, Panagiotis; Vroon, Daron}, Integrating reasoning about ordinal arithmetic into ACL2, 82-97 [Zbl 1117.68485] \textit{Aagaard, Mark D.; Ciubotariu, Vlad C.; Higgins, Jason T.; Khalvati, Farzad}, Combining equivalence verification and completion functions, 98-112 [Zbl 1117.68300] \textit{Aagaard, Mark D.; Day, Nancy A.; Jones, Robert B.}, Synchronization-at-retirement for pipeline verification, 113-127 [Zbl 1117.68301] \textit{Arditi, Laurent; Berry, Gerard; Kishinevsky, Michael}, Late design changes (ECOs) for sequentially optimized Esterel designs, 128-143 [Zbl 1117.68302] \textit{Moon, In-Ho; Pixley, Carl}, Non-miter-based combinational equivalence checking by comparing BDDs with different variable orders, 144-158 [Zbl 1117.68535] \textit{Mony, Hari; Baumgartner, Jason; Paruthi, Viresh; Kanzelman, Robert; Kuehlmann, Andreas}, Scalable automated verification via expert-system guided transformations, 159-173 [Zbl 1117.68534] \textit{Zarpas, Emmanuel}, Simple yet efficient improvements of SAT based bounded model checking, 174-185 [Zbl 1117.68439] \textit{Latvala, Timo; Biere, Armin; Heljanko, Keijo; Junttila, Tommi}, Simple bounded LTL model checking, 186-200 [Zbl 1117.68432] \textit{Giunchiglia, Enrico; Narizzano, Massimo; Tacchella, Armando}, QuBE++: An efficient QBF solver, 201-213 [Zbl 1117.68488] \textit{Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa}, Bounded probabilistic model checking with the Mur\(\varphi\) verifier, 214-229 [Zbl 1117.68425] \textit{Awedh, Mohammad; Somenzi, Fabio}, Increasing the robustness of bounded model checking by computing lower bounds on the reachable states, 230-244 [Zbl 1117.68421] \textit{Cimatti, Alessandro; Roveri, Marco; Sheridan, Daniel}, Bounded verification of past LTL, 245-259 [Zbl 1117.68424] \textit{Amla, Nina; McMillan, Ken L.}, A hybrid of counterexample-based and proof-based abstraction, 260-274 [Zbl 1117.68420] \textit{Grumberg, Orna; Schuster, Assaf; Yadgar, Avi}, Memory efficient all-solutions SAT solver and its application for reachability analysis, 275-289 [Zbl 1117.68429] \textit{Nopper, Tobias; Scholl, Christoph}, Approximate symbolic model checking for incomplete designs, 290-305 [Zbl 1117.68434] \textit{Gurfinkel, Arie; Chechik, Marsha}, Extending extended vacuity, 306-321 [Zbl 1117.68430] \textit{Samer, Marko; Veith, Helmut}, Parameterized vacuity, 322-336 [Zbl 1117.68436] \textit{Claessen, Koen; Mårtensson, Johan}, An operational semantics for Weak PSL, 337-351 [Zbl 1117.68418] \textit{Brim, Luboš; Černá, Ivana; Moravec, Pavel; Šimša, Jiří}, Accepting predecessors are better than back edges in distributed LTL model-checking, 352-366 [Zbl 1117.68422] \textit{Dillinger, Peter C.; Manolios, Panagiotis}, Bloom filters in probabilistic verification, 367-381 [Zbl 1117.68426] \textit{Chou, Ching-Tsun; Mannava, Phanindra K.; Park, Seungjoon}, A simple method for parameterized verification of cache coherence protocols, 382-398 [Zbl 1117.68423] \textit{Sahoo, Debashis; Iyer, Subramanian; Jain, Jawahar; Stangier, Christian; Narayan, Amit; Dill, David L.; Emerson, E. Allen}, A partitioning methodology for BDD-based verification, 399-413 [Zbl 1117.68435] \textit{Stangier, Christian; Sidle, Thomas}, Invariant checking combining forward and backward traversal, 414-429 [Zbl 1117.68437] \textit{Yang, Zijiang; Alur, Rajeev}, Variable reuse for efficient image computation, 430-444 [Zbl 1117.68438]