Tools and algorithms for the construction and analysis of systems. 8th international conference, TACAS 2002. Held as part of the joint European conferences on theory and practice of software, ETAPS 2002, Grenoble, France, April 8--12, 2002 (Q1601176)

The articles of mathematical interest will be reviewed individually. The preceding conference (7th, 2001) has been reviewed (see Zbl 0960.00058). Indexed articles: \textit{Lowry, Michael R.}, Software construction and analysis tools for future space missions, 1-19 [Zbl 1043.68516] \textit{Jackson, Daniel}, Alloy: A new technology for software modelling, 20 [Zbl 1043.68520] \textit{Braberman, Víctor; Garbervetsky, Diego; Olivero, Alfredo}, Improving the verification of timed systems using influence information, 21-36 [Zbl 1043.68588] \textit{Ouaknine, Joël}, Digitisation and full abstraction for dense-time model checking, 37-51 [Zbl 1043.68581] \textit{Kwiatkowska, Marta; Norman, Gethin; Parker, David}, Probabilistic symbolic model checking with PRISM: A hybrid approach, 52-66 [Zbl 1043.68576] \textit{Fersman, Elena; Pettersson, Paul; Yi, Wang}, Timed automata with asynchronous processes: Schedulability and decidability, 67-82 [Zbl 1043.68589] \textit{Cha, Hojung; Ha, Rhan}, Validating timing constraints of dependent jobs with variable execution times in distributed real-time systems, 83-97 [Zbl 1043.68511] \textit{Subramani, K.}, An analysis of zero-clairvoyant scheduling, 98-112 [Zbl 1043.68512] \textit{Abdeddaïm, Yasmina; Maler, Oded}, Preemptive job-shop scheduling using stopwatch automata, 113-126 [Zbl 1043.68510] \textit{Wedde, Horst F.; Wedig, Arnim}, Explicit modeling of influences, and of their absence, in distributed systems, 127-141 [Zbl 1043.68508] \textit{Backhouse, Kevin}, A functional semantics of attribute grammars, 142-157 [Zbl 1043.68562] \textit{Ball, Thomas; Podelski, Andreas; Rajamani, Sriram K.}, Relative completeness of abstraction refinement for software model checking, 158-172 [Zbl 1043.68523] \textit{Delzanno, Giorgio; Raskin, Jean-François; Van Begin, Laurent}, Towards the automated verification of multithreaded Java programs, 173-187 [Zbl 1043.68530] \textit{Bouquet, Fabrice; Legeard, Bruno; Peureux, Fabien}, CLPS-B -- a constraint solver for B, 188-204 [Zbl 1043.68527] \textit{Kim, Taeho; Stringer-Calvert, David; Cha, Sungdeok}, Formal verification of functional properties of an SCR-style software requirements specification using PVS, 205-220 [Zbl 1043.68538] \textit{Bozzano, Marco; Delzanno, Giorgio}, Beyond parameterized verification, 221-235 [Zbl 1043.68565] \textit{Basu, Samik; Kumar, K. Narayan; Pokorny, L. Robert; Ramakrishnan, C. R.}, Resource-constrained model checking of recursive programs, 236-250 [Zbl 1043.68524] \textit{Emerson, E. Allen; Kahlon, Vineet}, Model checking large-scale and parameterized resource allocation systems, 251-265 [Zbl 1043.68569] \textit{Godefroid, Patrice; Khurshid, Sarfraz}, Exploring very large state spaces using genetic algorithms, 266-280 [Zbl 1043.68591] \textit{Mateescu, Radu}, Local model-checking of modal mu-calculus on acyclic labeled transition systems, 281-295 [Zbl 1043.68596] \textit{Armoni, Roy; Fix, Limor; Flaisher, Alon; Gerth, Rob; Ginsburg, Boris; Kanza, Tomer; Landver, Avner; Mador-Haim, Sela; Singerman, Eli; Tiemeyer, Andreas; Vardi, Moshe Y.; Zbar, Yael}, The ForSpec temporal logic: A new temporal property-specification language, 296-311 [Zbl 1043.68563] \textit{Jin, HoonSang; Kuehlmann, Andreas; Somenzi, Fabio}, Fine-grain conjunction scheduling for symbolic reachability analysis, 312-326 [Zbl 1043.68574] \textit{Hong, Hyoung Seok; Lee, Insup; Sokolsky, Oleg; Ural, Hasan}, A temporal logic based theory of test coverage and generation, 327-341 [Zbl 1043.68573] \textit{Havelund, Klaus; Rosu, Grigore}, Synthesizing monitors for safety properties, 342-356 [Zbl 1043.68534] \textit{Groce, Alex; Peled, Doron; Yannakakis, Mihalis}, Adaptive model checking, 357-370 [Zbl 1043.68570] \textit{Heljanko, Keijo; Khomenko, Victor; Koutny, Maciej}, Parallelisation of the Petri net unfolding algorithm, 371-385 [Zbl 1043.68593] \textit{Bornot, Sebastien; Morin, Remi; Niebert, Peter; Zennou, Sarah}, Black box unfolding with local first search, 386-400 [Zbl 1043.68587] \textit{Bustan, Doron; Grumberg, Orna}, Applicability of fair simulation, 401-414 [Zbl 1043.68567] \textit{Gentilini, Raffaella; Piazza, Carla; Policriti, Alberto}, Simulation as coarsest partition problem, 415-430 [Zbl 1043.68590] \textit{Gunter, Elsa; Peled, Doron}, Temporal debugging for concurrent systems, 431-444 [Zbl 1043.68592] \textit{Jin, HoonSang; Ravi, Kavita; Somenzi, Fabio}, Fate and free will in error traces, 445-459 [Zbl 1043.68575] \textit{Amnell, Tobias; Fersman, Elena; Mokrushin, Leonid; Pettersson, Paul; Yi, Wang}, TIMES -- a tool for modelling and implementation of embedded systems, 460-464 [Zbl 1043.68513] \textit{Lang, Frédéric}, Compositional verification using SVL scripts, 465-469 [Zbl 1043.68547] \textit{Clarke, Duncan; Jéron, Thierry; Rusu, Vlad; Zinovieva, Elena}, STG: A symbolic test generation tool, 470-475 [Zbl 1043.68546] \textit{Stehno, Christian}, Real-time systems design with PEP, 476-480 [Zbl 1043.68548]