Programme

14th International Colloquium on Theoretical Aspects of Computing

ICTAC 2017

23-27 October 2017, Hanoi, Vietnam
Preliminary Conference Programme
(Subject to change)
Tutorial Day 1: Monday, 23 October, 2017
Tutorial Venue: VNU Campus, Building E3, 144 Xuan Thuy
9:00 – 10:15 Tutorial 1, June Andronick, UNSW, Australia
10:15 – 10:45 Coffee Break
10:45 – 12:00 Tutorial 1 (cont’d), June Andronick, UNSW, Australia
12:00 – 14:00 Lunch Break
14:00 – 15:15 Tutorial 1: Principles of Probabilistic Programming, Joose-Pieter Katoen, RWTH Aachen University, Germany
15:15 – 15:45 Coffee Break
15:45 – 17:00 Tutorial 1: Principles of Probabilistic Programming (cont’d), Joose-Pieter Katoen, RWTH Aachen University, Germany

 

Tutorial Day 2: Tuesday, 24 October, 2017
Tutorial Venue: VNU Campus, Building E3, 144 Xuan Thuy
9:00 – 10:15 Tutorial 3, Rustan M. Leino, Microsoft Research, Redmond, USA
10:15 – 10:45 Coffee Break
10:45 – 12:00 Tutorial 3 (cont’d), Rustan M. Leino, Microsoft Research, Redmond, USA
12:00 – 14:00 Lunch Break
14:00 – 15:15 Tutorial 4: Towards a Contract-Based Model of Evolving Software Architecture, Zhiming Liu, Southwest University, China
15:15 – 15:45 Coffee Break
15:45 – 17:00 Tutorial 4: Towards a Contract-Based Model of Evolving Software Architecture (cont’d), Zhiming Liu, Southwest University, China

 

Conference Day 1: Wednesday, 25 October, 2017
Conference Venue: Nguy Nhu Kontum Hall, VNU, 19 Le Thanh Tong
8:00 – 8:30 Registration
8:30 – 8:40 Opening
8:40 – 9:40 Keynote: From Hoare Logic to Owicki-Gries and Rely-Guarantee for Interruptible eChronos and Multicore seL4, June Andronick
9:40 – 10:10 Coffee Break
10:10 – 12:10 Logics
A Formal Proof Generator from Semi-formal Proof Documents, Adrián Riesco and Kazuhiro Ogata
Institutions for Behavioural Dynamic Logic with Binders, Rolf Hennicker and Alexandre Madeira
The Delay Monad and Restriction Categories, Tarmo Uustalu and Niccolò Veltri
Logical Characterisation of Parameterised Bisimulations, Divyanshu Bagga and S. Arun Kumar
12:10 – 14:00 Lunch Break
14:00 – 15:00 Calculi
A Probabilistic Semantics for the pure $\lambda$-calculus, Alessandra Di Pierro
Towards a Calculus for Dynamic Architectures, Diego Marmsoler
15:00 – 15:30 Coffee Break
15:30 – 16:30 Concurrency
Class-diagrams for Abstract Data Types, Thai Son Hoang, Colin Snook, Dana Dghaym and Michael Butler
Value-Based or Conflict-Based? Opacity Definitions for STMs, Jürgen König and Heike Wehrheim
16:30 – 17:30 Business Meeting
18:00 – 20:00 Reception
Conference Day 2: Thursday, 26 October, 2017
Conference Venue: Nguy Nhu Kontum Hall, VNU, 19 Le Thanh Tong
9:00 – 10:00 Keynote: Tweaking The Odds — Parameter Synthesis in Markov Models
Joost-Pieter Katoen
10:00 – 10:30 Coffee Break
10:30 – 12:00 Automata
Derived-Term Automata of Weighted Rational Expressions with Quotient Operators, Akim Demaille, Thibaud Michaud
Polynomial Time Learner for Inferring Subclasses of Internal Contextual Grammars with Local Maximum Selectors, Abhisek Midya, DG Thomas, Saleem Malik and Alok Kumar Pani
Trace Relations and Logical Preservation for Continuous-Time Markov Decision Processes, Arpit Sharma
12:00 – 13:30 Lunch Break
13:30 – 19:00 Excursion
19:00 – 21:00 Conference Banquet
Conference Day 3: Friday, 27 October, 2017
Conference Venue: Nguy Nhu Kontum Hall, VNU, 19 Le Thanh Tong
9:00 – 10:00 Keynote: Directions to and for Verified Software, K. Rustan M. Leino
10:00 – 10:30 Coffee Break
10:30 – 12:00 SMT Solvers and Algorithms
Constructing Cycles in the Simplex Method for DPLL(T), Bertram Felgenhauer and Aart Middeldorp
Tableaux with Partial Caching for Hybrid PDL with Satisfaction Statements, Agathoklis Kritsimallis
PTrie: Data Structure for Compressing and Storing Sets via Prefix Sharing, Peter Gjøl Jensen, Kim Guldstrand Larsen, and Jirí Srba
12:00 – 14:00 Lunch Break
14:00 – 15:30 Algorithm and Security
Smaller-State Implementations of 2D FSSP Algorithms – Recent Developments -, Hiroshi Umeo, Keisuke Kubo and Akira Nomura
Inferring Secrets by Guided Experiments, Quoc Huy Do, Richard Bubel and Reiner Hähnle
ECBC: A High Performance Educational Certificate Blockchain with Efficient Query, Yuqin Xu, Shangli Zhao, Lanju Kong, Yongqing Zheng, Shidong Zhang, Qingzhong Li
15:30 – 16:00 Closing Session