---

ICTAC Conference | ICTAC 2021 | News | Important Dates | Overview and Scope | Call for Papers | Registration | Programme | Keynote Speakers | Committees | ICTAC School 2021

---

ICTAC 2021

18th International Colloquium on Theoretical Aspects of Computing

VIRTUAL EVENT organied by Nazarbayev University, Nur-Sultan, Kazakhstan, September 8-10, 2021

PROGRAMME

---

Session Schedule by Time Zone | Detailed Programme | List of accepted papers

---

SESSION SCHEDULE BY TIME ZONE

This table shows the starting time of each session by time zone. Click on the day or the session name to see the session detailed information.

Time zones:

• GMT-7:00 - US/Canada Pacific Time (Vancouver, Seattle, Los Angeles, San Francisco, Las Vegas)
• GMT-6:00 - Central America, US/Canada Mountain Time (Edmonton, Salt Lake City, Denver, Phoenix, El Paso)
• GMT-5:00 - Bogota, Lima, Mexico City, Quito, Rio Branco, US/Canada Central Time (Winnipeg, Chicago, Dallas, Houston)
• GMT-4:00 - Caracas, Cuba, La Paz, Santiago, US/Canada Eastern Time (Toronto, Detroit, Boston, New York, Washington DC, Atlanta, Miami)
• GMT-3:00 - Brasilia, Buenos Aires, Montevideo
• GMT: - Azores, Monrovia, Reykjavik
• GMT+1:00 - West Central Africa, WEST (Dublin, Lisbon, London)
• GMT+2:00 - Pretoria, CEST (Amsterdam, Berlin, Bern, Brussels, Budapest, Madrid, Oslo, Paris, Praga, Rome, Sofia, Stockholm, Vienn, Warsaw)
• GMT+3:00 - Nairobi, Beirut, Jerusalem, EEST (Athens, Bucharest, Helsinki, Kiev, Sofia), FET (Minsk, Moscow, St. Petersburg)
• GMT+4:00 - Abu Dhabi, Muscat, Yerevan
• GMT+4:30 - Kabul, Tehran
• GMT+5:00 - Ekaterinburg, Tashkent, West Kazakhstan (Aqtobe, Atyrau, Oral)
• GMT+5:30 - Kolkata, Mumbai, New Delhi
• GMT+6:00 - Dhaka, East Kazakhstan (Almaty, Karagandy, Nur-Sultan, Taraz)
• GMT+7:00 - Bangkok, Hanoi, Jakarta, Novosibirsk
• GMT+8:00 - Beijing, Hong Kong, Macau, Irkutsk, Perth, Ulan Batur
• GMT+9:00 - Seoul, Tokyo, Yakutsk
• GMT+9:30 - Adelaide, Darwin
• GMT+10:00 - Brisbane, Hobart, Melbourne, Sydney, Vladivostok
• GMT+12:00 - Auckland, Fiji, Wellington

DETAILED PROGRAMME

Wednesday, 8 September 2021

WED 13:15-13:30 GMT+6- OPENING

The indicated times refer to East Kazakhstan time zone. See the SESSION SCHEDULE for other time zones

Session Video Recoding

WED 13:30-14:30 GMT+6 - Session 1 (Keynote Speaker): Kim Larsen (Chair: Peter Csaba Ölveczky)

The indicated times refer to East Kazakhstan time zone. See the SESSION SCHEDULE for other time zones

Model Checking and Machine Learning Joining Forces

Session Video Recoding | Abstract and Speaker's Biography

WED 14:30-15:00 GMT+6 - SHORT BREAK

WED 15:00-16:30 GMT+6 - Session 2: Efficient Model Checking Methods Chair: Martin Leucker)

The indicated times refer to East Kazakhstan time zone. See the SESSION SCHEDULE for other time zones

Session Video Recoding

• A divide & conquer approach to conditional stable model checking
  Yati Phyo, Canh Do Minh and Kazuhiro Ogata


• Accelerating SpMV Multiplication in Probabilistic Model Checkers using GPUs
  Muhammad Hannan Khan, Osman Hasan and Shahid Khan


• A Set Automaton to Locate All Pattern Matches in a Term
  Rick Erkens and Jan Friso Groote

WED 16:30-17:30 GMT+6 - LONG BREAK

WED 17:30-18:30 GMT+6 - Session 3: Database and Distributed Transactions (Chair: Marcello Bonsangue)

The indicated times refer to East Kazakhstan time zone. See the SESSION SCHEDULE for other time zones

Session Video Recoding

• Some Aspects of the Database Resilience
  Luis Bustamante and Ana Teresa Martins


• On the Correctness Problem for Serializability
  Jürgen König and Heike Wehrheim

