ICTAC 2022

19th International Colloquium on Theoretical Aspects of Computing

September 27-30, 2022, Tbilisi, Georgia

Program

Tuesday, September 27th

09:00-10:00: Volker Diekert and Manfred Kufleitner. Reachability Games and Parity Games
10:00-10:30: Tomoyuki Yamakami. Formal Grammars for Turn-Bounded Deterministic Context-Free Languages
10:30-11:00: Coffee break
11:00-11:30: Eva Graversen, Fabrizio Montesi, Luis Cruz-Filipe, Lovro Lugovic and Marco Peressotti. Functional Choreographic Programming
11:30-12:00: Niels Voorneveld. Runners for Interleaving Algebraic Effects
12:00-12:30: Ningning Chen and Huibiao Zhu. Denotational and Algebraic Semantics for the CaIT calculus
12:30-14:00: Lunch
14:00-15:00: Miaomiao Zhang, Wanwei Liu, Xiaochen Tang, Bowen Du and Zhiming Liu. Human-Cyber-Physical Automata and Their Synthesis
15:00-15:30: Tajana Ban Kirigin, Musab A. Alturki, Max Kanovich, Vivek Nigam, Andre Scedrov and Carolyn Talcott. On the Formalization and Computational Complexity of Resilience Problems for Cyber-Physical Systems
15:30-16:00: Coffee break
16:00-16:30: Christopher Bischopink and Ernst-Ruediger Olderog. Spatial and Timing Properties in Highway Traffic
16:30-17:00: Zhen Huang, Bo Li, Dehui Du and Qin Li. A Model Checking Based Approach to Detect Safety-Critical Adversarial Examples on Autonomous Driving Systems
17:00-17:30: Raul Pardo, Einar Broch Johnsen, Ina Schaefer and Andrzej Wasowski. A Specification Logic for Programs in the Probabilistic Guarded Command Language
17:30-17:45: Nicolas Nalpon, Cyril Allignol and Celia Picard. Toward a user interface description language based on bigraphs

Wednesday, September 28th

09:00-10:00: David Basin, Thibault Dardinier, Nico Hauser, Lukas Heimes, Jonathan Julian Huerta y Munive, Nicolas Kaletsch, Srdjan Krstic, Emanuele Marsicano, Martin Raszyk, Joshua Schneider, Dawit Legesse Tirore, Dmitriy Traytel and Sheila Zingg. VeriMon: A Formally Verified Monitoring Tool
10:00-10:30: Niels Muendler and Tobias Nipkow. A Verified Implementation of B+-trees in Isabelle/HOL

Thursday, September 29th

09:00-10:00: Marsha Chechik. On Safety, Assurance and Reliability: A Software Engineering Perspective
10:00-10:30: Yehia Abd Alrahman, Mauricio Martel and Nir Piterman. A PO Characterisation of Reconfiguration
10:30-11:00: Coffee break
11:00-11:30: Pedro Angelo and Mario Florido. Type Inference for Rank-2 Intersection Types using Set Unification
11:30-12:00: Sandra Alves and Mario Florido. Structural Rules and Algebraic Properties of Intersection Types
12:00-12:30: Sandra Alves and Daniel Ventura. Quantitative Weak Linearisation
12:30-14:00: Lunch
14:00-14:30: Hai Lin and Christopher Lynch. Local XOR Unification: Definitions, Algorithms and Application to Cryptography
14:30-15:00: Matthieu Dien, Antoine Genitrini and Frederic Peschanski. A Combinatorial Study of Async/Await Processes
15:00-15:30: Luis Cruz-Filipe, Graca Gaspar and Isabel Nunes. Reconciling communication delays and negation
15:30-16:00: Coffee break
16:00-16:30: Ziyuan Gao, Sanjay Jain, Zeyong Li, Ammar Fathin Sabili and Frank Stephan. Alternating Automatic Register Machines
16:30-17:00: Hayato Shikata, Kodai Toyoda, Daiki Miyahara and Takaaki Mizuki. Card-minimal Protocols for Symmetric Boolean Functions of More Than Seven Inputs
17:00-17:15: Denis Firsov, Ekaterina Zhuchko and Sven Laur. Unsatisfiability of Comparison-Based Non-Malleability for Commitments
17:15-17:45: Dylan McDermott, Yasuaki Morita and Tarmo Uustalu. A Type System with Subtyping for WebAssembly's Stack Polymorphism

