FM 2005: Formal methods. International symposium of formal methods Europe, Newcastle, UK, July 18--22, 2005. Proceedings. (Q2577426)

The articles of this volume will be reviewed individually. Indexed articles: \textit{Joseph, Mathai}, Formal aids for the growth of software systems, 1 [Zbl 1120.68370] \textit{Gaudel, Marie-Claude}, Formal methods and testing: Hypotheses, and correctness approximations, 2-8 [Zbl 1120.68416] \textit{Johnson, C. W.}, The natural history of bugs: Using formal methods to analyse software related failures in space missions, 9-25 [Zbl 1120.68389] \textit{Leino, K. Rustan M.; Müller, Peter}, Modular verification of static class invariants, 26-42 [Zbl 1120.68377] \textit{Kassios, Ioannis T.}, Decoupling in object orientation, 43-58 [Zbl 1120.68376] \textit{Pierik, Cees; Clarke, Dave; de Boer, Frank S.}, Controlling object allocation using creation guards, 59-74 [Zbl 1120.68379] \textit{Bouquet, Fabrice; Dadeau, Frédéric; Legeard, Bruno; Utting, Mark}, Symbolic animation of JML specifications, 75-90 [Zbl 1120.68375] \textit{Cachera, David; Jensen, Thomas; Pichardie, David; Schneider, Gerardo}, Certified memory usage analysis, 91-106 [Zbl 1120.68385] \textit{Celiku, Orieta; McIver, Annabelle}, Compositional specification and analysis of cost-based properties in probabilistic programs, 107-122 [Zbl 1120.68386] \textit{Salverda, Pierre; Roşu, Grigore; Zilles, Craig}, Formally defining and verifying master/slave speculative parallelization, 123-138 [Zbl 1120.68302] \textit{De Wulf, Martin; Doyen, Laurent; Raskin, Jean-François}, Systematic implementation of real-time models, 139-156 [Zbl 1120.68413] \textit{Wassyng, Alan; Lawford, Mark; Hu, Xiayong}, Timing tolerances in safety-critical software, 157-172 [Zbl 1120.68396] \textit{Bohnenkamp, Henrik; Belinfante, Axel}, Timed testing with TorX, 173-188 [Zbl 1120.68409] \textit{Rusu, Vlad; Marchand, Hervé; Jéron, Thierry}, Automatic verification and conformance testing for validating safety properties of reactive systems, 189-204 [Zbl 1120.68420] \textit{Bolton, Christie}, Adding conflict and confusion to CSP, 205-220 [Zbl 1120.68410] \textit{Butler, Michael; Leuschel, Michael}, Combining CSP and B for specification and property verification, 221-236 [Zbl 1120.68411] \textit{Woodcock, Jim; Cavalcanti, Ana; Freitas, Leonardo}, Operational semantics for model checking Circus, 237-252 [Zbl 1120.68423] \textit{Cavalcanti, Ana; Clayton, Phil; O'Halloran, Colin}, Control law diagrams in Circus, 253-268 [Zbl 1120.68412] \textit{Basin, David; Kuruma, Hironobu; Takaragi, Kazuo; Wolff, Burkhart}, Verification of a signature architecture with HOL-Z, 269-285 [Zbl 1120.68407] \textit{Buchholtz, Mikael; Gilmore, Stephen; Haenel, Valentin; Montangero, Carlo}, End-to-end integrated security and performance analysis on the DEGAS Choreographer platform, 286-301 [Zbl 1120.68388] \textit{Andronick, June; Chetali, Boutheina; Paulin-Mohring, Christine}, Formal verification of security properties of smart card embedded source code, 302-317 [Zbl 1120.68384] \textit{Zave, Pamela}, A formal model of addressing for interoperating networks, 318-333 [Zbl 1120.68335] \textit{Lei, Yu; Iyer, S. Purushothaman}, An approach to unfolding asynchronous communication protocols, 334-349 [Zbl 1120.68339] \textit{Qiu, Zongyan; Wang, Shuling; Pu, Geguang; Zhao, Xiangpeng}, Semantics of BPEL4WS-like fault and compensation handling, 350-365 [Zbl 1120.68324] \textit{Bošnački, Dragan}, On some Galois connection based abstractions for the mu-calculus, 366-381 [Zbl 1120.68408] \textit{Banach, Richard; Poppleton, Michael; Jeske, Czeslaw; Stepney, Susan}, Retrenching the purse: Finite sequence numbers, and the tower pattern, 382-398 [Zbl 1120.68406] \textit{Alves, T. L.; Silva, P. F.; Visser, J.; Oliveira, J. N.}, Strategic term rewriting and its application to a VDM-SL to SQL conversion, 399-414 [Zbl 1120.68399] \textit{Sun, Jun; Dong, Jin Song}, Synthesis of distributed processes from scenario-based specifications, 415-431 [Zbl 1120.68422] \textit{Katz, Emilia; Katz, Shmuel}, Verifying scenario-based aspect specifications, 432-447 [Zbl 1120.68419] \textit{Kim, Soon-Kyeong; Burger, Damian; Carrington, David}, An MDA approach towards integrating formal and informal modeling languages, 448-464 [Zbl 1120.68390] \textit{Hoenicke, Jochen; Maier, Patrick}, Model-checking of specifications integrating processes, data and time, 465-480 [Zbl 1120.68417] \textit{Donaldson, A. F.; Miller, A.}, Automatic symmetry detection for model checking using computational group theory, 481-496 [Zbl 1120.68414] \textit{Iyer, Subramanian; Sahoo, Debashis; Emerson, E. Allen; Jain, Jawahar}, On partitioning and symbolic model checking, 497-511 [Zbl 1120.68418] \textit{Sharygina, Natasha; Chaki, Sagar; Clarke, Edmund; Sinha, Nishant}, Dynamic component substitutability analysis, 512-528 [Zbl 1120.68421] \textit{Harrison, John}, Floating-point verification, 529-532 [Zbl 1120.68355] \textit{Eisler, Stefan; Scheidler, Christian; Josko, Bernhard; Sandmann, Guido; Stroop, Joachim}, Preliminary results of a case study: Model checking for advanced automotive applications, 533-536 [Zbl 1120.68415] \textit{Pretschner, Alexander}, Model-based testing in practice, 537-541 [Zbl 1120.68393] \textit{Campbell, Colin; Grieskamp, Wolfgang; Nachmanson, Lev; Schulte, Wolfram; Tillmann, Nikolai; Veanes, Margus}, Testing concurrent object-oriented systems with Spec Explorer, 542-547 [Zbl 1120.68354] \textit{Broadfoot, Guy H.}, ASD case notes: Costs and benefits of applying formal methods to industrial control software, 548-551 [Zbl 1120.68387] \textit{Muller, Gerrit}, The informal nature of systems engineering, 552-556 [Zbl 1120.68369]