WED 18:30-19:00 GMT+6 - SHORT BREAK

WED 19:00-20:30 GMT+6 - Session 4: Formalization and Verification in Coq and Isabelle (Chair: Sanjiva Prasad)

The indicated times refer to East Kazakhstan time zone. See the SESSION SCHEDULE for other time zones

Session Video Recoding

• Certifying Choreography Compilation
  Luís Cruz-Filipe, Fabrizio Montesi and Marco Peressotti


• A Mechanically Verified Theory of Contracts
  Stéphane Kastenbaum, Benoît Boyer and Jean-Pierre Talpin


• A Complete Semantics of K and Its Translation to Isabelle
  Liyi Li and Elsa Gunter

Thursday, 9 September 2021

THU 13:30-14:30 GMT+6 - Session 5 (Keynote Speaker): Wil van der Aalst (Chair: Antonio Cerone)

The indicated times refer to East Kazakhstan time zone. See the SESSION SCHEDULE for other time zones

Concurrency and Objects Matter: Disentangling the Fabric of Real Operational Processes

Session Video Recoding | Presentation Slides | Abstract and Speaker's Biography

THU 14:30-15:00 GMT+6 - SHORT BREAK

THU 15:00-16:30 GMT+6 - Session 6: Security and Privacy (Chair: Étienne André)

The indicated times refer to East Kazakhstan time zone. See the SESSION SCHEDULE for other time zones

Session Video Recoding

• Card-based Cryptographic Protocols with a Standard Deck of Cards Using Private Operations
  Yoshifumi Manabe and Hibiki Ono


• Compositional Analysis of Protocol Equivalence in the Applied pi-calculus using Quasi-Open Bisimilarity
  Ross Horne, Sjouke Mauw and Semen Yurkov


• Assessing Security of Crypto-Currencies with Attack-Defense Trees: Proof of Concept and Future Directions
  Julia Eisentraut, Stephan Holzer, Katharina Klioba, Jan Kretinsky, Lukas Pin and Alexander Wagner

THU 16:30-17:30 GMT+6 - LONG BREAK

THU 17:30-18:30 GMT+6 - Session 7: Security and Privacy (Chair: Frédéric Mallet)

The indicated times refer to East Kazakhstan time zone. See the SESSION SCHEDULE for other time zones

Session Video Recoding

• An Incentive Mechanism for Trading Personal Data in Data Market)
  Sayan Biswas, Kangsoo Jung and Catuscia Palamidessi


• Normalising Lustre Preserves Security
  Sanjiva Prasad and Rathnakar Madhukar Yerraguntla

THU 18:30-19:00 GMT+6 - SHORT BREAK

