Theses

PhD Theses

  • Yuichi Komorida, Fibrational Theory of Behaviors and Observations: Bisimulation, Logic, and Games from Modalities, PhD thesis, Mar 2023. SOKENDAI.
  • Satoshi Kura, Semantic Refinements for Program Verification, PhD thesis, Mar 2022. SOKENDAI.
  • Takamasa Okudono, Algebraic Abstraction in Formal Methods, PhD thesis, Mar 2021. SOKENDAI.
  • Zhenya Zhang, Hierarchical Optimization for Hybrid System Falsification, PhD thesis, Sep 2020. SOKENDAI.
  • Masaki Waga, Empowering Runtime Verification with Polyhedra, PhD thesis, Sep 2020. SOKENDAI.
  • Soichiro Fujii, Foundations of Algebraic Theories and Higher Dimensional Categories. PhD thesis, Mar 2019. Dept. Comp. Sci., Univ. Tokyo. (Formal superviser: Prof. Masami Hagiya)
  • Natsuki Urabe, Probabilistic Verification via Category Theory: Categorical Generalization of Fair Simulation and Ranking Function by Kleisli Coalgebras, and Its Concretization. PhD thesis, Mar 2019. Dept. Comp. Sci., Univ. Tokyo. (Formal superviser: Prof. Naoki Kobayashi)
  • Kengo Kido, Reachability Analysis of Hybrid Systems via Predicate and Relational Abstraction. PhD thesis, Mar 2018. Dept. Comp. Sci., Univ. Tokyo. (Formal superviser: Prof. Naoki Kobayashi)
  • Akira Yoshimizu, Geometry of Parallelism: A Uniform Analysis of Evaluation Strategies and Effects by Synchronous Interaction Abstract Machine. PhD thesis, Nov 2017. Dept. Comp. Sci., Univ. Tokyo. (Formal superviser: Prof. Naoki Kobayashi)

MSc Theses

  • Yuichiro Oyabu, A Study towards an Effective Inference on Probabilistic Programs: Hierarchical Sampling via Separation of Control and Data. MSc thesis, Mar 2019. SOKENDAI.
  • Hiroki Kobayashi, Enriching and Lifting Stone-like Dualities, MSc thesis, Mar 2018.
    Dept. Comp. Sci., Univ. Tokyo. (Supervised by Prof. Masami Hagiya)
  • Masaki Hara, (Title to be confirmed), MSc thesis, Mar 2018.
    Dept. Comp. Sci., Univ. Tokyo. (Supervised by Prof. Naoki Kobayashi)
  • Masaki Waga, Techniques for Efficient Timed Pattern Matching, MSc thesis, Mar 2018.
    Dept. Comp. Sci., Univ. Tokyo. (Supervised by Prof. Masami Hagiya)
  • Takamasa Okudono, Sharper and Simpler Nonlinear Interpolants for Program Verification, MSc thesis, Mar 2018. Dept. Comp. Sci., Univ. Tokyo. (Supervised by Prof. Naoki Kobayashi)
  • Wataru Hino, Varieties of Metric and Quantitative Algebras, MSc thesis, Mar 2017. Dept. Comp. Sci., Univ. Tokyo.
  • Shunsuke Shimizu, An Automata-Theoretic Approach to Quantitative Model Checking of Coalgebras with Linear Time Logics, MSc thesis, Mar 2017. Dept. Comp. Sci., Univ. Tokyo.
  • Ryo Tanaka, Token Machines for Multiport Interaction Combinators, MSc thesis, Mar 2017. Dept. Comp. Sci., Univ. Tokyo.
  • Soichiro Fujii, A 2-Categorical Study of Graded and Indexed Monads, MSc thesis, Mar 2016. Dept. Comp. Sci., Univ. Tokyo.
  • Koko Muroya, Recursion and Adequacy in Memoryful Geometry of Interaction, MSc thesis, Mar 2016. Dept. Comp. Sci., Univ. Tokyo.
  • Shota Nakagawa, Near-Optimal Scheduling for Linear Temporal Logic with Future Discounting, MSc thesis, Mar 2016. Dept. Comp. Sci., Univ. Tokyo.
  • Natsuki Urabe, Extension of Kleisli Simulation to Infinite Traces, MSc thesis, Mar 2016. Dept. Comp. Sci., Univ. Tokyo.
  • Takumi Akazaki, Robust Semantics of MTL Sensitive to Relative Time-Constraints, MSc thesis, Mar 2015. Dept. Comp. Sci., Univ. Tokyo.
  • Kengo Kido, Nonstandard Abstract Interpretation with Infinitesimals for Hybrid Systems, MSc thesis, Mar 2015. Dept. Comp. Sci., Univ. Tokyo.
  • Kenta Cho, Semantics for a Quantum Programming Language by Operator Algebras, MSc thesis, Mar 2014. Dept. Comp. Sci., Univ. Tokyo.
  • Toshiki Kataoka, Topos-Theoretical Łoś Theorem: Towards Intuitionistic Nonstandard Analysis with Superstructures, MSc thesis, Mar 2014. Dept. Comp. Sci., Univ. Tokyo.
  • Hiroyoshi Sekine, Verification of Hybrid Systems Using Nonstandard Stream Processing, MSc thesis, Mar 2014. Dept. Comp. Sci., Univ. Tokyo.
  • Akira Yoshimizu, Measurements in Proof Nets as Higher-Order Quantum Circuits, MSc thesis, Mar 2014. Dept. Comp. Sci., Univ. Tokyo.

