Ichiro Hasuo

• National Institute of Informatics
• ichiro [at] is.s.u-tokyo.ac.jp

• English
• Japanese
• Dutch
• Chinese

• Home
• Contact
• Research
• Cv
• Papers
• Talks
• Teaching
• Group

For talks in Japanese, see also here.

2024

• Proving Safety of Automated Driving Vehicles.
  ICTAC 2024 Keynote Talk, Bangkok, Thailand.
  27 November 2024. Slides: [pdf]
• Abstract and Concrete Model Checking.
  ICTAC 2024 Invited Tutorial, Bangkok, Thailand.
  25 November 2024. Lecture notes: [pdf] Boards: [folder]
• Logical Manifestation of Specifications, Requirements and Responsibilities: Approaches from Software Science. JSAE Annual Congress (Spring), invited talk, Yokohama, Japan.
  24 May 2024. Slides: [pdf]
• Compositional Probabilistic Model Checking with String Diagrams of MDPs.
  Shonan Meeting 175 (New Directions and Challenges in Interactive Semantics), Hayama, Japan.
  20 May 2024. Slides: [pdf]
• Explicit Hopcroft’s Trick in Categorical Partition Refinement.
  CMCS 2024, Luxembourg.
  7 April 2024. Slides: [pdf]

2023

• Formal Verification of Intersection Safety for Automated Driving.
  ITSC 2023, Bilbao, Spain.
  25 September 2023. Slides: [pdf]
• Proving Safety of Automated Driving Vehicles: Formalization of RSS with Program Logic.
  Invited talk at The 3rd Workshop on Safety Testing and Validation of Connected and Automated Vehicles with ITSC 2023, Bilbao, Spain.
  24 September 2023. Slides: [pdf]
• Proving Safety of Automated Driving Vehicles.
  Invited talk at Forum "Math for Industry" 2023, Kyushu University, Fukuoka, Japan.
  29 Aug 2023. Slides: [pdf]
• Compositionality in Probabilistic Verification, Statistical Inference, and Stochastic Optimization.
  VeriProP 2023 workshop, Maison de la Chimie, Paris, France.
  17 July 2023. Slides: [pdf]
• Logic-Guided Optimization Metaheuristics in Hybrid System Falsification and Parameter Tuning.
  A seminar talk at OASIS: The Oxford Advanced Seminar on Informatic Structures, University of Oxford.
  21 June 2023. Slides: [pdf]
• Proving Safety of Automated Driving Vehicles.
  A seminar talk at OASIS: The Oxford Advanced Seminar on Informatic Structures, University of Oxford.
  20 June 2023. Slides: [pdf]
• Compositional Probabilistic Model Checking with String Diagrams of MDPs.
  A seminar talk at OASIS: The Oxford Advanced Seminar on Informatic Structures, University of Oxford.
  19 June 2023. Slides: [pdf]
• Proving Safety of Automated Driving Vehicles.
  A seminar talk at ITU Copenhagen (remote).
  16 May 2023. Slides: [pdf]
• Proving Safety of Automated Driving Vehicles.
  IFIP WG 1.3 Meeting, Paris, France.
  25 April 2023.

2022

• Blackbox Analysis of Automotive Systems by Logic and Optimization Software Science Approaches to Efficiency and Deployability.
  2022 JSAE Annual Congress (Spring), Pacifico Yokohama Conference Center, Yokohama, Japan.
  27 May 2022. Slides: [pdf]
• Goal-Aware RSS for Complex Scenarios via Program Logic.
  FoMLAS 2022, Technion, Haifa, Israel.
  31 July 2022. Slides: [pdf]
• Bisimulation Games Played in Fibered Categories.
  VardiFest: A workshop in honor of Moshe Y. Vardi, Technion, Haifa, Israel.
  1 August 2022. Slides: [pdf]
• Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games. VeriProP 2022 workshop, Technion, Haifa, Israel.
  12 August 2022. Slides: [pdf]

2021

• Software Science under Uncertainties: A Survey. (In Japanese)
  PPL Workshop (category 4, online).
  11 March 2021. Slides: [pdf]
• Think Abstractly, Work Concretely.
  Programming Languages Mentoring Workshop (PLMW) @ POPL 2021 (online).
  18 January 2021. Slides: [pdf]

2020

• Quantum Programming Languages: from Static Analysis to Quantum IDE.
  IPSJ Seminar (online).
  14 December 2020. Slides (mostly in English): [pdf]
• Codensity Lifting: a Unified Framework for Observations in Process Theory.
  IFIP WG 1.3 Meeting, Massa Marittima, Italy.
  14 January 2020. Slides: [pdf]

2019

