Tools and algorithms for the construction and analysis of systems. 10th international conference, TACAS 2004, held as part of the joint conferences on theory and practice of software, ETAPS 2004, Barcelona, Spain, March 29 -- April 2, 2004. Proceedings. (Q1881365)

The articles of this volume will be reviewed individually. The preceding conference has been reviewed (see Zbl 1017.00035) Indexed articles: \textit{Lahiri, Shuvendu K.; Bryant, Randal E.; Goel, Amit; Talupur, Muralidhar}, Revisiting positive equality, 1-15 [Zbl 1126.68570] \textit{McMillan, K. L.}, An interpolating theorem prover, 16-30 [Zbl 1126.68573] \textit{Ravi, Kavita; Somenzi, Fabio}, Minimal assignments for bounded model checking, 31-45 [Zbl 1126.68486] \textit{Younes, Håkan L. S.; Kwiatkowska, Marta; Norman, Gethin; Parker, David}, Numerical vs. statistical probabilistic model checking: an empirical study, 46-60 [Zbl 1126.68490] \textit{Baier, Christel; Haverkort, Boudewijn; Hermanns, Holger; Katoen, Joost-Pieter}, Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes, 61-76 [Zbl 1126.68467] \textit{Alfaro, Luca de; Faella, Marco; Henzinger, Thomas A.; Majumdar, Rupak; Stoelinga, Mariëlle}, Model checking discounted temporal properties, 77-92 [Zbl 1126.68465] \textit{Ball, Thomas; Levin, Vladimir; Xie, Fei}, Automatic creation of environment models via training, 93-107 [Zbl 1126.68468] \textit{Groce, Alex}, Error explanation with distance metrics, 108-122 [Zbl 1126.68477] \textit{Sen, Koushik; Roşu, Grigore; Agha, Gul}, Online efficient predictive safety analysis of multithreaded programs, 123-138 [Zbl 1126.68357] \textit{Diethers, Karsten; Huhn, Michaela}, Vooduu: verification of object-oriented designs using UPPAAL, 139-143 [Zbl 1126.68473] \textit{Piazza, Carla; Pivato, Enrico; Rossi, Sabina}, CoPS -- checker of persistent security, 144-152 [Zbl 1126.68509] \textit{Virtanen, Heikki; Hansen, Henri; Valmari, Antti; Nieminen, Juha; Erkkilä, Timo}, Tampere verification tool, 153-157 [Zbl 1126.68488] \textit{Deng, Xianghua; Dwyer, Matthew B.; Hatcliff, John; Mizuno, Masaaki}, SyncGen: an aspect-oriented framework for synchronization, 158-162 [Zbl 1126.68472] \textit{Müller-Olm, Markus; Yoo, Haiseung}, MetaGame: an animation tool for model-checking games, 163-167 [Zbl 1126.68483] \textit{Clarke, Edmund; Kroening, Daniel; Lerda, Flavio}, A tool for checking ANSI-C programs, 168-176 [Zbl 1126.68470] \textit{Mailund, Thomas; Westergaard, Michael}, Obtaining memory-efficient reachability graph representations using the sweep-line method, 177-191 [Zbl 1126.68506] \textit{Schmidt, Karsten}, Automated generation of a progress measure for the sweep-line method, 192-204 [Zbl 1126.68511] \textit{Geldenhuys, Jaco; Valmari, Antti}, Tarjan's algorithm makes on-the-fly LTL verification more efficient, 205-219 [Zbl 1126.68476] \textit{Rasmussen, J. I.; Larsen, Kim G.; Subramani, K.}, Resource-optimal scheduling using priced timed automata, 220-235 [Zbl 1126.68461] \textit{Krčál, Pavel; Yi, Wang}, Decidable and undecidable problems in schedulability analysis using timed automata, 236-250 [Zbl 1126.68456] \textit{Nielson, Flemming; Nielson, Hanne Riis; Sun, Hongyan; Buchholtz, Mikael; Hansen, René Rydhof; Pilegaard, Henrik; Seidl, Helmut}, The succinct solver suite, 251-265 [Zbl 1126.68354] \textit{Linger, Nathan; Sheard, Tim}, Binding-time analysis for MetaML via type inference and constraint solving, 266-279 [Zbl 1126.68352] \textit{Su, Zhendong; Wagner, David}, A class of polynomially solvable range constraints for interval analysis without widenings and narrowings, 280-295 [Zbl 1126.68358] \textit{Lugiez, D.; Niebert, P.; Zennou, S.}, A partial order semantics approach to the clock explosion problem of timed automata, 296-311 [Zbl 1126.68458] \textit{Behrmann, Gerd; Bouyer, Patricia; Larsen, Kim G.; Pelánek, Radek}, Lower and upper bounds in zone based abstractions of timed automata, 312-326 [Zbl 1126.68453] \textit{Leue, Stefan; Mayr, Richard; Wei, Wei}, A scalable incomplete test for the boundedness of UML RT models, 327-341 [Zbl 1126.68502] \textit{Delzanno, Giorgio; Ganty, Pierre}, Automatic verification of time sensitive cryptographic protocols, 342-356 [Zbl 1126.68392] \textit{Lindsey, A. E.; Pecheur, Charles}, Simulation-based verification of autonomous controllers via Livingstone PathFinder, 357-371 [Zbl 1126.68616] \textit{Beauquier, Danièle; Crolard, Tristan; Prokofieva, Evguenia}, Automatic parametric verification of a root contention protocol based on abstract state machines and first order timed logic, 372-387 [Zbl 1126.68318] \textit{Ball, Thomas; Cook, Byron; Das, Satyaki; Rajamani, Sriram K.}, Refining approximations in software predicate abstraction, 388-403 [Zbl 1126.68344] \textit{Robby; Rodríguez, Edwin; Dwyer, Matthew B.; Hatcliff, John}, Checking strong specifications using an extensible software model checking framework, 404-420 [Zbl 1126.68356] \textit{Abramsky, Samson; Ghica, Dan R.; Murawski, Andrzej S.; Ong, C.-H. Luke}, Applying game semantics to compositional software modeling and verification, 421-435 [Zbl 1126.68343] \textit{Groote, Jan Friso; Keinänen, Misa}, Solving disjunctive/conjunctive Boolean equation systems with alternating fixed points, 436-450 [Zbl 1126.68478] \textit{Gurfinkel, Arie; Chechik, Marsha}, How vacuous is vacuous?, 451-466 [Zbl 1126.68479] \textit{Alur, Rajeev; Etessami, Kousha; Madhusudan, P.}, A temporal logic of nested calls and returns, 467-481 [Zbl 1126.68466] \textit{Fang, Yi; Piterman, Nir; Pnueli, Amir; Zuck, Lenore}, Liveness with incomprehensible ranking, 482-496 [Zbl 1126.68474] \textit{Qian, Kairong; Nymeyer, Albert}, Guided invariant model checking based on abstraction and symbolic pattern databases, 497-511 [Zbl 1126.68484] \textit{Gopan, Denis; DiMaio, Frank; Dor, Nurit; Reps, Thomas; Sagiv, Mooly}, Numeric domains with summarized dimensions, 512-529 [Zbl 1126.68348] \textit{Yorsh, G.; Reps, Thomas; Sagiv, Mooly}, Symbolically computing most-precise abstract operations for shape analysis, 530-545 [Zbl 1126.68359] \textit{Shoham, Sharon; Grumberg, Orna}, Monotonic abstraction-refinement for CTL, 546-560 [Zbl 1126.68487] \textit{Boigelot, Bernard; Legay, Axel; Wolper, Pierre}, Omega-regular model checking, 561-575 [Zbl 1126.68469] \textit{Bardin, Sébastien; Finkel, Alain; Leroux, Jérôme}, Faster acceleration of counter automata in practice, 576-590 [Zbl 1126.68452] \textit{Kupferman, Orna; Vardi, Moshe Y.}, From complementation to certification, 591-606 [Zbl 1126.68481]