THU 19:00-20:00 GMT+6 - Session 8 (Keynote Speaker): Grigore Rosu (Chair: Peter Csaba Ölveczky

The indicated times refer to East Kazakhstan time zone. See the SESSION SCHEDULE for other time zones

Formal Design, Implementation and Verification of Blockchain Languages

Session Video Recoding | Presentation Slides | Abstract and Speaker's Biography

Friday, 10 September 2021

FRI 13:30-14:30 GMT+6 - Session 9 (Keynote Speaker): Alan Dix (Chair: Antonio Cerone)

The indicated times refer to East Kazakhstan time zone. See the SESSION SCHEDULE for other time zones

Qualitative–Quantitative Reasoning: thinking informally about formal things

Session Video Recoding | Presentation Slides | Abstract and Speaker's Biography

FRI 14:30-15:00 GMT+6 - SHORT BREAK

FRI 15:00-16:30 GMT+6 - Session 10: Synthesis and Learning (Chair: Kazuhiro Ogata)

The indicated times refer to East Kazakhstan time zone. See the SESSION SCHEDULE for other time zones

Session Video Recoding

• Reactive Synthesis from Visibly Register Pushdown Automata
  Ryoma Senda, Yoshiaki Takata and Hiroyuki Seki


• AlCons: Deductive Synthesis of Sorting Algorithms in Theorema
  Isabela Dramnesc and Tudor Jebelean


• Learning Probabilistic Automata using Residuals
  Wenjing Chu, Shuo Chen and Marcello Bonsangue

FRI 16:30-17:30 GMT+6 - LONG BREAK

FRI 17:30-19:00 GMT+6 - Session 11: Systems Calculi and Analysis (Chair: Catuscia Palamidessi)

The indicated times refer to East Kazakhstan time zone. See the SESSION SCHEDULE for other time zones

Session Video Recoding

• A Proof Method for Local Sufficient Completeness of Term Rewriting Systems
  Tomoki Shiraishi, Kentaro Kikuchi and Takahito Aoto


• A Calculus for Attribute-based Memory Updates
  Michele Pasqua and Marino Miculan


• ComplexityParser: an automatic tool for certifying poly-time complexity of Java programs
  Emmanuel Hainry, Emmanuel Jeandel, Romain Péchoux and Olivier Zeyen

FRI 19:00-19:30 GMT+6 - Session 12: Quantum Computing (Chair: Martin Lukac)

The indicated times refer to East Kazakhstan time zone. See the SESSION SCHEDULE for other time zones

Session Video Recoding

• A New Connective in Natural Deduction, and its Application to Quantum Computing
  Alejandro Díaz-Caro and Gilles Dowek

FRI 19:30-19:45 GMT+6 - CLOSING

Session Video Recoding

• Best Paper Award shared by:
  • Accelerating SpMV Multiplication in Probabilistic Model Checkers using GPUs
    Muhammad Hannan Khan, Osman Hasan and Shahid Khan
    BPA certificate and 500 € Springer Prize.
  • A New Connective in Natural Deduction, and its Application to Quantum Computing
    Alejandro Díaz-Caro and Gilles Dowek
    BPA certificate and 500 € Springer Prize.
• Announcement about ICTAC 2022: See you next year in Tblisi, Georgia

LIST OF ACCEPTED PAPERS

• Card-based Cryptographic Protocols with a Standard Deck of Cards Using Private Operations
  Yoshifumi Manabe and Hibiki Ono
  [presentation schedule]
   
• Learning Probabilistic Automata using Residuals
  Wenjing Chu, Shuo Chen and Marcello Bonsangue
  [presentation schedule]
   
• ComplexityParser: an automatic tool for certifying poly-time complexity of Java programs
  Emmanuel Hainry, Emmanuel Jeandel, Romain Péchoux and Olivier Zeyen
  [presentation schedule]
   
• On the Correctness Problem for Serializability
  Jürgen König and Heike Wehrheim
  [presentation schedule]
   
• A Complete Semantics of K and Its Translation to Isabelle
  Liyi Li and Elsa Gunter
  [presentation schedule]
   
• Assessing Security of Crypto-Currencies with Attack-Defense Trees: Proof of Concept and Future Directions
  Julia Eisentraut, Stephan Holzer, Katharina Klioba, Jan Kretinsky, Lukas Pin and Alexander Wagner
  [presentation schedule]
   
• A divide & conquer approach to conditional stable model checking
  Yati Phyo, Canh Do Minh and Kazuhiro Ogata
  [presentation schedule]
   
• A Set Automaton to Locate All Pattern Matches in a Term
  Rick Erkens and Jan Friso Groote
  [presentation schedule]
   
• Normalising Lustre Preserves Security
  Sanjiva Prasad and Rathnakar Madhukar Yerraguntla
  [presentation schedule]
   
• Certifying Choreography Compilation
  Luís Cruz-Filipe, Fabrizio Montesi and Marco Peressotti
  [presentation schedule]
   
• A New Connective in Natural Deduction, and its Application to Quantum Computing
  Alejandro Díaz-Caro and Gilles Dowek
  [presentation schedule]
   
• Accelerating SpMV Multiplication in Probabilistic Model Checkers using GPUs
  Muhammad Hannan Khan, Osman Hasan and Shahid Khan
  [presentation schedule]
   
• AlCons: Deductive Synthesis of Sorting Algorithms in Theorema
  Isabela Dramnesc and Tudor Jebelean
  [presentation schedule]
   
• A Mechanically Verified Theory of Contracts
  Stéphane Kastenbaum, Benoît Boyer and Jean-Pierre Talpin
  [presentation schedule]
   
• A Calculus for Attribute-based Memory Updates
  Michele Pasqua and Marino Miculan
  [presentation schedule]
   
• Some Aspects of the Database Resilience
  Luis Bustamante and Ana Teresa Martins
  [presentation schedule]
   
• A Proof Method for Local Sufficient Completeness of Term Rewriting Systems
  Tomoki Shiraishi, Kentaro Kikuchi and Takahito Aoto
  [presentation schedule]
   
• Reactive Synthesis from Visibly Register Pushdown Automata
  Ryoma Senda, Yoshiaki Takata and Hiroyuki Seki
  [presentation schedule]
   
• Compositional Analysis of Protocol Equivalence in the Applied pi-calculus using Quasi-Open Bisimilarity
  Ross Horne, Sjouke Mauw and Semen Yurkov
  [presentation schedule]
   
• An Incentive Mechanism for Trading Personal Data in Data Market
  Sayan Biswas, Kangsoo Jung and Catuscia Palamidessi
  [presentation schedule]