CARI/ICTAC School, ICTAC Conference Program

All of the school/conference events take place at STIAS (Stellenbosch Institute for Advanced Study, 10 Marais Road).

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

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

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

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

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

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

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

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