Computer aided verification. 12th international conference, CAV 2000. Chicago, IL, USA, July 15--19, 2000. Proceedings (Q1572746)

The articles of mathematical interest will be reviewed individually. The preceding conference (11th, 1999) has been indicated (see Zbl 0925.68015). Indexed articles: \textit{Baumgartner, Jason; Tripp, Anson; Aziz, Adnan; Singhal, Vigyan; Andersen, Flemming}, An abstraction algorithm for the verification of generalized \(C\)-slow designs, 5-19 [Zbl 0974.94032] \textit{Heyman, Tamir; Geist, Danny; Grumberg, Orna; Schuster, Assaf}, Achieving scalability in parallel reachability analysis of very large circuits, 20-35 [Zbl 0974.68547] \textit{Kupferman, Orna; Vardi, Moshe Y.}, An automata-theoretic approach to reasoning about infinite-state systems, 36-52 [Zbl 0974.68083] \textit{Delzanno, Giorgio}, Automatic verification of parameterized cache coherence protocols, 53-68 [Zbl 0974.68500] \textit{Dang, Zhe; Ibarra, Oscar H.; Bultan, Tevfik; Kemmerer, Richard A.; Su, Jianwen}, Binary reachability analysis of discrete pushdown timed automata, 69-84 [Zbl 0974.68085] \textit{Bryant, Randal E.; Velev, Miroslav N.}, Boolean satisfiability with transitivity constraints, 85-98 [Zbl 0974.94501] \textit{Ayari, Abdelwaheb; Basin, David}, Bounded model construction for monadic second-order logics, 99-112 [Zbl 0974.68115] \textit{Kukula, James H.; Shiple, Thomas R.}, Building circuits from relations, 113-123 [Zbl 0974.94502] \textit{Williams, Poul F.; Biere, Armin; Clarke, Edmund M.; Gupta, Anubhav}, Combining decision diagrams and SAT procedures for efficient symbolic model checking, 124-138 [Zbl 0974.68526] \textit{Namjoshi, Kedar S.; Trefler, Richard J.}, On the completeness of compositional reasoning, 139-153 [Zbl 0974.68127] \textit{Clarke, Edmund; Grumberg, Orna; Jha, Somesh; Lu, Yuan; Veith, Helmut}, Counterexample-guided abstraction refinement, 154-169 [Zbl 0974.68517] \textit{Ayari, Abdelwaheb; Basin, David; Klaedtke, Felix}, Decision procedures for inductive Boolean functions based on alternating automata, 170-185 [Zbl 0974.94033] \textit{de Alfaro, Luca; Henzinger, Thomas A.; Mang, Freddy Y. C.}, Detecting errors before reaching them, 186-201 [Zbl 0974.68550] \textit{Vöge, Jens; Jurdziński, Marcin}, A discrete strategy improvement algorithm for solving parity games. (Extended abstract), 202-215 [Zbl 0974.68527] \textit{Behrmann, Gerd; Hune, Thomas; Vaandrager, Frits}, Distributing timed model checking -- how the search order matters, 216-231 [Zbl 0974.68518] \textit{Esparza, Javier; Hansel, David; Rossmanith, Peter; Schwoon, Stefan}, Efficient algorithms for model checking pushdown systems, 232-247 [Zbl 0974.68116] \textit{Somenzi, Fabio; Bloem, Roderick}, Efficient Büchi automata form LTL formulae, 248-263 [Zbl 0974.68086] \textit{Stoller, Scott D.; Unnikrishnan, Leena; Liu, Yanhong A.}, Efficient detection of global properties in distributed systems using partial-order methods, 264-279 [Zbl 0974.68501] \textit{Alur, R.; Grosu, R.; McDougall, M.}, Efficient reachability analysis of hierarchical reactive machines, 280-295 [Zbl 0974.68551] \textit{Velev, Miroslav N.}, Formal verification of VLIW microprocessors with speculative execution, 296-311 [Zbl 0974.68554] \textit{McMillan, Kenneth L.; Qadeer, Shaz; Saxe, James B.}, Induction in compositional model checking, 312-327 [Zbl 0974.68520] \textit{Pnueli, Amir; Shahar, Elad}, Liveness and acceleration in parameterized verification, 328-343 [Zbl 0974.68521] \textit{Rusinowitch, Michaël; Stratulat, Sorin; Klay, Francis}, Mechanical verification of an ideal incremental ABR conformance algorithm, 344-357 [Zbl 0974.68559] \textit{Baier, Christel; Haverkort, Boudewijn; Hermanns, Holger; Katoen, Joost-Pieter}, Model checking continuous-time Markov chains by transient analysis, 358-372 [Zbl 0974.68017] \textit{Cassez, Franck; Laroussinie, François}, Model-checking for hybrid systems by quotienting and constraints solving, 373-388 [Zbl 0974.68117] \textit{Fraer, Ranan; Kamhi, Gila; Ziv, Barukh; Vardi, Moshe Y.; Fix, Limor}, Prioritized traversal: Efficient reachability analysis for verification and falsification, 389-402 [Zbl 0974.68572] \textit{Bouajjani, Ahmed; Jonsson, Bengt; Nilsson, Marcus; Touili, Tayssir}, Regular model checking, 403-418 [Zbl 0974.68118] \textit{Annichini, Aurore; Asarin, Eugene; Bouajjani, Ahmed}, Symbolic techniques for parametric reasoning about counter and clock systems, 419-434 [Zbl 0974.68523] \textit{Namjoshi, Kedar S.; Kurshan, Robert P.}, Syntactic program transformations for automatic abstraction, 435-449 [Zbl 0974.68524] \textit{Chan, William}, Temporal-logic queries, 450-463 [Zbl 0974.68525] \textit{Bouyer, Patricia; Dufourd, Catherine; Fleury, Emmanuel; Petit, Antoine}, Are timed automata updatable?, 464-479 [Zbl 0974.68084] \textit{Shtrichman, Ofer}, Tuning SAT checkers for bounded model checking, 480-494 [Zbl 0974.68565] \textit{Abdulla, Parosh Aziz; Iyer, S. Purushothaman; Nylén, Aletta}, Unfoldings of unbounded Petri nets, 495-507 [Zbl 0974.68528] \textit{Rushby, John}, Verification diagrams revisited: Disjunctive invariants for easy verification, 508-520 [Zbl 0974.68566] \textit{Hosabettu, Ravi; Gopalakrishnan, Ganesh; Srivas, Mandayam}, Verifying advanced microarchitectures that support speculation and exceptions, 521-537 [Zbl 0974.68568] \textit{Abarbanel, Yael; Beer, Ilan; Gluhovsky, Leonid; Keidar, Sharon; Wolfsthal, Yaron}, FoCs -- automatic generation of simulation checkers from formal specifications, 538-542 [Zbl 0974.68552] \textit{Bozga, Marius; Fernandez, Jean-Claude; Ghirvu, Lucian; Graf, Susanne; Krimm, Jean-Pierre; Mounier, Laurent}, IF: A validation environment for timed asynchronous systems, 543-547 [Zbl 0974.68556] \textit{Owre, Sam; Rueß, Harald}, Integrating WS1S with PVS, 548-551 [Zbl 0974.68557] \textit{Gunter, Elsa; Kurshan, Robert; Peled, Doron}, PET: An interactive software testing tool, 552-556 [Zbl 0974.68561] \textit{Colby, Christopher; Lee, Peter; Necula, George C.}, A proof-carrying code architecture for Java, 557-560 [Zbl 0974.68546] \textit{Bienmüller, Tom; Damm, Werner; Wittke, Hartmut}, The Statemate verification environment -- making it real, 561-567 [Zbl 0974.68564] \textit{Cohen, Ernie}, TAPS: A first-order verifier for cryptographic protocols, 568-571 [Zbl 0974.68562] \textit{Yoneda, Tomohiro}, VINAS-P: A tool for trace theoretic verification of timed asynchronous circuits, 572-575 [Zbl 0974.68569] \textit{Ramakrishnan, C. R.; Ramakrishnan, I. V.; Smolka, Scott A.; Dong, Yifei; Du, Xiaoqun; Roychoudhury, Abhik; Venkatakrishnan, V. N.}, XMC: A logic-programming-based verification toolset, 576-580 [Zbl 0974.68571]