Abstract is missing.
- Shape and Content - A Database-Theoretic Perspective on the Analysis of Data StructuresDiego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger. 3-17 [doi]
- How to Break the Bank: Semantics of Capability PoliciesSophia Drossopoulou, James Noble. 18-35 [doi]
- Model-Checking Circus State-Rich SpecificationsMarcel Vinicius Medeiros Oliveira, Augusto C. A. Sampaio, Madiel S. Conserva Filho. 39-54 [doi]
- An Interactive Verification Tool Meets an IDEMartin Hentschel, Stefan Käsdorf, Reiner Hähnle, Richard Bubel. 55-70 [doi]
- An Analysis Pathway for the Quantitative Evaluation of Public Transport SystemsStephen Gilmore, Mirco Tribastone, Andrea Vandin. 71-86 [doi]
- Modeling UML Template Classes with FoCaLiZeMessaoud Abbas, Choukri-Bey Ben-Yelles, Renaud Rioboo. 87-102 [doi]
- Integrating Event-B Modelling and Discrete-Event Simulation to Analyse Resilience of Data Stores in the CloudLinas Laibinis, Benjamin Byholm, Inna Pereverzeva, Elena Troubitsyna, Kuan Eeik Tan, Ivan Porres. 103-119 [doi]
- Applying an Integrated Modelling Process to Run-time Management of Many-Core SystemsAsieh Salehi Fathabadi, Colin F. Snook, Michael Butler. 120-135 [doi]
- Verifying Behavioral UML Systems via CEGARYael Meller, Orna Grumberg, Karen Yorav. 139-154 [doi]
- Formal Refinement in SysMLAlvaro Miyazawa, Ana Cavalcanti. 155-170 [doi]
- Verifying Modal Workflow Specifications Using Constraint SolvingHadrien Bride, Olga Kouchnarenko, Fabien Peureux. 171-186 [doi]
- Proofs and Refutations in Invariant-Based ProgrammingJohannes Eriksson, Masoumeh Parsa, Ralph-Johan Back. 189-204 [doi]
- Automated Theorem Prover Assisted Program CalculationsDipak L. Chaudhari, Om P. Damani. 205-220 [doi]
- Managing LTL Properties in Event-B RefinementSteve A. Schneider, Helen Treharne, Heike Wehrheim, David M. Williams. 221-237 [doi]
- Formal Security Analysis of the MaCAN ProtocolAlessandro Bruni, Michal Sojka, Flemming Nielson, Hanne Riis Nielson. 241-255 [doi]
- A Probabilistic Framework for Security Scenarios with Dependent ActionsBarbara Kordy, Marc Pouly, Patrick Schweitzer. 256-271 [doi]
- A Hybrid Analysis for Security Protocols with StateJohn D. Ramsdell, Daniel J. Dougherty, Joshua D. Guttman, Paul D. Rowe. 272-287 [doi]
- Towards a Formal Semantics-Based Technique for Interprocedural SlicingIrina Mariuca Asavoae, Mihail Asavoae, Adrián Riesco. 291-306 [doi]
- Integrating Software and Hardware VerificationMarie-Christine Jakobs, Marco Platzner, Heike Wehrheim, Tobias Wiersema. 307-322 [doi]
- Code Generation for Event-BAndreas Fürst, Thai Son Hoang, David A. Basin, Krishnaji Desai, Naoto Sato, Kunihiko Miyazaki. 323-338 [doi]
- Verifying Linearizability on TSO ArchitecturesJohn Derrick, Graeme Smith, Brijesh Dongol. 341-356 [doi]
- A Compositional Proof Method for Linearizability Applied to a Wait-Free MultisetBogdan Tofan, Gerhard Schellhorn, Wolfgang Reif. 357-372 [doi]
- A Separation Principle for Embedded System InterfacingLucian M. Patcas, Mark Lawford, Tom Maibaum. 373-388 [doi]