Tools and algorithms for the construction and analysis of systems. 11th international conference, TACAS 2005, held as part of the joint European conference on theory and practice of software, ETAPS 2005, Edinburgh, UK, April 4--8, 2005. Proceedings. (Q2388070): Difference between revisions

The articles of this volume will be reviewed individually. The preceding conference has been reviewed (see Zbl 1046.68008). Indexed articles: \textit{McMillan, K. L.}, Applications of Craig interpolants in model checking, 1-12 [Zbl 1087.68597] \textit{Bouajjani, Ahmed; Habermehl, Peter; Moro, Pierre; Vojnar, Tomáš}, Verifying programs with dynamic 1-selector-linked structures in regular model checking, 13-29 [Zbl 1087.68585] \textit{Abdulla, Parosh Aziz; Legay, Axel; d'Orso, Julien; Rezine, Ahmed}, Simulation-based iteration of tree transducers, 30-44 [Zbl 1087.68052] \textit{Vardhan, Abhay; Sen, Koushik; Viswanathan, Mahesh; Agha, Gul}, Using language inference to verify omega-regular properties, 45-60 [Zbl 1087.68062] \textit{Alur, Rajeev; Chaudhuri, Swarat; Etessami, Kousha; Madhusudan, P.}, On-the-fly reachability and cycle detection for recursive state machines, 61-76 [Zbl 1087.68581] \textit{Bingham, Jesse; Hu, Alan J.}, Empirically efficient verification for a class of infinite-state systems, 77-92 [Zbl 1087.68584] \textit{Qadeer, Shaz; Rehof, Jakob}, Context-bounded model checking of concurrent software, 93-107 [Zbl 1087.68598] \textit{Isobe, Yoshinao; Roggenbach, Markus}, A generic theorem prover of CSP refinement, 108-123 [Zbl 1087.68592] \textit{Pnueli, Amir; Podelski, Andreas; Rybalchenko, Andrey}, Separating fairness and well-foundedness for the analysis of fair discrete systems, 124-139 [Zbl 1087.68066] \textit{Ranzato, Francesco; Tapparo, Francesco}, An abstract interpretation-based refinement algorithm for strong preservation, 140-156 [Zbl 1087.68058] \textit{Komondoor, Raghavan; Ramalingam, G.; Chandra, Satish; Field, John}, Dependent types for program understanding, 157-173 [Zbl 1087.68544] \textit{Schwoon, Stefan; Esparza, Javier}, A note on on-the-fly verification algorithms, 174-190 [Zbl 1087.68599] \textit{Hammer, Moritz; Knapp, Alexander; Merz, Stephan}, Truly on-the-fly LTL model checking, 191-205 [Zbl 1087.68591] \textit{Kupferman, Orna; Vardi, Moshe Y.}, Complementation constructions for nondeterministic automata on infinite words, 206-221 [Zbl 1087.68050] \textit{Marrero, Will}, Using BDDs to decide CTL, 222-236 [Zbl 1087.68057] \textit{Remke, Anne; Haverkort, Boudewijn R.; Cloth, Lucia}, Model checking infinite-state Markov chains, 237-252 [Zbl 1087.68059] \textit{Etessami, Kousha; Yannakakis, Mihalis}, Algorithmic verification of recursive probabilistic state machines, 253-270 [Zbl 1087.68054] \textit{Grosu, Radu; Smolka, Scott A.}, Monte Carlo model checking, 271-286 [Zbl 1087.68590] \textit{Jin, HoonSang; Han, HyoJung; Somenzi, Fabio}, Efficient conflict analysis for finding all satisfying assignments of a Boolean circuit, 287-300 [Zbl 1087.68631] \textit{Sharma, Babita; Pandya, Paritosh. K.; Chakraborty, Supratik}, Bounded validity checking of interval duration logic, 301-316 [Zbl 1087.68061] \textit{Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; van Rossum, Peter; Schulz, Stephan; Sebastiani, Roberto}, An incremental and layered procedure for the satisfiability of linear arithmetic logic, 317-333 [Zbl 1087.68630] \textit{Leino, K. Rustan M.; Musuvathi, Madan; Ou, Xinming}, A two-tier technique for supporting quantifiers in a lazily proof-explicating theorem prover, 334-348 [Zbl 1087.68632] \textit{Jeannet, Bertrand; Jéron, Thierry; Rusu, Vlad; Zinovieva, Elena}, Symbolic test selection based on approximate analysis, 349-364 [Zbl 1087.68594] \textit{Xie, Tao; Marinov, Darko; Schulte, Wolfram; Notkin, David}, Symstra: A framework for generating object-oriented unit tests using symbolic execution, 365-381 [Zbl 1087.68601] \textit{Emerson, E. Allen; Wahl, Thomas}, Dynamic symmetry reduction, 382-396 [Zbl 1087.68587] \textit{Jain, Himanshu; Ivančić, Franjo; Gupta, Aarti; Ganai, Malay K.}, Localization and register sharing for predicate abstraction, 397-412 [Zbl 1087.68593] \textit{Jiang, Jie-Hong R.}, On some transformation invariants under retiming and resynthesis, 413-428 [Zbl 1087.68595] \textit{Genest, Blaise}, Compositional message sequence charts (CMSCs) are better to implement than MSCs, 429-444 [Zbl 1087.68589] \textit{Kugler, Hillel; Harel, David; Pnueli, Amir; Lu, Yuan; Bontemps, Yves}, Temporal logic for scenario-based specifications, 445-460 [Zbl 1087.68596] \textit{Weimer, Westley; Necula, George C.}, Mining temporal specifications for error detection, 461-476 [Zbl 1087.68600] \textit{Harding, Aidan; Ryan, Mark; Schobbens, Pierre-Yves}, A new algorithm for strategy synthesis in LTL games, 477-492 [Zbl 1087.68020] \textit{Schuppan, Viktor; Biere, Armin}, Shortest counterexamples for symbolic model checking of LTL with past, 493-509 [Zbl 1087.68060] \textit{Genest, Blaise; Kuske, Dietrich; Muscholl, Anca; Peled, Doron}, Snapshot verification, 510-525 [Zbl 1087.68055] \textit{Bao, Tonglaga; Jones, Michael}, Time-efficient model checking with magnetic disk, 526-540 [Zbl 1087.68582] \textit{Suwimonteerabuth, Dejvuth; Schwoon, Stefan; Esparza, Javier}, jMoped: A Java bytecode checker based on Moped, 541-545 [Zbl 1087.68556] \textit{Chen, Feng; Roşu, Grigore}, Java-MOP: A monitoring oriented programming environment for Java, 546-550 [Zbl 1087.68550] \textit{Bouquet, Fabrice; Dadeau, Frédéric; Legeard, Bruno; Utting, Mark}, JML-testing-tools: A symbolic animator for JML specifications using CLP, 551-556 [Zbl 1087.68549] \textit{Margaria, Tiziana; Nagel, Ralf; Steffen, Bernhard}, jETI: A tool for remote tool integration, 557-562 [Zbl 1087.68553] \textit{Keller, Curtis W.; Saha, Diptikalyan; Basu, Samik; Smolka, Scott A.}, FocusCheck: A tool for model checking and debugging sequential C programs, 563-569 [Zbl 1087.68552] \textit{Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen}, SATABS: SAT-based predicate abstraction for ANSI-C, 570-574 [Zbl 1087.68586] \textit{Ganai, Malay K.; Gupta, Aarti; Ashar, Pranav}, DiVer: SAT-based model checking platform for verifying large scale systems, 575-580 [Zbl 1087.68588] \textit{Bergamini, Damien; Descoubes, Nicolas; Joubert, Christophe; Mateescu, Radu}, BISIMULATOR: A modular tool for on-the-fly equivalence checking, 581-585 [Zbl 1087.68583]