19th International Symposium on Formal Methods

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