{"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":"2025-04-11T15:31:06","modified_gmt":"2025-04-11T06:31:06","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\"><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><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><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><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><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><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><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><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><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><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><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><\/ul>\n\n\n\n<h2 class=\"wp-block-heading\">MSc Theses<\/h2>\n\n\n\n<ul class=\"wp-block-list\"><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><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><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><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><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><li>Wataru Hino,   <em>Varieties of Metric and Quantitative Algebras<\/em>, MSc thesis, Mar 2017. Dept. Comp. Sci., Univ. Tokyo.<\/li><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><li>Ryo Tanaka,   <em>Token Machines for Multiport Interaction Combinators<\/em>, MSc thesis, Mar 2017. Dept. Comp. Sci., Univ. Tokyo.<\/li><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><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><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><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><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><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><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><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><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><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><\/ul>\n\n\n\n<h2 class=\"wp-block-heading\">BSc Theses<\/h2>\n\n\n\n<ul class=\"wp-block-list\"><li>Yoshihiro Kumazawa,      <em>Specification Decomposition for Hybrid System Falsification<\/em>, BSc thesis, Mar 2017. Dept. Inf. Sci., Univ. Tokyo.<\/li><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><li>Ibuki Okamoto,      <em>Extension of Winning Cores for Stochastic Parity Games<\/em>, BSc thesis, Mar 2017. Dept. Inf. Sci., Univ. Tokyo.<\/li><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><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><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><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><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><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><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><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><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><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><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><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><li>Tetsuri Moriya,   <em>B\u00fcchi Automata, Categorically<\/em>, BSc thesis, Mar 2012. Dept. Inf. Sci., Univ. Tokyo.<\/li><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><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><\/ul>\n","protected":false},"excerpt":{"rendered":"<p>PhD Theses Mayuko Kori, Model Checking via Fixed Points in Categories and Lattices, PhD thesis, Mar 2025. SOKENDAI. Kazuki Watanabe, Compositional Model Checking with String Diagrams, PhD thesis, Mar 2025. SOKENDAI. 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 &hellip; <a href=\"https:\/\/group-mmm.org\/eratommsd\/theses\/\" class=\"more-link\">Continue reading <span class=\"screen-reader-text\">Theses<\/span><\/a><\/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":2753,"href":"https:\/\/group-mmm.org\/eratommsd\/wp-json\/wp\/v2\/pages\/1670\/revisions\/2753"}],"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}]}}