FM 2019: 23RD INTERNATIONAL SYMPOSIUM ON FORMAL METHODS
PROGRAM

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

Wednesday, October 9th

View this program: with abstractssession overviewtalk overview

10:30-12:30 Session 2A: Verification
10:30
Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm (abstract)
11:00
Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions (abstract)
11:30
Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol (abstract)
12:00
On the Nature of Symbolic Execution (abstract)
10:30-12:30 Session 2B: Synthesis Techniques
10:30
GR(1)*: GR(1) Specifications Extended with Existential Guarantees (abstract)
11:00
Counterexample-Driven Synthesis for Probabilistic Program Sketches (abstract)
11:30
Synthesis of Railway Signaling Layout from Local Capacity Specifications (abstract)
12:00
Pegasus: A Framework for Sound Continuous Invariant Generation (abstract)
15:30-17:00 Session 4A: Concurrency
15:30
A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems (abstract)
16:00
Verifying Correctness of Persistent Concurrent Data Structures (abstract)
16:30
Compositional Verication of Concurrent Systems by Combining Bisimulations (abstract)
15:30-16:00 Session 4B: Journal First Track 1
15:30
Alloy*: a general-purpose higher-order relational constraint solver (abstract)
16:00-17:00 Session 5: Model Checking Circus
16:00
Towards a Model-Checker for Circus (abstract)
16:30
Circus2CSP: A Tool for Model-Checking Circus Using FDR (abstract)
Thursday, October 10th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 7: Keynote 2
09:00
Formal Methods for Security Functionality and for Secure Functionality (abstract)
10:30-12:30 Session 8A: Model Checking
10:30
How Hard is Finding Shortest Counter-Example Lassos in Model Checking? (abstract)
11:00
From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata (abstract)
11:30
Generic Partition Refinement and Weighted Tree Automata (abstract)
12:00
Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games (abstract)
10:30-12:30 Session 8B: Analysis Techniques 1
10:30
Abstract Execution (abstract)
11:00
Static Analysis for Detecting High-Level Races in RTOS Kernels (abstract)
11:30
Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic (abstract)
12:00
An Axiomatic Approach to Liveness for Differential Equations (abstract)
Friday, October 11th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 10: Keynote 3
09:00
Successes in Deployed Verified Software (and Insights on Key Social Factors) (abstract)
10:30-12:30 Session 11A: Analysis Techniques 2
10:30
Local Consistency Check in Synchronous Dataflow Models (abstract)
11:00
Gray-Box Monitoring of Hyperproperties (abstract)
11:30
Quantitative Verification of Numerical Stability for Kalman Filters (abstract)
12:00
Concolic Testing Heap-Manipulating Programs (abstract)
10:30-12:30 Session 11B: Specification Languages
10:30
Formal Semantics Extraction from Natural Language Specifications for ARM (abstract)
11:00
GOSPEL - Providing OCaml with a Formal Specification Language (abstract)
11:30
Unification in Matching Logic (abstract)
12:00
Embedding High-Level Formal Specifications into Applications (abstract)
14:00-15:30 Session 12A: Reasoning Techniques
14:00
Value-Dependent Information-Flow Security on Weak Memory Models (abstract)
14:30
Reasoning Formally about Database Queries and Updates (abstract)
15:00
Abstraction and Subsumption in Modular Verification of C Programs (abstract)
14:00-14:30 Session 12B: Journal First Track 2
14:00
Unifying separation logic and region logic to allow interoperability (abstract)
14:30-15:30 Session 13: Modelling Languages
14:30
IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain (abstract)
15:00
APML: An Architecture Proof Modelling Language (abstract)
16:00-17:30 Session 14A: Learning-Based Techniques and Applications
16:00
Learning Deterministic Variable Automata over Infinite Alphabets (abstract)
16:30
L*-Based Learning of Markov Decision Processes (abstract)
17:00
Star-Based Reachability Analysis of Deep Neural Networks (abstract)
16:00-16:30 Session 14B: Journal First Track 3
16:00
Conditions of contracts for separating responsibilities in heterogeneous systems (abstract)
16:30-17:30 Session 15: Refactoring and Reprogramming
16:30
SOA and the Button Problem (abstract)
17:00
Controlling Large Boolean Networks with Temporary and Permanent Perturbations (abstract)