Institute for Mathematical Sciences Event Archive
Workshop on Higher-Order Model Checking (HOMC) + Communicating, Distributed and Parameterised Systems (CDPS)
(19 - 23 September 2016)
Venue: IMS Auditorium
Organizing Committee · Visitors and Participants · Overview · Activities · Venue
Monday, 19 Sep 2016 |
|
09:25am - 09:30am |
Registration |
09:30am - 10:30am |
Automata-based analysis of threaded programs (PDF) |
10:30am - 11:00am |
--- Group Photo & Coffee Break --- |
11:00am - 12:00nn |
Systems with parametric thread creation (PDF) |
12:00nn - 02:30pm |
--- Lunch Break --- |
02:30pm - 03:30pm |
Nested words for order-2 pushdown systems (PDF) |
03:30pm - 04:00pm |
--- Coffee Break --- |
04:00pm - 05:00pm |
Summaries for context-free games (PDF) |
Tuesday, 20 Sep 2016 |
|
09:25am - 09:30am |
Registration |
09:30am - 12:00nn |
Tutorial: Verification of concurrent data structures (PDF) |
12:00nn - 02:00pm |
--- Lunch Break --- |
02:00pm - 03:30pm |
Tutorial: Introduction to collapsible pushdown automata and higher-order recursion schemes (PDF) |
03:30pm - 04:00pm |
--- Coffee Break --- |
04:00pm - 05:30pm |
Tutorial: Applications of higher-order model checking to program verification (PDF) Hiroshi Unno, University of Tsukuba, Japan |
Wednesday, 21 Sep 2016 |
|
09:25am - 09:30am |
Registration |
09:30am - 10:15am |
Higher-order model checking in direct style (PDF) |
10:15am - 11:00am |
Nominal games: a semantics paradigm for effectful languages (PDF) |
11:00am - 11:30am |
--- Coffee Break --- |
11:30am - 12:15pm |
Refinement types and higher-order constrained horn clauses (PDF) |
12:15pm - 01:00pm |
Higher-order Buchi types (PDF) |
01:00pm - 02:00pm |
--- Lunch Break --- |
|
Social Activities - Marina Bay |
Thursday, 22 Sep 2016 |
|
09:25am - 09:30am |
Registration |
09:30am - 10:15am |
How to decide quantitative properties for higher-order program with nature? (PDF) |
10:15am - 10:45am |
--- Coffee Break --- |
10:45am - 11:30am |
First steps towards probabilistic higher-order model-checking (PDF) |
11:30am - 12:15pm |
On two notions of higher-order model checking (PDF) |
12:15pm - 02:00pm |
--- Lunch Break --- |
02:00pm - 02:45pm |
Modular verification of higher-order functional programs |
02:45pm - 03:30pm |
Finitary proof systems for Kozen's mu (PDF) Graham Leigh,
University of Gothenburg, Sweden |
03:30pm - 04:00pm |
--- Coffee Break --- |
04:00pm - 04:45pm |
Automata, logic and games for higher-type Bohm trees (PDF) |
04:45pm - 05:30pm |
Negations in refinement intersection type systems (PDF) |
Friday, 23 Sep 2016 |
|
09:25am - 09:30am |
Registration |
09:30am - 10:15am |
Compiling untyped Lambda Calculus to lower-level code by game semantics and partial evaluation (PDF) |
10:15am - 10:45am |
--- Coffee Break --- |
10:45am - 11:30am |
Automata theory and game semantics of higher-order computation (PDF) |
Organizing Committee · Visitors and Participants · Overview · Activities · Venue