FM 2016: 21ST INTERNATIONAL SYMPOSIUM ON FORMAL METHODS
PROGRAM

Days: Wednesday, November 9th Thursday, November 10th Friday, November 11th

Wednesday, November 9th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 1: Keynote Speech: Manfred Broy
Location: Panorama
09:00
A Logical Approach to Systems Engineering Artifacts: Semantic Relationships and Dependencies beyond Traceability - From Requirements to Functional and Architectural View ( abstract )
10:00-10:30Coffee Break
10:30-12:30 Session 2: Concurrency
Location: Panorama
10:30
An algebra of synchronous atomic steps ( abstract )
11:00
Explaining Relaxed Memory Models with Program Transformations ( abstract )
11:30
Error Invariants for Concurrent Traces ( abstract )
12:00
A Generic Logic for Proving Linearizability ( abstract )
12:30-14:00Lunch Break
14:00-16:00 Session 3A: Model Checking
Chair:
Location: Panorama
14:00
Dealing with Incompleteness in Automata-based Model Checking ( abstract )
14:30
A Model Checking Approach to Discrete Bifurcation Analysis ( abstract )
15:00
Regression Verification for unbalanced recursive functions ( abstract )
15:30
GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking ( abstract )
15:45
Compositional Parameter Synthesis ( abstract )
14:00-16:00 Session 3B: Hybrid Systems
Location: Phoenix
14:00
A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems ( abstract )
14:30
Approximate Bisimulation and Discretization of Hybrid CSP ( abstract )
15:00
Towards Concolic Testing for Hybrid Systems ( abstract )
15:30
From Electrical Switched Networks to Hybrid Automata ( abstract )
16:00-16:30Coffee Break
16:30-18:00 Session 4A: Safety
Location: Panorama
16:30
State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI ( abstract )
17:00
Tighter Reachability Criteria for Deadlock-Freedom Analysis ( abstract )
17:30
Danger Invariants ( abstract )
16:30-18:00 Session 4B: Specification and Verification
Chair:
Location: Phoenix
16:30
Automated Mutual Explicit Induction Proof in Separation Logic ( abstract )
17:00
Recovering high-level conditions from binary programs ( abstract )
17:30
Formal Verification of Multi-Paxos for Distributed Consensus ( abstract )
Thursday, November 10th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 5: Keynote Speech: Peter O'Hearn
Location: Panorama
09:00
Moving Fast with Program Verification Technology ( abstract )
10:00-10:30Coffee Break
10:30-12:30 Session 6A: Program Analysis
Location: Panorama
10:30
Modal Kleene Algebra Applied to Program Correctness ( abstract )
11:00
Mechanised Verification Patterns for Dafny ( abstract )
11:30
Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations ( abstract )
12:00
Sound and Complete Mutation-Based Program Repair ( abstract )
10:30-12:30 Session 6B: Industry Track
Location: Phoenix
10:30
Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems ( abstract )
11:00
Rule-based Incremental Verification Tools Applied to Railway Designs and Regulations ( abstract )
11:30
RIVER: A Binary Analysis Framework using Symbolic Execution and Reversible x86 Instructions ( abstract )
12:00
Model-Based Design of an Energy-System Embedded Controller using Taste ( abstract )
12:30-14:00Lunch Break and FME Business Meeting
14:00-15:45 Session 7A: Learning
Location: Panorama
14:00
Learning Moore Machines from Input-Output Traces ( abstract )
14:30
Finite Model Finding Using the Logic of Equality with Uninterpreted Functions ( abstract )
15:00
Exploring Model Quality for ACAS X ( abstract )
15:30
Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation ( abstract )
14:00-15:00 Session 7B: Industry Track
Location: Phoenix
14:00
Taming Interrupts For Verifying Industrial Multifunction Vehicle Bus Controllers ( abstract )
14:30
Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller ( abstract )
15:45-16:30Coffee Break
Friday, November 11th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 10: Keynote Speech: Jan Peleska
Location: Panorama
09:00
Industrial-strength Model-based Testing of Safety-critical Systems ( abstract )
10:00-10:30Coffee Break
10:30-12:30 Session 11: Timed Systems
Location: Panorama
10:30
Battery-Aware Scheduling in Low Orbit: The GomX-3 Case ( abstract )
11:00
Discounted Duration Calculus ( abstract )
11:30
Validated Simulation-Based Verification of Delayed Differential Dynamics ( abstract )
12:00
Local Planning of Multiparty Interactions with Bounded Horizons ( abstract )
12:30-14:00Lunch Break
14:00-16:00 Session 12A: Abstraction
Location: Panorama
14:00
Refactoring Refinement Structures of Event-B Machines ( abstract )
14:30
Finding Suitable Variability Abstractions for Family-Based Analysis ( abstract )
15:00
Counter-Example Guided Program Verification ( abstract )
15:30
Decoupled simulating abstractions of non-linear ordinary differential equations ( abstract )
14:00-16:00 Session 12B: Security
Location: Phoenix
14:00
SpecCert: Specifying and Verifying Hardware-based Security Enforcement ( abstract )
14:30
Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor ( abstract )
15:00
Automated Verification of Timed Security Protocols with Clock Drift ( abstract )
15:30
Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow ( abstract )
16:00-16:30Coffee Break
16:30-18:00 Session 13: Case Studies
Location: Panorama
16:30
An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for The LEON3 Processor ( abstract )
17:00
Formalising and Validating the Interface Description in the FMI standard ( abstract )
17:15
Equivalence Checking of a Floating-point Unit Against a High-level C Model ( abstract )
17:30
An Implementation of Deflate in Coq ( abstract )