Overview of the Program for ICTAC 2023
| Monday Dec 04 |
Tuesday Dec 05 |
Wednesday Dec 06 |
Thrusday Dec 07 |
Friday Dec 08 |
|---|---|---|---|---|
| ICTAC 2023 Training School on Applied Formal Methods | ICTAC 2023 Main Conference Program | |||
| ICTAC 2023 Tutorials | ||||
| - | Reception | City Tour | Conference Dinner | - |
Overview of the Social Program
- Reception - Place and time: UTEC terrasse (Jr. Medrano Silva 165, Barranco), Tuesday Dec 05 at 17:45.
- City Tour - Place and time: UTEC (Jr. Medrano Silva 165, Barranco), Wednesday Dec 06, bus will arrive at 15:00 and depart at 15:30. Please be on time! The tour will last 3 hours approx.
- Conference dinner - Place and time: La Rosa Náutica (Espigón Miraflores, Lima 18, Circuito de Playas, Miraflores), Thursday Dec 07 at 19:00 (It is recommended to reach the restaurant by taxi).
For details about the social activities, see below.
Overview of the Training School and Tutorials
| Time | Training School | Tutorials | ||
|---|---|---|---|---|
| Room: A705 | Room: A706 | |||
| Monday Dec 04 | Tuesday Dec 05 | Monday Dec 04 | Tuesday Dec 05 | |
| 08:00 - 09:00 | Registration | |||
| 09:00 - 10:30 | Pedro R. D'Argenio Probabilistic Model Checking Part I |
Marijn J.H. Heule Satisfiability Solving Part I |
Shaukat Ali Mahsa Varshosaz Testing Cyber-Physical Systems Part I |
Einar Broch Johnsen Semantically Lifted Digital Twin |
| 10:30 - 11:00 | Coffee Break | |||
| 11:00 - 12:30 | Pedro R. D'Argenio Probabilistic Model Checking Part II |
Marijn J.H. Heule Satisfiability Solving Part II |
Shaukat Ali Mahsa Varshosaz Testing Cyber-Physical Systems Part II |
Maurice H. ter Beek FM & Tools for Software Product Lines |
| 12:30 - 14:00 | Lunch - UTEC canteen | |||
| 14:00 - 15:30 | Christian Colombo The Theory & Practice of Runtime Verification Part I |
Ana Cavalcanti Ziggy Attala Jim Woodcock Software Engineering for Robotics Part I |
Ina Schaefer Maximilian Kodetzki Correctness-by-Construction Approach to Programming Part I |
Martin Leucker Automata Learning Part I |
| 15:30 - 16:00 | Coffee Break | |||
| 16:00 - 17:30 | Christian Colombo The Theory & Practice of Runtime Verification Part II |
Ana Cavalcanti Ziggy Attala Jim Woodcock Software Engineering for Robotics Part II |
Ina Schaefer Maximilian Kodetzki Correctness-by-Construction Approach to Programming Part II |
Martin Leucker Automata Learning Part II |
| 17:45 - | - | Reception UTEC terrasse |
- | Reception UTEC terrasse |
Overview of the Main Conference
For the detailed program, see here.
| Time | Room: SALA SUM | ||
|---|---|---|---|
| Wednesday Dec 06 | Thursday Dec 07 | Friday Dec 08 | |
| 08:00 - 08:50 | Registration | ||
| 08:50 - 09:00 | Opening | Registration | |
| 09:00 - 10:00 | Invited Speaker: Marijn J.H. Heule Without Loss of Satisfaction |
Invited Speaker: Pedro R. D'Argenio Optimal Route Synthesis in Space DTN using Markov Decision Processes |
Invited Speaker: Ana Cavalcanti Learning in RoboStar |
| 10:00 - 10:30 | Coffee Break | ||
| 10:30 - 12:00 | Security & privacy | Logics & languages | Modeling languages |
| 12:00 - 14:00 | Lunch - UTEC canteen | ||
| 14:00 - 15:00 | Proof complexity | Logics & languages | Verification |
| 15:00 - 15:30 | City Tour. Bus will arrive at 15:00 and depart at 15:30. Please be on time! The tour will last 3 hours approx |
||
| 15:30 - 16:00 | Coffee Break | ||
| 16:00 - 17:30 | Synthesis | Verification | |
| 17:30 - 17:40 | - | Best Paper Award | |
| 19:00 - | Conference dinner La Rosa Náutica |
- | |
Social Activities
City Tour: The bus will depart from UTEC at 15:30. The tour program will present the City of Lima in its three
historical periods: Pre-Hispanic, Colonial and Modern. ANCESTRAL LIMA: The tour begins with a panoramic view of
the “Huaca Pucllana”, a magnificent ceremonial and archaeological center built in the 4th century AD.
COLONIAL LIMA: The tour will visit the Historic Center of Lima, where you will see more than fifty monuments and colonial buildings,
highlighting the Paseo de la República, Plaza San Martín, Plaza Mayor, the Government Palace, the Archbishop’s Palace,
the Cathedral Basilica, the Municipal Palace among others, you will also visit the Convent of San Francisco or the Convent
of Santo Domingo, which highlights its Sevillian cloister, where the oldest university in South America was founded and they
keep the remains of Peruvian saints: Santa Rosa de Lima, San Martín de Porres, San Juan Macías.
CONTEMPORARY LIMA: The tour will visit the most traditional residential areas of Lima, San Isidro,
Miraflores and Larcomar. At the end of the tour, the bus will return to UTEC.
Conference Dinner: It will take place in La Rosa Náutica on the 7th of December at 19:00. La Rosa Náutica is a Peruvian food
restaurant located on a breakwater on the Costa Verde of Lima. The restaurant, with Victorian-style architecture, was founded in 1983
at the initiative of Carlín Semsch on a pier on a rocky breakwater on the Costa Verde Beach Circuit in the Miraflores district. See the map.
Accepted Papers
- Rindo Nakanishi, Yoshiaki Takata and Hiroyuki Seki: A game-theoretic approach to indistinguishability of winning objectives as user privacy
- Florian Dorfhuber, Julia Eisentraut and Jan Kretinsky: Learning Attack Trees by Genetic Algorithms
- Suthee Ruangwises: The Landscape of Computing Symmetric $n$-Variable Functions with $2n$ Cards
- Stepan Kuznetsov: On the complexity of reasoning in Kleene algebras with commutativity conditions
- Matteo Cimini: Towards the Complexity Analysis of Programming Language Proof Methods
- Carlos G. Lopez Pombo, Agustín E. Martínez Suñé and Emilio Tuosto: A Dynamic Temporal Logic for Quality of Service in Choreographic Models
- Jan Tušil, Péter Bereczky and Dániel Horpácsi: Interactive Matching Logic Proofs in Coq
- Tom T.P. Franken, Thomas Neele and Jan Friso Groote: An Autonomous Data Language
- Karla Morris, Thai Son Hoang, Colin Snook and Michael Butler: Formal Language Semantics for Triggered Enable Statecharts with a Run-to-Completion Scheduling
- Beniamino Accattoli, Giulio Guerrieri and Maico Leberle: Strong Call-by-Value and Multi Types
- Weihao Su, Rongchen Li, Chengyao Peng and Haiming Chen: Algorithms for Checking Intersection Non-emptiness of Regular Expressions
- Maurice ter Beek, Rolf Hennicker and José Proença: Realisability of Global Models of Interaction
- Matías Brizzio and César Sánchez: Efficient Reactive Synthesis Using Mode Decomposition
- Leo Lobski, Fabio Zanasi and Ella Gale: A Categorical Approach to Synthetic Chemistry
- Amazigh Amrane, Hugo Bazille, Uli Fahrenberg and Krzysztof Ziemianski: Closure and Decision Properties for Higher-Dimensional Automata
- Francesco Dagnino, Amin Farjudian and Eugenio Moggi: Robustness in Metric Spaces over Continuous Quantales and the Hausdorff-Smyth Monad
- Karam Kharraz, Martin Leucker, Shaun Azzopardi and Gerardo Schneider. Synchronous Agents, Verification, and Blame — A Deontic View
- Uwe Nestmann and Nadine Karsten: Store Locally, Prove Globally
- Erik Voogd, Åsmund Aqissiaq Arild Kløvstad and Einar Broch Johnsen: Denotational Semantics for Symbolic Execution
- Marian Johannes Begemann, Hannes Kallwies, Martin Leucker and Malte Schmitz: TOOL PAPER: Tessla-ROS-Bridge - Runtime Verification of Robotic Systems
- Anna Stramaglia, Jeroen J.A. Keiren and Thomas Neele: Simplifying process parameters by unfolding algebraic data types
- Ida Sandberg Motzfeldt, Ingrid Chieh Yu, Crystal Chang Din, Violet Ka I Pun and Volker Stolz: Modular Soundness Checking of Feature Model Evolution Plans