IFM 2020: INTEGRATED FORMAL METHODS
PROGRAM

Days: Tuesday, November 17th Wednesday, November 18th Thursday, November 19th

Tuesday, November 17th

View this program: with abstractssession overviewtalk overview

08:45-10:00 Session 1: Welcome and Invited Talk 1

All times listed are in GMT.

08:45
Welcome (abstract)
09:00
Verification with Stochastic Games: Advances and Challenges (abstract)
10:30-11:30 Session 2: Integrating Machine Learning and Formal Modelling

All times listed are in GMT.

10:30
Clustering-Guided SMT(LRA) Learning (abstract)
10:50
Grey-Box Learning of Register Automata (abstract)
11:10
Formal Policy Synthesis for Continuous-State Systems via Reinforcement Learning (abstract)
13:00-14:00 Session 3: Domain-Specific Approaches

All times listed are in GMT.

13:00
Reformulation of SAT into a PolynomialBox-Constrainted Optimization Problem (abstract)
13:20
Chain of events: Modular Process Models for the Law (abstract)
13:40
Meeduse: A Tool to Build and Run Proved DSLs (abstract)
14:30-15:30 Session 4: Program Analysis and Testing

All times listed are in GMT.

14:30
Formal methods for GPGPU programming: is the demand met? (abstract)
14:50
Automatic Generation of Test Stable Floating Point Code (abstract)
15:10
Jaint: A Framework for User-Defined Dynamic Taint-Analyses based on Dynamic Symbolic Execution of Java Programs (abstract)
Wednesday, November 18th

View this program: with abstractssession overviewtalk overview

10:00-11:00 Session 5: Verification of Interactive Behaviour

All times listed are in GMT.

10:00
Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch (abstract)
10:20
History-based Specification and Verification of Java Collections in KeY (abstract)
10:40
Active Objects with Deterministic Behaviour (abstract)
11:30-12:30 Session 6: Static Analysis

All times listed are in GMT.

11:30
Detection of Polluting Test Objectives for Dataflow Criteria (abstract)
11:50
Tight Error Analysis in Fixed-point Arithmetics (abstract)
12:10
Lock and Fence When Needed: State Space Exploration + Static Analysis = Improved Fence and Lock Insertion (abstract)
14:00-15:00 Session 7: Formal Verification

All times listed are in GMT.

14:00
Synthesizing clock-efficient timed automata (abstract)
14:20
A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-based Sorting Algorithms (abstract)
14:40
Formal Verification of Executable Complementation and Equivalence Checking for Büchi Automata (abstract)
15:30-16:30 Session 8: Invited Talk 2

All times listed are in GMT.

15:30
Verifying Parallel and Distributed Systems: The Observer Problem (abstract)
Thursday, November 19th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 9: Invited Talk 3

All times listed are in GMT.

09:00
Towards Verified Stochastic Variational Inference for Probabilistic Programs (abstract)
10:30-11:30 Session 10: Algebraic Techniques

All times listed are in GMT.

10:30
Algebra-based Loop Synthesis (abstract)
10:50
Philosophers may Dine - Definitively! (abstract)
11:10
PALM: a technique for Process ALgebraic specification Mining (abstract)
13:00-14:00 Session 11: Modelling and Verification in B and Event-B

All times listed are in GMT.

13:00
Generating SPARK from Event-B Models (abstract)
13:20
An Event-B Based Generic Framework for Hybrid Systems Formal Modelling (abstract)
13:40
Fast and Effective Well-Definedness Checking for Formal Models (abstract)