{"id":1670,"date":"2021-04-10T19:22:46","date_gmt":"2021-04-10T10:22:46","guid":{"rendered":"https:\/\/group-mmm.org\/eratommsd\/?page_id=1670"},"modified":"2026-05-30T17:59:43","modified_gmt":"2026-05-30T08:59:43","slug":"theses","status":"publish","type":"page","link":"https:\/\/group-mmm.org\/eratommsd\/theses\/","title":{"rendered":"Theses"},"content":{"rendered":"\n<h2 class=\"wp-block-heading\">PhD Theses<\/h2>\n\n\n\n<ul class=\"wp-block-list\">\n<li><a href=\"https:\/\/midoriao.github.io\/portfolio\/\">Sota Sato<\/a>, <em>Logic and Optimization for Hybrid System Specification<\/em>, PhD thesis, Mar 2026. <a href=\"https:\/\/www.nii.ac.jp\/graduate\/en\/\">SOKENDAI<\/a>. <\/li>\n\n\n\n<li><a href=\"https:\/\/mkori.com\/\">Mayuko Kori<\/a>, <em>Model Checking via Fixed Points in Categories and Lattices<\/em>, PhD thesis, Mar 2025. <a href=\"https:\/\/www.nii.ac.jp\/graduate\/en\/\">SOKENDAI<\/a>. <\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/~kazuki\/\">Kazuki Watanabe<\/a>, <em>Compositional Model Checking with String Diagrams,<\/em> PhD thesis, Mar 2025. <a href=\"https:\/\/www.nii.ac.jp\/graduate\/en\/\">SOKENDAI<\/a>.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/~y-komorida\/\">Yuichi Komorida<\/a>, <em>Fibrational Theory of Behaviors and Observations: Bisimulation, Logic, and Games from Modalities<\/em>, PhD thesis, Mar 2023. <a href=\"https:\/\/www.nii.ac.jp\/graduate\/en\/\">SOKENDAI<\/a>.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/~skura\/\">Satoshi Kura<\/a>, <em>Semantic Refinements for Program Verification<\/em>, PhD thesis, Mar 2022. <a href=\"https:\/\/www.nii.ac.jp\/graduate\/en\/\">SOKENDAI<\/a>.<\/li>\n\n\n\n<li><a href=\"http:\/\/group-mmm.org\/~tokudono\/\">Takamasa Okudono<\/a>,   <em>Algebraic Abstraction in Formal Methods<\/em>, PhD thesis, Mar 2021. <a href=\"https:\/\/www.nii.ac.jp\/graduate\/en\/\">SOKENDAI<\/a>.<\/li>\n\n\n\n<li><a href=\"http:\/\/group-mmm.org\/~zhenya\/\">Zhenya Zhang<\/a>,   <em>Hierarchical Optimization for Hybrid System Falsification<\/em>, PhD thesis, Sep 2020. <a href=\"https:\/\/www.nii.ac.jp\/graduate\/en\/\">SOKENDAI<\/a>.<\/li>\n\n\n\n<li><a href=\"http:\/\/www.fos.kuis.kyoto-u.ac.jp\/~mwaga\/\">Masaki Waga<\/a>,   <em>Empowering Runtime Verification with Polyhedra<\/em>, PhD thesis, Sep 2020. <a href=\"https:\/\/www.nii.ac.jp\/graduate\/en\/\">SOKENDAI<\/a>.<\/li>\n\n\n\n<li><a href=\"https:\/\/sites.google.com\/view\/soichirofujii\/\">Soichiro Fujii<\/a>, <em>Foundations of Algebraic Theories and Higher Dimensional Categories<\/em>. PhD thesis, Mar 2019.  Dept. Comp. Sci., Univ. Tokyo. (Formal superviser: Prof. Masami Hagiya)<\/li>\n\n\n\n<li><a href=\"http:\/\/group-mmm.org\/~nurabe\/\">Natsuki Urabe<\/a>, <em>Probabilistic Verification via Category Theory: Categorical Generalization of Fair Simulation and Ranking Function by Kleisli Coalgebras, and Its Concretization<\/em>.  PhD thesis, Mar 2019.  Dept. Comp. Sci., Univ. Tokyo. (Formal superviser: Prof. Naoki Kobayashi)           <\/li>\n\n\n\n<li><a href=\"http:\/\/group-mmm.org\/~kkido\/\">Kengo Kido<\/a>, <em>Reachability Analysis of Hybrid Systems via Predicate and Relational Abstraction<\/em>. PhD thesis, Mar 2018.  Dept. Comp. Sci., Univ. Tokyo. (Formal superviser: Prof. Naoki Kobayashi)      <\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/~ayoshimizu\/\">Akira Yoshimizu<\/a>, <em>Geometry of Parallelism: A Uniform Analysis of Evaluation Strategies and Effects by Synchronous Interaction Abstract Machine<\/em>. PhD thesis, Nov 2017. Dept. Comp. Sci., Univ. Tokyo. (Formal superviser: Prof. Naoki Kobayashi)     <\/li>\n<\/ul>\n\n\n\n<h2 class=\"wp-block-heading\">MSc Theses<\/h2>\n\n\n\n<ul class=\"wp-block-list\">\n<li>Yuichiro Oyabu, <em>A Study towards an Effective Inference on Probabilistic Programs:  Hierarchical Sampling via Separation of Control and Data<\/em>. MSc thesis, Mar 2019. <a href=\"https:\/\/www.nii.ac.jp\/graduate\/en\/\">SOKENDAI<\/a>.          <\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~hkoba\/\">Hiroki Kobayashi<\/a>,      <em>Enriching and Lifting Stone-like Dualities<\/em>, MSc thesis, Mar 2018.          <br>Dept. Comp. Sci., Univ. Tokyo. (Supervised by Prof. Masami Hagiya) <\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~qnighy\/\">Masaki Hara<\/a>,      <em>(Title to be confirmed)<\/em>, MSc thesis, Mar 2018.          <br>Dept. Comp. Sci., Univ. Tokyo. (Supervised by Prof. Naoki Kobayashi) <\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~mwaga\/\">Masaki Waga<\/a>, <em>Techniques for Efficient Timed Pattern Matching<\/em>, MSc thesis, Mar 2018.          <br>Dept. Comp. Sci., Univ. Tokyo. (Supervised by Prof. Masami Hagiya) <\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~tokudono\/\">Takamasa Okudono<\/a>,      <em>Sharper and Simpler Nonlinear Interpolants for Program Verification<\/em>, MSc thesis, Mar 2018. Dept. Comp. Sci., Univ. Tokyo. (Supervised by Prof. Naoki Kobayashi)<\/li>\n\n\n\n<li>Wataru Hino,   <em>Varieties of Metric and Quantitative Algebras<\/em>, MSc thesis, Mar 2017. Dept. Comp. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li>Shunsuke Shimizu,   <em>An Automata-Theoretic Approach to Quantitative Model Checking of Coalgebras with Linear Time Logics<\/em>, MSc thesis, Mar 2017. Dept. Comp. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li>Ryo Tanaka,   <em>Token Machines for Multiport Interaction Combinators<\/em>, MSc thesis, Mar 2017. Dept. Comp. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~soichi\/\">Soichiro Fujii<\/a>,   <em>A 2-Categorical Study of Graded and Indexed Monads<\/em>, MSc thesis, Mar 2016. Dept. Comp. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~koko\/\">Koko Muroya<\/a>,   <em>Recursion and Adequacy in Memoryful Geometry of Interaction<\/em>, MSc thesis, Mar 2016. Dept. Comp. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~snakagawa\/\">Shota Nakagawa<\/a>,   <em>Near-Optimal Scheduling for Linear Temporal Logic with Future Discounting<\/em>, MSc thesis, Mar 2016. Dept. Comp. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~nurabe\/\">Natsuki Urabe<\/a>,   <em>Extension of Kleisli Simulation to Infinite Traces<\/em>, MSc thesis, Mar 2016. Dept. Comp. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~takazaki\/\">Takumi Akazaki<\/a>,   <em>Robust Semantics of MTL Sensitive to Relative Time-Constraints<\/em>, MSc thesis, Mar 2015. Dept. Comp. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~kkido\/\">Kengo Kido<\/a>,   <em>Nonstandard Abstract Interpretation with Infinitesimals for Hybrid Systems<\/em>, MSc thesis, Mar 2015. Dept. Comp. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~ckn\/\">Kenta Cho<\/a>,   <em>Semantics for a Quantum Programming Language by Operator Algebras<\/em>, MSc thesis, Mar 2014. Dept. Comp. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~tos\/\">Toshiki Kataoka<\/a>,   <em>Topos-Theoretical \u0141o\u015b Theorem: Towards Intuitionistic Nonstandard Analysis with Superstructures<\/em>, MSc thesis, Mar 2014. Dept. Comp. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~hsekine\/\">Hiroyoshi Sekine<\/a>,   <em>Verification of Hybrid Systems Using Nonstandard Stream Processing<\/em>, MSc thesis, Mar 2014. Dept. Comp. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~ayoshimizu\/\">Akira Yoshimizu<\/a>,   <em>Measurements in Proof Nets as Higher-Order Quantum Circuits<\/em>, MSc thesis, Mar 2014. Dept. Comp. Sci., Univ. Tokyo.<\/li>\n<\/ul>\n\n\n\n<h2 class=\"wp-block-heading\">BSc Theses<\/h2>\n\n\n\n<ul class=\"wp-block-list\">\n<li>Yoshihiro Kumazawa,      <em>Specification Decomposition for Hybrid System Falsification<\/em>, BSc thesis, Mar 2017. Dept. Inf. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li>Satoshi Kura,      <em>Predicate Transformers for the Second Moment of Runtime of Recursive Probabilistic Programs<\/em>, BSc thesis, Mar 2017. Dept. Inf. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li>Ibuki Okamoto,      <em>Extension of Winning Cores for Stochastic Parity Games<\/em>, BSc thesis, Mar 2017. Dept. Inf. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~hkoba\/\">Hiroki Kobayashi<\/a>,      <em>A Duality-Based Formulation of Healthiness Conditions for Weakest Preconditions<\/em>, BSc thesis, Mar 2016. Dept. Inf. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~qnighy\/\">Masaki Hara<\/a>,      <em>On Extension of Parameterized Coinduction<\/em>, BSc thesis, Mar 2016. Dept. Inf. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~mwaga\/\">Masaki Waga<\/a>,      <em>Timed Pattern Matching with Automata<\/em>, BSc thesis, Mar 2016. Dept. Inf. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~shunsuke\/\">Shunsuke Shimizu<\/a>,      <em>Coalgebraic Interpretation of Linear Temporal Logic Formulas<\/em>, BSc thesis, Mar 2015. Dept. Inf. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~alpicola\/\">Ryo Tanaka<\/a>, <em>Computational Adequacy for Productive Coprogramming<\/em>, BSc thesis, Mar 2015. Dept. Inf. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~koko\/\">Koko Muroya<\/a>,   <em>Resumption-Based Categorical Geometry of Interaction for Effects<\/em>, BSc thesis, Mar 2014. Dept. Inf. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~snakagawa\/\">Shota Nakagawa<\/a>,   <em>Games for Discrete-Time Markov Chain and Their Application to Verification<\/em>, BSc thesis, Mar 2014. Dept. Inf. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~ogawa\/\">Hiroshi Ogawa<\/a>,   <em>Coalgebraic Approach to Equivalences of Quantum Systems<\/em>, BSc thesis, Mar 2014. Dept. Inf. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~nurabe\/\">Natsuki Urabe<\/a>,   <em>Kleisli Simulation for Real-Weighted Automata and Its Algorithm<\/em>, BSc thesis, Mar 2014. Dept. Inf. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~takazaki\/\">Takumi Akazaki<\/a>,   <em>A Test Generation Methodology for Hybrid Systems with Fixed-Interval<\/em>, BSc thesis, Mar 2013. Dept. Inf. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~kkido\/\">Kengo Kido<\/a>,   <em>An Alternative Denotational Semantics for an Imperative Language with Infinitesimals<\/em>, BSc thesis, Mar 2013. Dept. Inf. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~ckn\/\">Kenta Cho<\/a>,   <em>Characterization of the Eilenberg-Moore Algebras of the Kraus Monad<\/em>, BSc thesis, Mar 2012. Dept. Inf. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li>Tetsuri Moriya,   <em>B\u00fcchi Automata, Categorically<\/em>, BSc thesis, Mar 2012. Dept. Inf. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~hsekine\/\">Hiroyoshi Sekine<\/a>,   <em>Simulink Blocks as Stream Processing: an Approach from Nonstandard Analysis<\/em>, BSc thesis, Mar 2012. Dept. Inf. Sci., Univ. Tokyo.<\/li>\n\n\n\n<li><a href=\"https:\/\/group-mmm.org\/eratommsd\/wp-admin\/~ayoshimizu\/\">Akira Yoshimizu<\/a>,   <em>On Geometry of Interaction Construction and Its Applications<\/em>, BSc thesis, Mar 2012. Dept. Inf. Sci., Univ. Tokyo.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>PhD Theses MSc Theses BSc Theses<\/p>\n","protected":false},"author":7,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"_locale":"en_US","_original_post":"1670","footnotes":""},"class_list":["post-1670","page","type-page","status-publish","hentry","en-US"],"_links":{"self":[{"href":"https:\/\/group-mmm.org\/eratommsd\/wp-json\/wp\/v2\/pages\/1670","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/group-mmm.org\/eratommsd\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/group-mmm.org\/eratommsd\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/group-mmm.org\/eratommsd\/wp-json\/wp\/v2\/users\/7"}],"replies":[{"embeddable":true,"href":"https:\/\/group-mmm.org\/eratommsd\/wp-json\/wp\/v2\/comments?post=1670"}],"version-history":[{"count":10,"href":"https:\/\/group-mmm.org\/eratommsd\/wp-json\/wp\/v2\/pages\/1670\/revisions"}],"predecessor-version":[{"id":2852,"href":"https:\/\/group-mmm.org\/eratommsd\/wp-json\/wp\/v2\/pages\/1670\/revisions\/2852"}],"wp:attachment":[{"href":"https:\/\/group-mmm.org\/eratommsd\/wp-json\/wp\/v2\/media?parent=1670"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}