SEFM 2016

A Cognitive Framework based on Rewriting Logic for the Analysis of Interactive Systems

(Antonio Cerone)

Automatic Derivation of Platform Noninterference Properties

(Oliver Schwarz and Mads Dam)

BMotionWeb: A Tool for Rapid Creation of Formal Prototypes (Tool Paper)

(Lukas Ladenberger and Michael Leuschel)

CoCoSpec: A mode aware contract language

(Adrien Champion, Arie Gurfinkel, Temesghen Kahsai and Cesare Tinelli)

Combining Abstract Interpretation with Symbolic Execution for a Static Value Range Analysis of Block Diagrams

(Christian Dernehl, Norman Hansen and Stefan Kowalewski)

Combining Predicate Abstraction with Fixpoint Approximations

(Tuba Yavuz)

Correlating Structured Inputs and Outputs in Functional Specifications

(Oana Fabiana Andreescu, Thomas Jensen and Stéphane Lescuyer)

Counterexamples from Proof Failures in SPARK

(David Hauzar, Claude Marché and Yannick Moy)

Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis

(Jaroslav Bendík, Nikola Benes, Jiri Barnat and Ivana Cerna)

Incentive Stackelberg Mean-payoff Games

(Anshul Gupta, Sven Schewe, Ashutosh Trivedi, Maram Sai Krishna Deepak and Bharath Kumar Padarthi)

Linearizability and Causality

(Simon Doherty and John Derrick)

LTL Parameter Synthesis of Parametric Timed Automata

(Peter Bezděk, Nikola Beneš, Jiří Barnat and Ivana Černá)

Model checking simulation rules for linearizability

(Graeme Smith)

Modularizing Crosscutting Concerns in Component-Based Systems

(Antoine El-Hokayem, Ylies Falcone and Mohamad Jaber)

Program Generation using Simulated Annealing and Model Checking

(Idress Husien and Sven Schewe)

Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution

(Jera Hensel, Jürgen Giesl, Florian Frohn and Thomas Ströder)

Refinement-based verification of Communicating Unstructured Code

(Nils Jähnig, Thomas Göthel and Sabine Glesner)

SMT-based automatic proof of ASM model refinement

(Paolo Arcaini, Angelo Gargantini and Elvinia Riccobene)

Stability-based Adaptation of Asynchronously Communicating Software

(Carlos Canal and Gwen Salaün)

Tightening a Contract Refinement

(Alessandro Cimatti, Ramiro Demasi and Stefano Tonetta)

Compliance Checking in the Open Payments Ecosystem

(Shaun Azzopardi, Christian Colombo, Gordon Pace and Brian Vella)

Coq Implementation of OO Verification Framework VeriJ

(Ke Zhang and Zongyan Qiu)

Guided Dynamic Symbolic Execution Using Subgraph Control-Flow Information

(Josselin Feist, Mounier Laurent and Marie-Laure Potet)

LTL Model Checking under Fairness in ProB

(Ivaylo Dobrikov, Daniel Plagge and Michael Leuschel)

Towards a Proof Framework for Information Systems with Weak Consistency

(Peter Zeller and Arnd Poetzsch-Heffter)