Invited Papers
Reasoning about Separation using Abstraction and Reification
An Interface Theory for the Internet of Things
Program Verification
Learning Assertions to Verify Linked-List Programs
Verifying Protocol Implementations by Augmenting Existing Cryptographic Libraries with Specifications
Specification and Verification of Atomic Operations in GPGPU Programs
History-based Verification of Functional Behaviour of Concurrent Programs
Investigating Instrumentation Techniques for ESB Runtime Verification
Towards Domain Refinement for UML/OCL Bounded Verification
Testing
Efficient Testing of Different Loop Paths
Model-Based Robustness Testing in Event-B using Mutation
On the Testability of Properties Patterns
Certification
Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning
Formal Analysis of Proactive, Distributed Routing
Certification of Distributed Algorithms Solving Problems with Optimal Substructure
Formal Specification and Proof
From Failure to Proof: The ProB Disprover for B and Event-B
Formalizing a Secure Foreign Function Interface
A Formal Study of Backward Compatible Dynamic Software Updates
Testing and Model Checking
Memory Management Test-Case Generation of C Programs using Bounded Model Checking
Techniques for Memory-Efficient Model Checking of C and C++ Code
NAT2TEST Tool: from Natural Language Requirements to Test Cases based on CSP
Planning
Task Planning of Cyber-Human Systems
Generating None-Plans in Order to Find Plans
Modelling and Model Transformation Twitlang(er): interactions modeling language (and interpreter) for Twitter
From Featured Transition Systems to Modal Transition Systems with Variability Constraints
An extensible operational semantics for UML activity diagrams.