CARI/ICTAC School, ICTAC Conference Program
All of the school/conference events take place at STIAS (Stellenbosch Institute for Advanced Study, 10 Marais Road).
Day 1: Friday 12 October 2018 (School)
Auditorium 1
8:30 |
Tutorials
Yves Bertot Interactive Theorem Proving and Program Development 1 |
10:30 | Break |
11:00 |
Yves Bertot
Interactive Theorem Proving and Program Development 2 |
12:30 | Lunch |
14:00 |
Willem Visser
Symbolic Execution for Java 1 |
15:30 | Break |
16:00 |
Willem Visser
Symbolic Execution for Java 2 |
18:00 | Close |
Day 2: Saturday 13 October 2018 (School)
Manor Library
9:00 |
Tutorials
Vincent Cheval Verification of Security Protocols: From Confidentiality to Privacy 1 |
11:00 | Break |
11:15 |
Vincent Cheval
Verification of Security Protocols: From Confidentiality to Privacy 2 |
12:45 | Lunch |
13:45 |
Thomas A. Meyer
An Introduction to Description Logics 1 |
15:15 | Break |
15:30 |
Thomas A. Meyer
An Introduction to Description Logics 2 |
17:30 | Close |
Day 3: Sunday 14 October 2018 (School)
Manor Library
9:00 |
Tutorials
Peter Thiemann Derivation beyond Regular Languages 1 |
11:00 | Break |
11:15 |
Peter Thiemann
Derivation beyond Regular Languages 2 |
12:45 | Lunch |
13:45 |
Ina Schaefer, Loek Cleophas
The Correctness-by-Construction Approach to Programming 1 |
15:15 | Break |
15:30 |
Ina Schaefer, Loek Cleophas
The Correctness-by-Construction Approach to Programming 2 |
17:30 | Close |
Day 4: Monday 15 October 2018 (School, Workshops)
Manor Library
8:30 |
Tutorial
Martin Leucker Runtime Verification: Some Basics and Some Latest Developments 1 |
10:30 | Break |
11:00 |
Martin Leucker
Runtime Verification: Some Basics and Some Latest Developments 2 |
12:30 | Lunch |
14:00 |
Workshop: Algebra and Coalgebra in Languages and Automata
Alexandra Silva CALF: A Categorical Automata Learning Framework Sergey Goncharov Equational Theories for Real-Time Coalgebraic State Machines |
15:30 | Break |
16:00 |
Hellis Tamm
Atoms of Regular Languages Peter Thiemann On Compositionally Defined Functions on Regular Expressions Tarmo Uustalu Derivatives of Existentially Regular Trace Languages |
18:00 | Close |
Breakaway room 1&2
8:45 |
Workshop: Finding Software Errors before They Find Us
Opening |
9:00 |
Matthew B. Dwyer, Antonio Filieri
Towards Conditional Probabilistic Software Analysis |
10:30 | Break |
11:00 |
Yunho Kim
Directed Compositional Concolic Testing with Function Summary Refinement for Crashing Input Generation Jaco Geldenhuys Concolic vs Concolic Michael W. Whalen Veritesting with SPF |
12:30 | Lunch |
14:00 |
Willem Visser
Fuzzing and Symbolic Execution Ina Schaefer Confidentiality-by-Construction |
15:30 | Break |
16:00 |
Jan Taljaard
Experiments with Green Alex Leid Smart Contract Analysis |
17:00 | Discussion |
18:00 | Close |
Day 5: Tuesday 16 October 2018 (Conference)
First session 8.45-10.00 joint with CARI in Auditorium 2; rest of the day Auditorium 1
8:45 | ICTAC opening |
9:00 |
ICTAC/CARI joint invited talk
[Session chair: Hélène Kirchner] Yves Bertot Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs |
10:00 | Break |
10:30 |
Contributed talks
[Session chair: David Pym] Bertram Felgenhauer, Franziska Rapp Layer Systems for Confluence -- Formalized Beniamino Accattoli Proof Nets and the Linear Substitution Calculus Apiwat Chantawibul, Paweł Soboćinski Monoidal Multiplexing David Janin Spatio-Temporal Domains: An Overview |
12:30 | Lunch |
14:00 |
[Session chair: Éric Badouel]
Sergey Goncharov, Christoph Rauch, Lutz Schröder A Metalanguage for Guarded Iteration Härmel Nestra Double Applicative Functors Fredrik Dahlqvist, Louis Parlant, Alexandra Silva Layer by Layer: Combining Monads |
15:30 | Break |
16:00 |
[Session chair: Martin Leucker]
David Venhoek, Joshua Moerman, Jurriaan Rot Fast Computations on Ordered Nominal Sets Martin Jonáš, Jan Strejček Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers Mikhail Rybakov, Dmitry Shkatov Computational Complexity and Expressivity of Branching- and Alternating-Time Temporal Logics with Finitely Many Variables |
17:30 | PC chair report, best paper award |
17:45 | Close |
Day 6: Wednesday 17 October 2018 (Excursion)
8.30 | Departure by buses from Stellenbosch Town Hall (37 Plein Street) |
Full-day excursion to Cape Peninsula (Boulders Penguin Colony in Simons Town, Cape Point and Cape of Good Hope) | |
Winetasting at Groot Constantia | |
18.30 | Boerebraai at Middelvlei |
Day 7: Thursday 18 October 2018 (Conference)
Auditorium 2
9:00 |
Invited talk
[Session chair: Tarmo Uustalu] Peter Thiemann From Logic to Automata by Derivation |
10:00 |
Contributed talks
Martin Berglund, Willem Bester, Brink van der Merwe Formalising Boost POSIX Regular Expression Matching |
10:30 | Break |
11:00 |
[Session chair: Peter Thiemann]
Éric Badouel, Rodrigue Aimé Djeumen Djatcha Modular Design of Domain-Specific Languages Using Splittings of Catamorphisms Ryoma Senda, Yoshiaki Takata, Hiroyuki Seki Complexity Results on Register Context-Free Grammars and Register Tree Automata Hiroshi Umeo, Naoki Kamikawa, Gen Fujita The Smallest FSSP Partial Solutions for One-Dimensional Ring Cellular Automata: Symmetric and Asymmetric Synchronizers |
12:30 | Lunch |
14:00 |
Invited talk
[Session chair: Willem Visser] Thomas A. Meyer What is Knowledge Representation and Reasoning? |
15:00 |
Contributed talks
Henriette Harmse, Katarina Britz, Aurona Gerber Generating Armstrong Aboxes for ALC Tboxes |
15:30 | Break |
16:00 |
[Session chair: Ina Schaefer]
Wilmer Ricciotti, James Cheney Explicit Auditing Manuel Töws, Heike Wehrheim Information Flow Certificates Henrich Lauko, Petr Ročkai, Jiří Barnat Symbolic Computation via Program Transformation |
17:30 | Close |
18:15 | Departure by bus from from Stellenbosch Town Hall (37 Plein Street) |
Conference dinner at Jardine's Restaurant on the Jordan Wine Estate |
Day 8: Friday 19 October 2018 (Conference)
Auditorium 2
9:00 |
Invited talk
[Session chair: Bernd Fischer] Gennaro Parlato Finding Rare Concurrent Programming Bugs: An Automatic, Symbolic, Randomized, and Parallelizable Approach |
10:00 |
Contributed talks
Siyang Xiao, Hanru Jiang, Hongjin Liang, Xinyu Feng Non-preemptive Semantics for Data-Race-Free Programs |
10:30 | Break |
11:00 |
[Session chair: Gennaro Parlato]
Gerco van Heert, Justin Hsu, Joël Ouaknine, Alexandra Silva Convex Language Semantics for Nondeterministic Probabilistic Automata Ruggero Lanotte, Simone Tini Weak Bisimulation Metrics in Models with Nondeterminism and Continuous State Spaces Pedro R. D'Argenio, Raúl E. Monti Input/Output Stochastic Automata with Urgency: Confluence and Weak Determinism |
12:30 | Lunch |
14:00 |
[Session chair: David Janin]
Martin Berglund, Ina Schaefer An Automata-Based View on Configurability and Uncertainty Omer Nguena Timo, Alexandre Petrenko, S. Ramesh Checking Sequence Generation for Symbolic Input/Output FSMs by Constraint Solving Einar Broch Johnsen, Martin Steffen, Johanna Beate Stumpf, Lars Tveito Checking Modal Contracts for Virtually Timed Ambients |
15:30 | Next ICTAC advert, closing remarks |
15:45 | Close |