Tools and algorithms for the construction and analysis of systems. 9th international conference TACAS 2003, held as part of the joint European conferences on theory and practice of software, ETAPS 2003, Warsaw, Poland, April 7--11, 2003. Proceedings
The articles of this volume will be reviewed individually. The preceding conference has been reviewed (see Zbl 0988.00082). Indexed articles: \textit{Lee, Peter}, What are we trying to prove? Reflections on experiences with proof-carrying code, 1 [Zbl 1031.68793] \textit{McMillan, Kenneth L.; Amla, Nina}, Automatic abstraction without counterexamples, 2-17 [Zbl 1031.68520] \textit{Benedetti, Marco; Cimatti, Alessandro}, Bounded model checking for past LTL, 18-33 [Zbl 1031.68077] \textit{Amla, Nina; Kurshan, Robert; McMillan, Kenneth L.; Medel, Ricardo}, Experimental analysis of different techniques for bounded model checking, 34-48 [Zbl 1031.68541] \textit{Henzinger, Thomas A.; Kupferman, Orna; Majumdar, Rupak}, On the universal and existential fragments of the \(\mu\)-calculus, 49-64 [Zbl 1031.68080] \textit{Armoni, Roy; Bustan, Doron; Kupferman, Orna; Vardi, Moshe Y.}, Resets vs. aborts in linear temporal logic, 65-80 [Zbl 1031.68075] \textit{Mateescu, Radu}, A generic on-the-fly solver for alternation-free Boolean equation systems, 81-96 [Zbl 1031.68583] \textit{Fontaine, Pascal; Gribomont, E. Pascal}, Decidability of invariant validation for paramaterized systems, 97-112 [Zbl 1031.68049] \textit{Chkliaev, Dmitri; Hooman, Jozef; de Vink, Erik}, Verification and improvement of the sliding window protocol, 113-127 [Zbl 1031.68503] \textit{Esparza, Javier; Maidl, Monika}, Simple representative instantiations for multicast protocols, 128-143 [Zbl 1031.68504] \textit{Emerson, E. Allen; Kahlon, Vineet}, Rapid parameterized model checking of snoopy cache coherence protocols, 144-159 [Zbl 1031.68548] \textit{Gurfinkel, Arie; Chechik, Marsha}, Proof-like counter-examples, 160-175 [Zbl 1031.68079] \textit{Glusman, Marcelo; Kamhi, Gila; Mador-Haim, Sela; Fraer, Ranan; Vardi, Moshe Y.}, Multiple-counterexample guided iterative abstraction refinement: An industrial evaluation, 176-191 [Zbl 1031.68549] \textit{Clarke, Edmund; Fehnker, Ansgar; Han, Zhi; Krogh, Bruce; Stursberg, Olaf; Theobald, Michael}, Verification of hybrid systems based on counterexample-guided abstraction refinement, 192-207 [Zbl 1031.68078] \textit{Alur, Rajeev; Dang, Thao; Ivančić, Franjo}, Counter-example guided predicate abstraction of hybrid systems, 208-223 [Zbl 1031.68074] \textit{Fersman, Elena; Mokrushin, Leonid; Pettersson, Paul; Yi, Wang}, Schedulability analysis using two clocks, 224-239 [Zbl 1031.68031] \textit{Abdeddaïm, Yasmina; Asarin, Eugene; Maler, Oded}, On optimal scheduling under uncertainty, 240-253 [Zbl 1031.68030] \textit{Behrmann, Gerd; Bouyer, Patricia; Fleury, Emmanuel; Larsen, Kim G.}, Static guard analysis in timed automata verification, 254-270 [Zbl 1031.68076] \textit{Dierks, Henning; Tapken, Josef}, Moby/DC -- A tool for model-checking parametric real-time specifications, 271-277 [Zbl 1031.68547] \textit{Dembiński, Piotr; Janowska, Agata; Janowski, Paweł; Penczek, Wojciech; Półrola, Agata; Szreter, Maciej; Wozna, Bozena; Zbrzezny, Andrzej}, \(\surd\)erics: A tool for verifying timed automata and Estelle specifications, 278-283 [Zbl 1031.68546] \textit{Cibrario B., Ivan; Durante, Luca; Sisto, Riccardo; Valenzano, Adriano}, A new knowledge representation strategy for cryptographic protocol analysis, 284-298 [Zbl 1031.94514] \textit{Bozga, Liana; Lakhnech, Yassine; Périn, Michael}, Pattern-based abstraction for verifying secrecy in protocols, 299-314 [Zbl 1031.94512] \textit{Basu, Samik; Ramakrishnan, C. R.}, Compositional analysis for verification of parameterized systems, 315-330 [Zbl 1031.68543] \textit{Cobleigh, Jamieson M.; Giannakopoulou, Dimitra; Păsăreanu, Corina S.}, Learning assumptions for compositional verification, 331-346 [Zbl 1031.68545] \textit{Tripakis, Stavros}, Automated module composition, 347-362 [Zbl 1031.68521] \textit{Alur, Rajeev; La Torre, Salvatore; Madhusudan, Parthasarathy}, Modular strategies for recursive game graphs, 363-378 [Zbl 1031.68048] \textit{Ciardo, Gianfranco; Marmorstein, Robert; Siminiceanu, Radu}, Saturation unbound, 379-393 [Zbl 1031.68544] \textit{Bartzis, Constantinos; Bultan, Tevfik}, Construction of efficient BDDs for bounded arithmetic constraints, 394-408 [Zbl 1031.68542] \textit{Sokolsky, Oleg; Philippou, Anna; Lee, Insup; Christou, Kyriakos}, Modeling and analysis of power-aware systems, 409-424 [Zbl 1031.68553] \textit{Hermanns, Holger; Joubert, Christophe}, A set of performance and dependability analysis components for CADP, 425-430 [Zbl 1031.68552] \textit{Zhang, Dezhuang; Cleaveland, Rance; Stark, Eugene W.}, The integrated CWB-NC/PIOATool for functional verification and performance analysis of concurrent systems, 431-436 [Zbl 1031.68554] \textit{Braghin, Chiara; Cortesi, Agostino; Filippone, Stefano; Focardi, Riccardo; Luccio, Flaminia L.; Piazza, Carla}, BANANA -- A tool for boundary ambients nesting analysis, 437-441 [Zbl 1031.68659] \textit{Berthomieu, Bernard; Vernadat, François}, State class constructions for branching analysis of time Petri nets, 442-457 [Zbl 1031.68082] \textit{Khomenko, Victor; Koutny, Maciej}, Branching processes of high-level Petri nets, 458-472 [Zbl 1031.68083] \textit{Schmidt, Karsten}, Using Petri net invariants in state space construction, 473-488 [Zbl 1031.68084] \textit{Stoller, Scott D.; Cohen, Ernie}, Optimistic synchronization-based state-space reduction, 489-504 [Zbl 1031.68085] \textit{Vaziri, Mandana; Jackson, Daniel}, Checking properties of heap-manipulating procedures with a constraint solver, 505-520 [Zbl 1031.68518] \textit{Berezin, Sergey; Ganesh, Vijay; Dill, David L.}, An online proof-producing decision procedure for mixed-integer linear arithmetic, 521-536 [Zbl 1031.68584] \textit{Conchon, Sylvain; Krstić, Sava}, Strategies for combining decision procedures, 537-552 [Zbl 1031.68585] \textit{Khurshid, Sarfraz; Păsăreanu, Corina S.; Visser, Willem}, Generalized symbolic execution for model checking and testing, 553-568 [Zbl 1031.68519] \textit{Baray, Fabrice; Codognet, Philippe; Diaz, Daniel; Michel, Henri}, Code-based test generation for validation of functional processor descriptions, 569-584 [Zbl 1031.68509] \textit{Groote, Jan Friso; van Ham, Frank}, Large state space visualization, 585-590 [Zbl 1031.68522] \textit{Bigot, Céline; Faivre, Alain; Gallois, Jean-Pierre; Lapitre, Arnault; Lugato, David; Pierron, Jean-Yves; Rapin, Nicolas}, Automatic test generation with AGATHA, 591-596 [Zbl 1031.68551] \textit{Uchitel, Sebastian; Chatley, Robert; Kramer, Jeff; Magee, Jeff}, LTSA-MSC: Tool support for behaviour model elaboration using implied scenarios, 597-601 [Zbl 1031.68550]
scientific article; zbMATH DE number 1955936