Abstract is missing.
- From Z to B and then Event-B: Assigning Proofs to Meaningful ProgramsJean-Raymond Abrial. 1-15 [doi]
- Systems Design Guided by Progress ConcernsSimon Hudon, Thai Son Hoang. 16-30 [doi]
- Assume-Guarantee Specifications of State Transition Diagrams for Behavioral RefinementChristian Prehofer. 31-45 [doi]
- Translating VDM to AlloyKenneth Lausdahl. 46-60 [doi]
- 3 Specifications Using CADPDimitris Vekris, Frédéric Lang, Catalin Dima, Radu Mateescu. 61-76 [doi]
- Knowledge for the Distributed Implementation of Constrained SystemsSusanne Graf, Sophie Quinton. 77-93 [doi]
- Automated Anonymity Verification of the ThreeBallot Voting SystemMurat Moran, James Heather, Steve Schneider. 94-108 [doi]
- Compositional Verification of Software Product LinesJean-Vivien Millo, S. Ramesh, Shankara Narayanan Krishna, Ganesh Khandu Narwane. 109-123 [doi]
- Deductive Verification of State-Space AlgorithmsFrédéric Gava, Jean Fortin, Michaël Guedj. 124-138 [doi]
- Inductive Verification of Hybrid Automata with Strongest Postcondition CalculusDaisuke Ishii, Guillaume Melquiond, Shin Nakajima. 139-153 [doi]
- Priced Timed Automata and Statistical Model CheckingKim Guldstrand Larsen. 154-161 [doi]
- Improved Reachability Analysis in DTMC via Divide and ConquerSongzheng Song, Lin Gui 0002, Jun Sun 0001, Yang Liu, Jin Song Dong. 162-176 [doi]
- Solving Games Using Incremental InductionAndreas Morgenstern, Manuel Gesell, Klaus Schneider. 177-191 [doi]
- Model-Checking Software Library API Usage RulesFu Song, Tayssir Touili. 192-207 [doi]
- Formal Modelling and Verification of Population ProtocolsDominique Méry, Michael Poppleton. 208-222 [doi]
- Detecting Vulnerabilities in Java-Card Bytecode Verifiers Using Model-Based TestingAymerick Savary, Marc Frappier, Jean-Louis Lanet. 223-237 [doi]
- Integrating Formal Predictions of Interactive System Behaviour with User EvaluationRimvydas Ruksenas, Paul Curzon, Michael D. Harrison. 238-252 [doi]
- Automatic Inference of Erlang Module BehaviourRamsay Taylor, Kirill Bogdanov, John Derrick. 253-267 [doi]
- Integrating Proved State-Based Models for Constructing Correct Distributed AlgorithmsManamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh. 268-284 [doi]
- Quantified Abstractions of Distributed SystemsElvira Albert, Jesús Correas, Germán Puebla, Guillermo Román-Díez. 285-300 [doi]
- An Algebraic Theory for Web Service ContractsCosimo Laneve, Luca Padovani. 301-315 [doi]
- A Compositional Automata-Based Semantics for Property PatternsKalou Cabrera Castillos, Frédéric Dadeau, Jacques Julliand, Bilal Kanso, Safouan Taha. 316-330 [doi]
- A Formal Semantics for Complete UML State Machines with CommunicationsShuang Liu, Yang Liu, Étienne André, Christine Choppy, Jun Sun 0001, Bimlesh Wadhwa, Jin Song Dong. 331-346 [doi]
- From Small-Step Semantics to Big-Step Semantics, AutomaticallyStefan Ciobaca. 347-361 [doi]
- Program Equivalence by Circular ReasoningDorel Lucanu, Vlad Rusu. 362-377 [doi]
- Structural Transformations for Data-Enriched Real-Time SystemsErnst-Rüdiger Olderog, Mani Swaminathan. 378-393 [doi]
- Deadlock Analysis of Concurrent Objects: Theory and PracticeElena Giachino, Carlo A. Grazia, Cosimo Laneve, Michael Lienhardt, Peter Y. H. Wong. 394-411 [doi]
- Broadcast, Denial-of-Service, and Secure CommunicationRoberto Vigo, Flemming Nielson, Hanne Riis Nielson. 412-427 [doi]
- Characterizing Fault-Tolerant Systems by Means of Simulation RelationsRamiro Demasi, Pablo F. Castro, T. S. E. Maibaum, Nazareno Aguirre. 428-442 [doi]