Friday, September 30th

09:00-10:00: Bernhard Beckert, Mattias Ulbrich, Birgit Vogel-Heuser and Alexander Weigl. Generalized Test Tables: A Domain-specific Specification Language for Automated Production
10:00-10:30: Alexandru-Ioan Lungu and Dorel Lucanu. A Matching Logic Foundation for Alk
10:30-11:00: Coffee break
11:00-11:30: Rindo Nakanishi, Yoshiaki Takata and Hiroyuki Seki. Active Learning for Deterministic Bottom-up Nominal Tree Automata
11:30-12:00: Xiyue Zhang, Xiaohong Chen and Meng Sun. Towards a Unifying Logical Framework for Neural Networks
12:00-12:30: Kentaro Kikuchi. Ground Confluence and Strong Commutation modulo Alpha-Equivalence in Nominal Rewriting

Accepted Papers

Eva Graversen, Fabrizio Montesi, Luis Cruz-Filipe, Lovro Lugovic and Marco Peressotti. Functional Choreographic Programming
Tajana Ban Kirigin, Musab A. Alturki, Max Kanovich, Vivek Nigam, Andre Scedrov and Carolyn Talcott. On the Formalization and Computational Complexity of Resilience Problems for Cyber-Physical Systems
Xiyue Zhang, Xiaohong Chen and Meng Sun. Towards a Unifying Logical Framework for Neural Networks
Christopher Bischopink and Ernst-Rudiger Olderog. Spatial and Timing Properties in Highway Traffic
Rindo Nakanishi, Yoshiaki Takata and Hiroyuki Seki. Active Learning for Deterministic Bottom-up Nominal Tree Automata
Ziyuan Gao, Sanjay Jain, Zeyong Li, Ammar Fathin Sabili and Frank Stephan. Alternating Automatic Register Machines
Hayato Shikata, Kodai Toyoda, Daiki Miyahara and Takaaki Mizuki. Card-minimal Protocols for Symmetric Boolean Functions of More Than Seven Inputs
Dylan McDermott, Yasuaki Morita and Tarmo Uustalu. A Type System with Subtyping for WebAssembly's Stack Polymorphism
Pedro Angelo and Mario Florido. Type Inference for Rank-2 Intersection Types using Set Unification
Sandra Alves and Daniel Ventura. Quantitative Weak Linearisation
Hai Lin and Christopher Lynch. Local XOR Unification: Definitions, Algorithms and Application to Cryptography
Kentaro Kikuchi. Ground Confluence and Strong Commutation modulo Alpha-Equivalence in Nominal Rewriting
Niels Mundler and Tobias Nipkow. A Verified Implementation of B+-trees in Isabelle/HOL
Alexandru-Ioan Lungu and Dorel Lucanu. A Matching Logic Foundation for Alk
Nicolas Nalpon, Cyril Allignol and Celia Picard. Toward a user interface description language based on bigraphs
Zhen Huang, Bo Li, Dehui Du and Qin Li. A Model Checking Based Approach to Detect Safety-Critical Adversarial Examples on Autonomous Driving Systems
Luis Cruz-Filipe, Graca Gaspar and Isabel Nunes. Reconciling communication delays and negation
Denis Firsov, Ekaterina Zhuchko and Sven Laur. Unsatisfiability of Comparison-Based Non-Malleability for Commitments
Matthieu Dien, Antoine Genitrini and Frederic Peschanski. A Combinatorial Study of Async/Await Processes
Sandra Alves and Mario Florido. Structural Rules and Algebraic Properties of Intersection Types
Ningning Chen and Huibiao Zhu. Denotational and Algebraic Semantics for the CaIT calculus
Yehia Abd Alrahman, Mauricio Martel and Nir Piterman. A PO Characterisation of Reconfiguration
Raul Pardo, Einar Broch Johnsen, Ina Schaefer and Andrzej Wasowski. A Specification Logic for Programs in the Probabilistic Guarded Command Language
Niels Voorneveld. Runners for Interleaving Algebraic Effects
Tomoyuki Yamakami. Formal Grammars for Turn-Bounded Deterministic Context-Free Languages