The Workshop will take place on level 5 of the Sir Alwyn Williams (SAW) building.
The SAW building can be found on the "Location Information" page.
Monday 11th April
| 10:00 |
Registration and Coffee |
| 10:50 |
Welcome talk |
| 11:00 |
Short Talks |
|
| 11:00 |
Ryan Kirwan |
Abstraction for Model Checking Robot Behaviour |
| 11:05 |
Mohammad Khodadadi |
MetTeL: A Generic Tableau Prover |
| 11:10 |
Nourah Shenaiber |
Smart Semantic Tree Theorem Prover |
| 11:15 |
Robert Rothenberg |
Proof-Theoretic Soundness and Completeness |
| 11:20 |
Murdoch Gabbay |
Metamathematics based on nominal terms and nominal logic:
foundations of a nominal theorem-prover |
| 11:25 |
Fabio Papacchini |
A Modal Tableau Approach for Minimal Model Generation |
|
| 11:45 |
Poster Session |
|
| 12:00 |
Lunch will be provided |
|
| 13:00 |
Invited speaker: Colin Stirling |
| 14:00 |
Short Talks |
|
| 14:00 |
Yuhui Lin |
Productive use of failure in top-down formal methods |
| 14:05 |
Ekaterina Komendantskaya |
Coalgebraic Derivations in Logic Programming |
| 14:10 |
Clare Dixon |
The Application of AI Techniques to Deformation in Metal Manufacturing |
| 14:15 |
Matej Urbas |
Hetrogeneous Proofs: Spider Diagrams meet Higher-Order Provers |
| 14:20 |
Richard Stocker |
Towards the Formal Verification of Human-Agent Teamwork |
|
| 14:45 |
Poster Session |
|
|
| 16:00 |
Pannel Discussion |
| 17:00 |
End of Day 1 |
| 19:00 |
Dinner at Bothy |
|
| Bothy Glasgow |
| 11 Ruthven Lane |
| Hillhead |
| Glasgow West End |
| G12 9BG |
|
Tuesday 12th April
| 10:30 |
Coffee |
| 10:50 |
Introduction |
| 11:00 |
Short Talks |
|
| 11:00 |
Aliaa Alabdali |
Modelling of Wireless Local Area Network Security Attacks in Alloy |
| 11:05 |
Liam O'Reilly |
Compositional Reasoning for Processes and Data |
| 11:10 |
Alexander Bolotov |
Natural Deduction in the setting of Paraconsistent Logic |
|
| 11:45 |
Poster Session |
|
| 12:00 |
Lunch will be provied |
|
| 13:00 |
Invited speaker: Patricia Johann |
| 14:00 |
Short Talks |
|
| 14:00 |
Dmitry Tishkovsky |
Solving rule admissibility problem for S4 by a tableau method |
| 14:05 |
Iain McGinnis |
Typestate modelling and verification with Hanoi |
| 14:10 |
David Berry |
The Logical Verification of Security Protocols |
|
| 14:20 |
Poster Session |
|
|
| 15:20 |
End of Day 2 |