Abstract is missing.
- Contribution to a Rigorous Analysis of Web Application FrameworksEgon Börger, Antonio Cisternino, Vincenzo Gervasi. 1-20 [doi]
- Process Algebra for Event-Driven Runtime Verification: A Case Study of Wireless Network ManagementMuffy Calder, Michele Sevegnani. 21-23 [doi]
- Translating TLA + to B for Validation with ProBDominik Hansen, Michael Leuschel. 24-38 [doi]
- Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time BandsBrijesh Dongol, Ian J. Hayes. 39-53 [doi]
- Safety and Line Capacity in Railways - An Approach in Timed CSPYoshinao Isobe, Faron Moller, Hoang Nga Nguyen, Markus Roggenbach. 54-68 [doi]
- Refinement-Based Development of Timed SystemsJesper Berthing, Pontus Boström, Kaisa Sere, Leonidas Tsiopoulos, Jüri Vain. 69-83 [doi]
- Analysing and Closing Simulation Coverage by Automatic Generation and Verification of Formal Properties from Coverage ReportsTim Blackmore, David Halliwell, Philip Barker, Kerstin Eder, Naresh Ramaram. 84-98 [doi]
- Model Checking as Static Analysis: RevisitedFuyuan Zhang, Flemming Nielson, Hanne Riis Nielson. 99-112 [doi]
- Formal Verification of Compiler Transformations on Polychronous EquationsVan Chan Ngo, Jean-Pierre Talpin, Thierry Gautier, Paul Le Guernic, Loïc Besnard. 113-127 [doi]
- Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-ExamplesHerbert Rocha, Raimundo S. Barreto, Lucas Cordeiro, Arilo Dias Neto. 128-142 [doi]
- MULE-Based Wireless Sensor Networks: Probabilistic Modeling and Quantitative AnalysisFatemeh Kazemeyni, Einar Broch Johnsen, Olaf Owe, Ilangko Balasingham. 143-157 [doi]
- Mechanized Extraction of Topology Anti-patterns in Wireless NetworksMatthias Woehrle, Rena Bakhshi, Mohammad Reza Mousavi. 158-173 [doi]
- A Proof Framework for Concurrent ProgramsLeonard Lensink, Sjaak Smetsers, Marko C. J. D. van Eekelen. 174-190 [doi]
- A UTP Semantics of pGCL as a Homogeneous RelationRiccardo Bresciani, Andrew Butterfield. 191-205 [doi]
- Behaviour-Based Cheat Detection in Multiplayer Games with Event-BHaiYun Tian, Phillip J. Brooke, Anne-Gwenn Bosser. 206-220 [doi]
- Refinement-Preserving Translation from Event-B to Register-Voice Interactive SystemsDenisa Diaconescu, Ioana Leustean, Luigia Petre, Kaisa Sere, Gheorghe Stefanescu. 221-236 [doi]
- Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-BAnton Tarasyuk, Elena Troubitsyna, Linas Laibinis. 237-252 [doi]
- Partially-Supervised Plants: Embedding Control Requirements in Plant ComponentsJasen Markovski, Dirk A. van Beek, Jos C. M. Baeten. 253-267 [doi]
- Early Fault Detection in Industry Using Models at Various Abstraction LevelsJozef Hooman, Arjan J. Mooij, Hans van Wezep. 268-282 [doi]
- PE-KeY: A Partial Evaluator for Java ProgramsRan Ji, Richard Bubel. 283-295 [doi]
- Specification-Driven Unit Test Generation for Java Generic ClassesFrancisco Rebello de Andrade, João Pascoal Faria, Antónia Lopes, Ana C. R. Paiva. 296-311 [doi]
- Specifying UML Protocol State Machines in AlloyAna Gabriela Garis, Ana C. R. Paiva, Alcino Cunha, Daniel Riesco. 312-326 [doi]
- Patterns for a Log-Based Strengthening of Declarative Compliance ModelsDennis M. M. Schunselaar, Fabrizio Maria Maggi, Natalia Sidorova. 327-342 [doi]
- A Formal Interactive Verification Environment for the Plan Execution Interchange LanguageCamilo Rocha, Héctor Cadavid, César A. Muñoz, Radu Siminiceanu. 343-357 [doi]