BSc Theses

  • Yoshihiro Kumazawa, Specification Decomposition for Hybrid System Falsification, BSc thesis, Mar 2017. Dept. Inf. Sci., Univ. Tokyo.
  • Satoshi Kura, Predicate Transformers for the Second Moment of Runtime of Recursive Probabilistic Programs, BSc thesis, Mar 2017. Dept. Inf. Sci., Univ. Tokyo.
  • Ibuki Okamoto, Extension of Winning Cores for Stochastic Parity Games, BSc thesis, Mar 2017. Dept. Inf. Sci., Univ. Tokyo.
  • Hiroki Kobayashi, A Duality-Based Formulation of Healthiness Conditions for Weakest Preconditions, BSc thesis, Mar 2016. Dept. Inf. Sci., Univ. Tokyo.
  • Masaki Hara, On Extension of Parameterized Coinduction, BSc thesis, Mar 2016. Dept. Inf. Sci., Univ. Tokyo.
  • Masaki Waga, Timed Pattern Matching with Automata, BSc thesis, Mar 2016. Dept. Inf. Sci., Univ. Tokyo.
  • Shunsuke Shimizu, Coalgebraic Interpretation of Linear Temporal Logic Formulas, BSc thesis, Mar 2015. Dept. Inf. Sci., Univ. Tokyo.
  • Ryo Tanaka, Computational Adequacy for Productive Coprogramming, BSc thesis, Mar 2015. Dept. Inf. Sci., Univ. Tokyo.
  • Koko Muroya, Resumption-Based Categorical Geometry of Interaction for Effects, BSc thesis, Mar 2014. Dept. Inf. Sci., Univ. Tokyo.
  • Shota Nakagawa, Games for Discrete-Time Markov Chain and Their Application to Verification, BSc thesis, Mar 2014. Dept. Inf. Sci., Univ. Tokyo.
  • Hiroshi Ogawa, Coalgebraic Approach to Equivalences of Quantum Systems, BSc thesis, Mar 2014. Dept. Inf. Sci., Univ. Tokyo.
  • Natsuki Urabe, Kleisli Simulation for Real-Weighted Automata and Its Algorithm, BSc thesis, Mar 2014. Dept. Inf. Sci., Univ. Tokyo.
  • Takumi Akazaki, A Test Generation Methodology for Hybrid Systems with Fixed-Interval, BSc thesis, Mar 2013. Dept. Inf. Sci., Univ. Tokyo.
  • Kengo Kido, An Alternative Denotational Semantics for an Imperative Language with Infinitesimals, BSc thesis, Mar 2013. Dept. Inf. Sci., Univ. Tokyo.
  • Kenta Cho, Characterization of the Eilenberg-Moore Algebras of the Kraus Monad, BSc thesis, Mar 2012. Dept. Inf. Sci., Univ. Tokyo.
  • Tetsuri Moriya, Büchi Automata, Categorically, BSc thesis, Mar 2012. Dept. Inf. Sci., Univ. Tokyo.
  • Hiroyoshi Sekine, Simulink Blocks as Stream Processing: an Approach from Nonstandard Analysis, BSc thesis, Mar 2012. Dept. Inf. Sci., Univ. Tokyo.
  • Akira Yoshimizu, On Geometry of Interaction Construction and Its Applications, BSc thesis, Mar 2012. Dept. Inf. Sci., Univ. Tokyo.