19th International Symposium on Formal Methods

Download PDF file

Overall Program

12 May 2014	13 May 2014	14 May 2014	15 May 2014	16 May 2014
Workshops	Workshops	FM2014	FM2014	FM2014
FMTV	UTP FSFMA AI4FM ESSS	Keynote 1 Session 1A/1B Lunch Session 2A/2B Session 3A/3B Reception	Keynote 2 Session 4A/4B Lunch Session 5 Banquet	Keynote 3 Session 6 Lunch Session 7
Tutorials Tutorial 2(Full Day) Tutorial 5(Full Day)	Tutorials Tutorial 1(Full Day) Tutorial 3(am) and 4(pm) Doc Symposium

NOTE: The workshop QFM has now been cancelled.
For 12-13 May, here are the suggested timings of breaks: Morning break: 10:30-11:00; Lunch: 12:30-2:00pm; Afternoon break: 3:30-4:00pm.
Some workshops/tutorials may have a bit different timings.

Programs

WEDNESDAY, May 14 08:45-9:00: Opening Address by David S. Rosenblum, Jin Song Dong and Cliff Jones. Location: LT15 9:00-10:00: “Proof Engineering Considered Essential” (keynote talk) by Gerwin Klein, chaired by Jun Sun. Location: LT15
10:00-10:30: Coffee break
10:30-12:30: Session 1A Location: LT15 Session Chair: Ian Hayes	10:30-12:30: Session 1B Location: SR1 COM1-02-06 Session Chair: Lijun Zhang
“Co-induction Simply: Automatic Co-inductive Proofs in a Program Verifier”, by Rustan Leino and Michał Moskal	“Formal Verification of Operational Transformation”, by Yang Liu, Yi Xu, Shaojie Zhang, and Chengzheng Sun
“Proof Patterns for Formal Methods”, by Leo Freitas and Iain Whiteside	“SCJ: Memory-Safety Checking without Annotations”, by Chris Marriott and Ana Cavalcanti
“Flexible Invariants Through Semantic Collaboration”, by Nadia Polikarpova, Julian Tschannen, Carlo A. Furia, and Bertrand Meyer	“A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes”, by Pedro Antonino, Augusto Sampaio, and Jim Woodcock
“Verification of a Transactional Memory Manager under Hardware Failures and Restarts” by Ognjen Marić and Christoph Sprenger	“Revisiting Compatibility of Input-Output Modal Transition Systems Krka”, by Ivo Krka, Nicolas D'Ippolito, Nenad Medvidovic, and Sebastian Uchitel
12:30-14:00: Lunch
14:00-16:00: Session 2A Location: LT15 Session Chair: Bernhard Aichernig	14:00-16:00: Session 2B Location: SR1 COM1-02-06 Session Chair: Ralf Huuck
“Temporal Precedence Checking for Switched Models and its Application to a Parallel Landing Protocol”, by Parasara Sridhar Duggirala, Le Wang, Sayan Mitra, Mahesh Viswanathan, and Cesar Munoz	“A Graph-based Transformation Reduction to Reach UPPAAL States Faster”, by Jonas Rinast, Sibylle Schupp, and Dieter Gollmann
“Refactoring, Refinement, and Reasoning: A Logical Characterization for Hybrid Systems”, by Stefan Mitsch, Jan-David Quesel, and André Platzer	“Management of Time Requirements in Component-based Systems”, by Yi Li, Tian Huat Tan, and Marsha Chechik
“When Equivalence and Bisimulation Join Forces in Probabilistic Automata”, by Yuan Feng and Lijun Zhang	“A Symbolic Algorithm for the Analysis of Robust Timed Automata”, by Piotr Kordy, Rom Langerak, Sjouke Mauw, and Jan Willem Polderman
“Automatic Compositional Synthesis of Distributed Systems”, by Werner Damm and Bernd Finkbeiner	“Invariants, Well-founded Statements and Real-time Program Algebra”, by Ian Hayes and Larissa Meinicke
16:00-16:30: Coffee break
16:30-18:30: Session 3A Location: LT15 Session Chair: Ana Cavalcanti	16:30-18:30: Session 3B Location: SR1 COM1-02-06 Session Chair: Yang Liu
“Object Propositions”, by Ligia Nistor, Jonathan Aldrich, Stephanie Balzer, and Hannes Mehnert	“Compositional Synthesis of Concurrent Systems through Causal Model Checking and Learning”, by Shang-Wei Lin and Pao-Ann Hsiung
“Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools”, by Alasdair Armstrong, Victor B. F. Gomes, and Georg Struth	“Checking Liveness Properties of Presburger Counter Systems using Reachability Analysis”, by Vasanta Lakshmi K, Aravind Acharya, and Raghavan Komondoor
“Efficient Tight Field Bounds Computation based on Shape Predicates”, by Pablo Ponzio, Nicolas Rosner, Nazareno Aguirre, and Marcelo Frias	“IscasMC: A Web-Based Probabilistic Model Checker” (tool paper), by Ernst Moritz Hahn, Yi Li, Sven Schewe, Andrea Turrini, and Lijun Zhang
“Contracts in Practice”, by H.-Christian Estler, Carlo A. Furia, Martin Nordio, Marco Piccioni, and Bertrand Meyer	“Automated Real Proving in PVS via MetiTarski”, (tool paper), by William Denman and Cesar Munoz
19:00-21:00 Welcome Reception
THURSDAY, May 15^th, 2014 9:00-10:00:Validity Checking of Putback Transformations in Bidirectional Programming (keynote talk), by Zhenjiang Hu, chaired by Cliff Jones. Location: LT15
10:00-10:30: Coffee break
10:30-12:30: Session 4A Location: LT15 Session Chair: Sjouke Mauw	10:30-12:30: Session 4B: Industry Track A Location: SR1 COM1-02-06 Session Chair: Peter Gorm Larsen
“Computing Quadratic Invariants with Min- and Max-Policy Iterations:a Practical Comparison”, by Pierre Roux and Pierre-Loic Garoche	“Formal Verification of a Descent Guidance Control Program of a Lunar Lander”, by Hengjun Zhao, Mengfei Yang, Naijun Zhan, Bin Gu, Liang Zou, and Yao Chen
“Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs”, by Subodh Sharma, Vojtech Forejt, Daniel Kroening, and Ganesh Narayanaswamy	“MDP-based Reliability Analysis of an Ambient Assisted Living System”, by Yan Liu, Lin Gui, and Yang Liu
“Quiescent Consistency: Defining and Verifying Relaxed Linearizability”, by John Derrick, Heike Wehrheim, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, and Oleg Travkin	“Formal Verification of Lunar Rover Control Software Using UPPAAL”, by Lijun Shan
“The VerCors Tool Set for Verification of Concurrent Programs” (tool paper), by Stefan Blom and Marieke Huisman	“Diagnosing Industrial Business Processes: Early Experiences”, by Suman Roy, A. S. M. Sajeev, and Srivibha Sripathy
12:30-14:00: Lunch
14:00-16:00: Session 5 Location: LT15 Session Chair: John Fitzgerald “Efficient Runtime Monitoring with Metric Temporal Logic: A Case Study in the Android Operating System”, by Hendra Gunadi and Alwen Tiu “Efficient Self-Composition for Weakest Precondition Calculi”, by Christoph Scheben and Peter Schmitt “The Wireless Fire Alarm System: Ensuring Conformance to Industrial Standards through Formal Verification”, by Sergio Feo-Arenis, Bernd Westphal, Daniel Dietsch, Marco Muniz, and Ahmad Siyar Andisha “Formalizing and Verifying a Modern Build Language”, by Maria Christakis, Rustan Leino, and Wolfram Schulte
16:00-16:30: Coffee break
17:30-21:00: Conference Banquet
FRIDAY, May 16^th, 2014 9:00-10:00: Keynote 3: “Engineering UToPiA Formal Semantics for CML” (keynote talk), by Jim Woodcock, chaired by Jin Song Dong. Location: LT15
10:00-10:30: Coffee break
10:30-12:30: Session 6 Location: LT15 Session Chair: Lindsay Groves “Definition, Semantics, and Analysis of Multirate Synchronous AADL”, by Kyungmin Bae, Peter Olveczky, and Jose Meseguer “A Modular Theory of Object Orientation in Higher-Order UTP”, by Frank Zeyda, Thiago Santos, Ana Cavalcanti, and Augusto Sampaio “A Simplified Z Semantics for Presentation Interaction Models”, by Judy Bowen and Steve Reeves “40 Years of Formal Methods” (distinguished talk), by Dines Bjørner
12:30-14:00: Lunch / FME Meeting. Location: SR1
14:00-16:00: Session 7 Location: LT15 Session Chair: Dominique Méry “TrustFound: Towards a Formal Foundation for Model Checking Trusted Computing Platforms”, by Guangdong Bai, Jianan Hao, Jianliang Wu, Yang Liu, Zhenkai Liang, and Andrew Martin “Knowledge-based Automated Repair of Authentication Protocols”, by Borzoo Bonakdarpour, Reza Hajisheykhi, and Sandeep Kulkarni “Towards a Formal Analysis of Information Leakage for Signature Attacks in Preferential Elections”, by Roland Wen, Annabelle McIver, and Carroll Morgan “Log Analysis for Data Protection Accountability”, by Denis Butin and Daniel Le Métayer
16:00-16:15 Closing Session