Accepted Papers
TrustFound: Towards a Formal Foundation for Model Checking Trusted Computing Platforms
Authors: Guangdong Bai, Jianan Hao, Jianliang Wu, Yang Liu, Zhenkai Liang and Andrew Martin
Definition, Semantics, and Analysis of Multirate Synchronous AADL
Authors: Kyungmin Bae, Peter Olveczky and Jose Meseguer
Efficient Runtime Monitoring with Metric Temporal Logic: A Case Study in the Android Operating System
Authors: Hendra Gunadi and Alwen Tiu
Computing Quadratic Invariants with Min- and Max-Policy Iterations: a Practical Comparison
Authors: Pierre Roux and Pierre-Loic Garoche
Management of Time Requirements in Component-based Systems
Authors: Yi Li, Tian Huat Tan and Marsha Chechik
Automated Real Proving in PVS via MetiTarski (Tool Paper)
Authors: William Denman and Cesar Munoz
Knowledge-based Automated Repair of Authentication Protocols
Authors: Borzoo Bonakdarpour, Reza Hajisheykhi and Sandeep Kulkarni
Towards a Formal Analysis of Information Leakage for Signature Attacks in Preferential Elections
Authors: Roland Wen, Annabelle McIver and Carroll Morgan
Compositional Synthesis of Concurrent Systems through Causal Model Checking and Learning
Authors: Shang-Wei Lin and Pao-Ann Hsiung
Quiescent Consistency: Defining and Verifying Relaxed Linearizability
Authors: John Derrick, Heike Wehrheim, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan and Oleg Travkin
Contracts in Practice
Authors: H.-Christian Estler, Carlo A. Furia, Martin Nordio, Marco Piccioniand Bertrand Meyer
Flexible Invariants Through Semantic Collaboration
Authors: Nadia Polikarpova, Julian Tschannen, Carlo A. Furia andBertrand Meyer
A modular theory of object orientation in higher-order UTP
Authors: Frank Zeyda, Thiago Santos, Ana Cavalcanti and Augusto Sampaio
Verification of a Transactional Memory Manager under Hardware Failures and Restarts
Authors: Ognjen Marić and Christoph Sprenger
A Simplified Z Semantics for Presentation Interaction Models
Authors: Judy Bowen and Steve Reeves
Analyzing Clinical Practice Guidelines Using a Decidable Metric Interval-based Temporal Logic
Authors: Morteza Yousefsanati, Wendy MacCaull and Thomas S.E. Maibaum
Invariants, Well-founded Statements and Real-time Program Algebra
Authors: Ian Hayes and Larissa Meinicke
Formal Verification of Operational Transformation
Authors: Yang Liu, Shaojie Zhang, Yi Xu and Chengzheng Sun
SCJ: Memory-safety checking without annotations
Authors: Chris Marriott and Ana Cavalcanti
Log Analysis for Data Protection Accountability
Authors: Denis Butin and Daniel Le Métayer
A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes
Authors: Pedro Antonino, Augusto Sampaio and Jim Woodcock
Checking Liveness Properties of Presburger Counter Systems using Reachability Analysis
Authors: Vasanta Lakshmi K, Aravind Acharya and Raghavan Komondoor
A Graph-based Transformation Reduction to Reach UPPAAL States Faster
Authors: Jonas Rinast, Sibylle Schupp and Dieter Gollmann
Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools
Authors: Alasdair Armstrong, Victor B. F. Gomes and Georg Struth
IscasMC: A Web-Based Probabilistic Model Checker (Tool Paper)
Authors: Ernst Moritz Hahn, Yi Li, Sven Schewe, Andrea Turrini and Lijun Zhang
Proof Patterns for Formal Methods
Authors: Leo Freitas and Iain Whiteside
The VerCors Tool Set for Verification of Concurrent Programs (Tool Paper)
Authors: Stefan Blom and Marieke Huisman
A Symbolic Algorithm for the Analysis of Robust Timed Automata
Authors: Piotr Kordy, Rom Langerak, Sjouke Mauw and Jan Willem Polderman
Efficient Self-Composition for Weakest Precondition Calculi
Authors: Christoph Scheben and Peter Schmitt
Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs
Authors: Subodh Sharma, Vojtech Forejt, Daniel Kroening and Ganesh Narayanaswamy
Object Propositions
Authors: Ligia Nistor, Jonathan Aldrich, Stephanie Balzer and Hannes Mehnert
Revisiting Compatibility of Input-Output Modal Transition Systems
Authors: Ivo Krka, Nicolas D'Ippolito, Nenad Medvidovic and Sebastian Uchitel
Temporal Precedence Checking for Switched Models and its Application to a Parallel Landing Protocol
Authors: Parasara Sridhar Duggirala, Le Wang, Sayan Mitra, Mahesh Viswanathan and Cesar Munoz
Co-induction Simply: Automatic Co-inductive Proofs in a Program Verifier
Authors: Rustan Leino and Michał Moskal
Efficient Tight Field Bounds Computation based on Shape Predicates
Authors: Pablo Ponzio, Nicolas Rosner, Nazareno Aguirre and Marcelo Frias
Automatic Compositional Synthesis of Distributed Systems
Authors: Werner Damm and Bernd Finkbeiner
Refactoring, Refinement, and Reasoning: A Logical Characterization for Hybrid Systems
Authors: Stefan Mitsch, Jan-David Quesel and André Platzer
When Equivalence and Bisimulation Join Forces in Probabilistic Automata
Authors: Yuan Feng and Lijun Zhang