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.
Chair:
| 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.
Chair:
| 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.
Chair:
| 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.
Chair:
| 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.
Chair:
| 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.
Chair:
| 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.
Chair:
| 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.
Chair:
| 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.
Chair:
| 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.
Chair:
| 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.
Chair:
| 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) |