• Safety under 
Statistical and Environmental Uncertainties: Challenges in Cyber-Physical Systems with 
Machine-Learning Components.
  MLSE International Symposium​ 2019​ , Tokyo, Japan.
  18 October 2019. Slides: [pdf]
• Formal Methods for Cyber-Physical Systems, at Work.
  1st PKU-UTokyo-NII Joint Forum on Information Science, Beijing, China.
  24 September 2019. Slides: [pdf]
• The Power of Abstraction, in a Theory, a Project, and an Inspiring Mind.
  Symposium on the Categorical Unity of the Sciences
  (on the occasion of Samson Abramsky's visit), Kyoto, Japan.
  22 March 2019. Slides: [pdf]
  Supplementary slides: [pdf] (Problem with Acrobat, OK with Preview or Skim)

2018

• Quality Assurance of Cyber-Physical Systems: Mathematical Metatheory, Machine Learning and Automated Driving.
  Informatics Research Winter Festa Episode 4, Tokyo, Japan.
  26 December 2018. Slides: [pdf]
• Bounding Errors Due to Switching Delays in Incrementally Stable Switched Systems.
  ADHS 2018 (IFAC Conference on Analysis and Design of Hybrid Systems), Oxford, UK.
  12 July 2018. Slides: [pdf]
• Martingale-Based Methods for Reachability Probabilities: Excitements and Afterthoughts in Coalgebras.
  Coalgebra, Now @ FLoC 2018 Workshop, Oxford, UK.
  8 July 2018. Slides: [pdf]
• Coalgebras and Higher-Order Computation: a GoI Approach.
  Game Semantics 25 Workshop, Oxford, UK.
  8 July 2018. Slides: [pdf]
• Efficient Online Timed Pattern Matching by Automata-Based Skipping.
  (Based on [Waga, Hasuo & Suenaga, FORMATS'17])
  IFIP WG 1.3 Meeting, Royal Holloway, UK.
  6 July 2018. Slides: [pdf]
• Approximating Reachability Probabilities by (Super-)Martingales.
  SynCoP 2018, Thessaloniki, Greece.
  15 April 2018. Slides: [pdf]

2017

• Nonstandard Static Analysis: Literal Transfer of Deductive Verification Frameworks from Discrete to Hybrid.
  Keynote address at CyPhy 2017, Seoul, South Korea.
  19 October 2017. Slides: [pdf]
• Efficient Online Timed Pattern Matching by Automata-Based Skipping.
  FORMATS 2017, Berlin, Germany.
  6 September 2017. Slides: [keynote | pdf]
• Least and Alternating Fixed-Point Specifications in Coalgebraic System Modeling.
  IFIP WG 1.3 Meeting, Berlin, Germany.
  4 September 2017. Slides: [pdf]

2016

• Coalgebras and Higher-Order Computation: a GoI Approach.
  FSCD 2016 (invited talk), Porto, Portugal.
  27 June 2016. Slides: [keynote (5.3)|pdf]
• Lattice-Theoretic Progress Measures and Coalgebraic Model Checking.
  POPL 2016, St. Petersburg, FL.
  22 Jan 2016. Slides: [pdf]

2015

• ``Nonstandard Static Analysis'' of Cyber-Physical Systems (in Japanese).
  Mathematics and Data Science Seminar, Osaka University, Japan.
  12 Jun 2015. Slides: [pdf]

2014

• Generic Weakest Precondition Semantics from Monads Enriched with Order
  (or: Towards Coalgebraic Model Checking).
  CMCS 2014 (invited talk), Grenoble, France.
  6 Apr 2014. Slides: [keynote | pdf]

2013

• ``Nonstandard Static Analysis'' of Cyber-Physical Systems (in Japanese).
  Mathematical Society of Japan Autumn Meeting, Ehime University, Matsuyama, Japan.
  27 Sep 2013. Slides: [keynote | pdf | pdf (4up, no animation, for printout)]
• Coinductive Predicates and Final Sequences in a Fibration.
  MFPS XXIX, Tulane University, New Orleans LA, USA.
  24 June 2013. Slides: [keynote | pdf]
• Semantics of Higher-Order Quantum Computation via Geometry of Interaction.
  
  • PPS Seminar, Univ. Paris VII. January 2013. (Slides below)
  • GaLoP VIII (invited talk), Queen Mary Univ. London. 19 July 2013. Slides: [keynote | pdf]
• Hyperstream Processing Systems: Nonstandard Modeling of Continuous-Time Signals..
  POPL 2013, Rome, Italy.
  25 January 2013. Slides: [keynote | pdf]

2012

• Exercises in Nonstandard Static Analysis of Hybrid Systems.
  CAV 2012, Berkeley CA, USA.
  July 2012. Slides: [keynote | pdf]
• Trace Everywhere, or Coalgebraic Trace Semantics for Higher-Order Computation, Especially The Quantum One.
  Dagstuhl Seminar on Coalgebraic Logics, Germany.
  October 2012. Slides: [keynote | pdf]

2011

• Programming with Infinitesimals: A While-Language for Hybrid System Modeling.
  ICIS Colloquium, Radboud University Nijmegen, the Netherlands.
  Nov 2011. Slides (some by Kohei Suenaga): [keynote | pdf]
• Semantics of Higher-Order Quantum Computation via Geometry of Interaction.
  • (For theoretical computer scientists and logicians, 2 hrs)
    Plume Team Seminar, LIP, ENS Lyon, France.
    September 2011. Slides: [keynote | pdf | pdf (4up, no animation, for printout)]
  • (For logic-oriented quantum theorists, 1 hour)
    QPL 2011, Nijmegen, the Netherlands.
    October 2011. Slides: [keynote | pdf | pdf (4up, no animation, for printout)]
  • (For the general quantum computation & information crowd, 30 min.)
    QIT 24, Tokyo Institute of Technology, Tokyo, Japan.
    May 2011. Slides: [keynote | pdf]
• The Microcosm Principle and Compositionality of GSOS-Based Component Calculi.
  CALCO 2011, Winchester, UK.
  September 2011. Slides: [keynote | pdf]

2010

• Generic Forward and Backward Simulations II: Probabilistic Simulation.
  CONCUR 2010, Paris, France.
  September 2010. Slides: [keynote | pdf]
• Theory of Coalgebra: Towards Mathematics of Systems.
  A gentle introduction to the theory of coalgebra, targeted at CS master students.
  Colloquium, Dept. of Computer Science, Univ. of Tokyo.
  June 2010. Slides: [keynote | pdf]
• Coalgebraic Representation Theory of Fractals.
  MFPS XXVI, Ottawa, Canada.
  May 2010. Slides: [keynote | pdf]

2009

• Coalgebraic Components in a Many-Sorted Microcosm.
  CALCO 2009, Udine, Italy.
  September 2009. Slides: [pptx | ppt | pdf]

2008

• The Microcosm Principle and Concurrency in Coalgebra.
  FoSSaCS 2008, Budapest, Hungary.
  March 2008. Slides: [pptx | ppt | pdf]
• Tracing Anonymity with Coalgebras.
  PhD defense, Radboud University Nijmegen, the Netherlands.
  10 March 2008. Slides: [pptx | ppt | pdf]

2007

• The Microcosm Principle and Concurrency in Coalgebras.
  CALCO-jnr workshop, Bergen, Norway.
  August 2007. Slides: [ppt | pdf]
• Probablisitic Anonymity via Coalgebraic Simulations.
  
  • Comete-Parsifal Seminar, Ecole Polytechnique, France. March 2007.
  • ESOP '07, Braga (beautiful city!), Portugal. March 2007.
  Slides: [ppt | pdf]

2006

• Generic Forward and Backward Simulations.
  CONCUR 2006, University of Bonn, Germany.
  August 2006. Slides: [ppt | pdf]
• Freyd is Kleisli, for Arrows.
  MSFP '06, Kuressaare, Estonia.
  July 2006. Slides: [pdf]
• Coalgebras in Kleisli Categories: Generic Theory for Traces and Simulations.
  Modal Logic, Stone Duality and Coalgebras workshop,
  University of Leicester, UK.
  June 2006. Slides: [pdf]
• Trace Semantics for Coalgebras: a Generic Theory.
  ACG Colloquium, CWI, Amsterdam, the Netherlands.
  January 2006. Slides: [pdf]

2005

• Context-free Languages via Coalgebraic Trace Semantics, and also
  Coalgebraic Trace Semantics for Probabilistic Systems.
  CALCO 2005, University of Wales Swansea, UK.
  September 2005. Slides: [pdf]
• Introduction to Coalgebraic Trace Semantics. (Sneak preview of the talk above)
  CALCO-jnr workshop, University of Wales Swansea, UK.
  September 2005. Slides: [pdf]
• Provable Anonymity: Epistemic Logic for Anonymizing Protocols.
  • SPAN (Security PhD Association Netherlands) workshop, Technical University of Delft, the Netherlands. May 2005.
  • Summer School Marktoberdorf student session, Marktoberdorf, Germany. August 2005.
  Slides: [pdf]

2003

• Kripke Completeness of First-Order Constructive Logics with Strong Negation.
  NASSLLI 2003 Student Session, Indiana University, United States.
  June 2003. Slides: [pdf]