19th International Symposium on Formal Methods


Accepted Main Track 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