Abstract is missing.
- Reasoning about Separation Using Abstraction and ReificationCliff B. Jones, Nisansala Yatapanage. 3-19 [doi]
- An Interface Theory for the Internet of ThingsMarten Lohstroh, Edward A. Lee. 20-34 [doi]
- Learning Assertions to Verify Linked-List ProgramsJan Tobias Mühlberg, David H. White 0001, Mike Dodds, Gerald Lüttgen, Frank Piessens. 37-52 [doi]
- Verifying Protocol Implementations by Augmenting Existing Cryptographic Libraries with SpecificationsGijs Vanspauwen, Bart Jacobs 0002. 53-68 [doi]
- Specification and Verification of Atomic Operations in GPGPU ProgramsAfshin Amighi, Saeed Darabi, Stefan Blom, Marieke Huisman. 69-83 [doi]
- History-Based Verification of Functional Behaviour of Concurrent ProgramsStefan Blom, Marieke Huisman, Marina Zaharieva-Stojanovski. 84-98 [doi]
- Investigating Instrumentation Techniques for ESB Runtime VerificationChristian Colombo, Gabriel Dimech, Adrian Francalanza. 99-107 [doi]
- Towards Domain Refinement for UML/OCL Bounded VerificationRobert Clarisó, Carlos A. González, Jordi Cabot. 108-114 [doi]
- Efficient Testing of Different Loop PathsStefan Huster, Sebastian Burg, Hanno Eichelberger, Jo Laufenberg, Jürgen Ruf, Thomas Kropf, Wolfgang Rosenstiel. 117-131 [doi]
- Model-Based Robustness Testing in Event-B Using MutationAymerick Savary, Marc Frappier, Michael Leuschel, Jean-Louis Lanet. 132-147 [doi]
- On the Testability of Properties PatternsSimone Hanazumi, Ana Cristina Vieira de Melo. 148-155 [doi]
- Speed Up Configurable Certificate Validation by Certificate Reduction and PartitioningMarie-Christine Jakobs. 159-174 [doi]
- Formal Analysis of Proactive, Distributed RoutingMojgan Kamali, Peter Höfner, Maryam Kamali, Luigia Petre. 175-189 [doi]
- Certification of Distributed Algorithms Solving Problems with Optimal SubstructureKim Völlinger, Wolfgang Reisig. 190-195 [doi]
- From Failure to Proof: The ProB Disprover for B and Event-BSebastian Krings, Jens Bendisposto, Michael Leuschel. 199-214 [doi]
- Formalizing a Secure Foreign Function InterfaceAdriaan Larmuseau, Dave Clarke. 215-230 [doi]
- A Formal Study of Backward Compatible Dynamic Software UpdatesJun Shen, Rida A. Bazzi. 231-248 [doi]
- Memory Management Test-Case Generation of C Programs Using Bounded Model CheckingHerbert Rocha, Raimundo S. Barreto, Lucas C. Cordeiro. 251-267 [doi]
- Techniques for Memory-Efficient Model Checking of C and C++ CodePetr Rockai, Vladimír Still, Jiri Barnat. 268-282 [doi]
- NAT2TEST Tool: From Natural Language Requirements to Test Cases Based on CSPGustavo Carvalho, Flávia A. Barros, Ana Carvalho, Ana Cavalcanti, Alexandre Mota, Augusto Sampaio. 283-290 [doi]
- Task Planning of Cyber-Human SystemsRoykrong Sukkerd, David Garlan, Reid Simmons. 293-309 [doi]
- Generating None-Plans in Order to Find PlansMichal Knapik, Artur Niewiadomski, Wojciech Penczek. 310-324 [doi]
- Twitlang(er): Interactions Modeling Language (and Interpreter) for TwitterRocco De Nicola, Alessandro Maggi, Marinella Petrocchi, Angelo Spognardi, Francesco Tiezzi. 327-343 [doi]
- From Featured Transition Systems to Modal Transition Systems with Variability ConstraintsMaurice H. ter Beek, Ferruccio Damiani, Stefania Gnesi, Franco Mazzanti, Luca Paolini. 344-359 [doi]
- An Extensible Operational Semantics for UML Activity DiagramsZamira Daw, Rance Cleaveland. 360-368 [doi]