Overview

This is a three-day workshop celebrating Ahmed Bouajjani. He has been awarded an honorary doctorate, doctor honoris causa, at Uppsala University to appreciate his contribution to the scientific community in general and Uppsala University in particular.

Venue

Room 90103
Ångströmlaboratoriet
Lägerhyddsvägen 1, hus 9
Uppsala

Mazemap: https://link.mazemap.com/mcsaQ187

Zoom link: https://uu-se.zoom.us/j/68543245707

Program

Monday

• 08:50–09:00 Opening
• 09:00–09:40 Ahmed Bouajjani
  • TBD
• 09:40–10:20 Javier Esparza
  • Interactive proofs and BDDs
• 10:20–10:50 Coffee Break
• 10:50–11:30 Radu Iosif
  • Reasoning about Distributed Reconfigurable Systems
• 11:30–12:10 Wang Yi
  • MIMOS: from theory to tools for embedded software design & update
• 12:10–13:40 Lunch
  • Restaurant Rullan
• 13:40–14:20 Constantin Enea
  • Using Concurrent Objects in Randomized Programs
• 14:20–15:00 Shaz Qadeer (moved to 15:30)
  • Reasoning with permissions using linear types and first-order logic
• 15:00–15:30 Coffee Break
• 15:30–16:10 Roland Meyer (cancelled)
  • A Concurrent Program Logic with a Future and History
• 16:10–16:50 Markus Müller-Olm (moved to 14:20)
  • Logics for Asynchronous Hyperproperties

Tuesday

• 09:00–09:40 Kostis Sagonas
  • Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens
• 09:40–10:20 Rupak Majumdar
  • Recent Results in Context-Bounded Exploration
• 10:20–10:50 Coffee Break
• 10:50–11:30 Tayssir Touili
  • On static malware detection
• 11:30–12:10 Ahmed Rezine
  • Reachability in phaser programs
• 12:10–13:40 Lunch
  • Restaurant Rullan
• 13:40–14:20 Tomás Vojnar
  • Low-Level Bi-Abduction
• 14:20–15:00 Faouzi Atig and Lukás Holík
  • Flattening String Constraints
• 15:00–15:30 Coffee Break
• 15:30–16:10 Eugene Asarin
  • Timed pattern-matching
• 16:10–16:50 Lukás Holík (cancelled)
  • Counting in Regexes Considered Harmful: Exposing ReDoS Vulnerability of Nonbacktracking Matchers
• 16:50–17:10 Anthony W. Lin (moved to 16:10)
  • Liveness over Randomized Parameterized Systems
• 19:00 Workshop Dinner at the Peppar Peppar Restaurant

Wednesday

• 09:00–09:40 Jean-François Raskin
  • LTL Synthesis with a Few Hints
• 09:40–10:20 Cezara Drăgoi
  • Reasoning about State Machine Replication
• 10:20–10:50 Coffee Break
• 10:50–11:30 Paul Fiterau-Brostean
  • Automata-Based Automated Detection of State Machine Bugs in Protocol Implementations
• 11:30–12:10 Bengt Jonsson
  • Model Learning for Automata Models with Data
• 12:10–14:00 Lunch
  • Restaurant Rullan