» Timetable

The following timetable might slightly change before the 2nd of April.

Monday 2nd April 2012
14:00 Registration, tea and coffee (Kilburn, lower first floor)
15:45 Welcome (Kilburn, LT 1.1)
16:00 Invited keynote: Mike Edmunds (LT 1.1)
“The Antikythera Mechanism and the Early History of Mechanical Computing”
17:30 Reception (Christie’s bistro)

Tuesday 3rd April 2012
09:00 Registration (lower first floor)
09:30 Invited lecture: Reiner H&ähnle (LT 1.1)
“Formal Verification of Software Product Families”
10:30 Tea/coffee
11:00 ARW Short talks for posters (6 x 5 min slots, LT 1.5)

  • C. Nalon
    A Linear Strategy for Modal Resolution
  • A. Niknafs Kermani and B. Konev
    Symmetry Theorem Proving
  • R. Williams and B. Konev
    Simplified Temporal Resolution Using SAT Solvers
  • C. Sticksel and K. Korovin
    A Note on Model Representation and Proof Extraction in the First-Order Instantiation-based Calculus Inst-Gen
  • M. Meri
    Inverse Resolution in Case-Based Planning Cycle
  • A. Bolotov and V. Shangin
    Natural Deduction in the Setting of Paraconsistent and Paracomplete Logics PCont and PComp

11:30 ARW Posters
12:30 Buffet lunch
13:30 ARW Short talks for posters (6 x 5 min slots, LT 1.5)

  • B. Lellmann and D. Pattinson
    Graphical Construction of Cut Free Sequent Systems Suitable for Backwards Proof Search
  • Ş. Minică
    Automatic Reasoning for Interrogative Logics
  • M. Zawidzki
    Terminating Tableau Calculus for the Logic K(En)
  • D. Tishkovsky, C. Dixon, B. Konev and R. A. Schmidt
    A Labelled Tableau Approach for Temporal Logic with Constraints
  • F. Papacchini and R. A. Schmidt
    Minimal Models for Modal Logics
  • M. J. Gabbay (with C. Wirth)
    Quantifier Rules in Reductive Proof Using Nominal Semantics

14:00 ARW Posters
15:00 Tea/coffee
15:30 ARW Short talks for posters (6 x 5 min slots, LT 1.5)

  • R. Carter and E. M. Navarro-López
    Model Checking by Abstraction for Proving Liveness Properties of Hybrid Dynamical Systems
  • W. Denman
    Verification of Nonpolynomial Systems Using MetiTarski
  • A. Piel
    A Formal Behaviour Representation for the Analysis of Distributed Simulations of Unmanned Aircraft Systems
  • M. Alzahrani and L. Georgieva
    Analysing Data-Sensitive and Time-Sensitive Web Applications
  • Y. Lu and A. Miller
    Timed Analysis of RFID Distance Bounding Protocols
  • R. Kirwan and A. Miller
    Progress on Model Checking Robot Behaviour

16:00 ARW Posters
17:00 ARW Business meeting (for the Organisation Committee)
18:00 Pre-dinner Pub
Rain Bar
80 Great Bridgewater,
M1 5JG
19:30 ARW Dinner
Piccolino Ristorante e Bar
8 Clarence Street,
M2 4DW

Wednesday 4th April 2012
09:00 ARW Invited talk: Daniel Kroening (LT 1.1)
“SAT over an Abstract Domain”
10:00 ARW Short talks for posters (7 x 5 min slots, LT 1.5)

  • W. Sonnex
    Deforestation + Dependent Types = Automated Induction
  • M. Brain
    Using Algebra to Understand Search Spaces
  • A. Armstrong and G. Struth
    Automated Reasoning in Higher-Order Algebra
  • Q. Mahesar and V. Sorge
    Generation of Large Size Quasigroup Structures Using Algebraic Constraints
  • O. Al-Hassani, Q. Mahesar, C. Sacerdoti Coen and V. Sorge
    A Term Rewriting System for Kuratowski’s Closure-Complement
  • F. Cavallo, S. Colton and A. Pease
    Uncertainty Modelling in Automated Concept Formation
  • M. Khodadadi, D. Tishkovsky and R. A. Schmidt
    METTEL2: Towards a Prover Generation Platform

10:35 Tea/coffee
11:00 ARW Posters
12:30 Buffet lunch
13:30 End of the workshop