Model checking software. 11th international SPIN workshop, Barcelona, Spain, April 1--3, 2004. Proceedings. (Q1881812)

The articles of this volume will be reviewed individually. The preceding workshop has been reviewed (see Zbl 1019.00013). Indexed articles: \textit{Wilhelm, Reinhard}, Formal analysis of processor timing models, 1-4 [Zbl 1125.68376] \textit{Pelánek, Radek}, Typical structural properties of state spaces, 5-22 [Zbl 1125.68372] \textit{Geldenhuys, Jaco}, State caching reconsidered, 23-38 [Zbl 1125.68365] \textit{Leven, Peter; Mehler, Tilman; Edelkamp, Stefan}, Directed error detection in C++ with the assembly-level model checker StEAM, 39-56 [Zbl 1125.68339] \textit{Dillinger, Peter C.; Manolios, Panagiotis}, Fast and accurate bitstate verification for SPIN, 57-75 [Zbl 1125.68368] \textit{Holzmann, Gerard J.; Joshi, Rajeev}, Model-driven software verification, 76-91 [Zbl 1125.68366] \textit{Gastin, Paul; Moro, Pierre; Zeitoun, Marc}, Minimization of counterexamples in SPIN, 92-108 [Zbl 1125.68369] \textit{Krichen, Moez; Tripakis, Stavros}, Black-box conformance testing for real-time systems, 109-126 [Zbl 1125.68370] \textit{Ober, Iulian; Graf, Susanne; Ober, Ileana}, Validation of UML models via a mapping to communicating extended timed automata, 127-145 [Zbl 1125.68371] \textit{Jones, Michael; Mercer, Eric}, Explicit state model checking with Hopper, 146-150 [Zbl 1125.68387] \textit{Garavel, Hubert; Mateescu, Radu}, SEQ.OPEN: A tool for efficient trace-based verification, 151-157 [Zbl 1125.68386] \textit{Batt, Grégory; Bergamini, Damien; de Jong, Hidde; Garavel, Hubert; Mateescu, Radu}, Model checking genetic regulatory networks using GNA and CADP, 158-163 [Zbl 1125.68384] \textit{Păsăreanu, Corina S.; Visser, Willem}, Verification of Java programs using symbolic execution and invariant generation, 164-181 [Zbl 1125.68367] \textit{Finkel, Alain; Leroux, Jérôme}, Polynomial time image computation with interval-definable counters systems, 182-197 [Zbl 1125.68364] \textit{Bošnački, Dragan; Ioustinova, Natalia; Sidorova, Natalia}, Using fairness to make abstractions work, 198-215 [Zbl 1125.68361] \textit{Leue, Stefan; Mayr, Richard; Wei, Wei}, A scalable incomplete test for message buffer overflow in Promela models, 216-233 [Zbl 1125.68343] \textit{Chen, J.; Cui, H.}, Translation from adapted UML to Promela for CORBA-based applications, 234-251 [Zbl 1125.68340] \textit{Flanagan, Cormac}, Verifying commit-atomicity using model-checking, 252-266 [Zbl 1125.68341] \textit{Rangarajan, Murali; Dajani-Brown, Samar; Schloegel, Kirk; Cofer, Darren}, Analysis of distributed spin applied to industrial-scale models, 267-285 [Zbl 1125.68373] \textit{Siegel, Stephen F.; Avrunin, George S.}, Verification of MPI-based software for scientific computation, 286-303 [Zbl 1125.68375] \textit{Ruys, Theo C.; Holzmann, Gerard J.}, Advanced SPIN tutorial, 304-305 [Zbl 1125.68374] \textit{Bozga, Marius; Graf, Susanne; Mounier, Laurent; Ober, Iulian}, IF validation environment tutorial, 306-307 [Zbl 1125.68362]