Kensuke KOJIMA

Manuscripts

• Kensuke Kojima. BDDs Naturally Represent Boolean Functions, and ZDDs Naturally Represent Sets of Sets. https://arxiv.org/abs/1806.10261

Publications

• Yasuaki Kobayashi, Kensuke Kojima, Norihide Matsubara, Taiga Sone, Akihiro Yamamoto. Algorithms and Hardness Results for the Maximum Balanced Connected Subgraph Problem. In Proceedings of COCOA 2019, vol. 11949 of LNCS, pages 303-315. The final publication is available at Springer via https://doi.org/10.1007/978-3-030-36412-0_24. (Arxiv version)
• Kensuke Kojima, Minoru Kinoshita, and Kohei Suenaga. Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis. Theoretical Computer Science (published online on 19 June 2018). The final publication is available as https://doi.org/10.1016/j.tcs.2018.06.005.
• Kensuke Kojima, Akifumi Imanishi, and Atsushi Igarashi. Automated verification of functional correctness of race-free GPU programs. Journal of Automated Reasoning, 60(3):279-298, 2018. The final publication is available at Springer via http://dx.doi.org/10.1007/s10817-017-9428-2. An implementation is available as VeriCUDA.
• Takamasa Okudono, Yuki Nishida, Kensuke Kojima, Kohei Suenaga, Kengo Kido and Ichiro Hasuo. Sharper and Simpler Nonlinear Interpolants for Program Verification. In Proceedings of APLAS 2017, vol. 10695 of LNCS, pages 491-513. The final publication is available at Springer via https://doi.org/10.1007/978-3-319-71237-6_24. (Arxiv version)
• Hirofumi Nakamura, Kensuke Kojima, Kohei Suenaga and Atsushi Igarashi. A Nonstandard Functional Programming Language. In Proceedings of APLAS 2017, vol. 10695 of LNCS, pages 514-533. The final publication is available at Springer via https://doi.org/10.1007/978-3-319-71237-6_25.
• Kensuke Kojima and Atsushi Igarashi. A Hoare Logic for GPU kernels. ACM Transactions on Computational Logic, 18(1), pages 3:1--3:43, 2017. Final version is available at ACM Digital Library
• Kensuke Kojima, Akifumi Imanishi, and Atsushi Igarashi. Automated verification of functional correctness of race-free GPU programs. In Proceedings of the 8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016), vol. 9971 of LNCS, pages 90-106. Springer Verlag, 2016. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-48869-1_7.
• Kensuke Kojima, Minoru Kinoshita, and Kohei Suenaga. Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis. In Proceedings of SAS 2016, vol. 9837 of LNCS, pages 278-299. Springer Verlag, 2016. Available at http://arxiv.org/abs/1604.07201. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-53413-7_14.
• Kensuke Kojima and Atsushi Igarashi. A Hoare Logic for SIMT programs. In Proceedings of APLAS 2013, vol. 8301 of LNCS, pages 58-73. Springer Verlag, 2013. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-03542-0_5.
• Kensuke Kojima. Relational and neighborhood semantics for intuitionistic modal logic. Reports on Mathematical Logic, 47:87-113, 2012.
• Kensuke Kojima. Which classical correspondence is valid in intuitionistic modal logic? Logic Journal of the IGPL, 20(1):331-348, 2012. doi:10.1093/jigpal/jzr044
• Kensuke Kojima and Atsushi Igarashi. Constructive linear-time temporal logic: Proof systems and Kripke semantics. Information and Computation, 209(12):1491-1503, 2011. doi:10.1016/j.ic.2010.09.008

Education

• March, 2012. PhD, Graduate School of Informatics, Kyoto University
• March, 2006. MSc, Graduate School of Informatics, Kyoto University
• March, 2004. BSc, Faculty of Science, Kyoto University

Teahcing

• 2019.05-2020.03: program-specific senior lecturer, Kyoto University
• 2016.04-2016.09: part-time lecturer (Mathematical Logic), Kwansei Gakuin University
• 2007.04-2007.09: teaching assistant (Hardware and Software Laboratory Project 3), Kyoto University
• 2006.04-2006.09: teaching assistant (Hardware and Software Laboratory Project 3), Kyoto University
• 2004.10-2005-03: teaching assistant (Computation and Logic), Kyoto University

Others

• 決定グラフの自然性について（第106回人工知能基本問題研究会の発表資料に加筆・修正を行ったもの）
• Kensuke Kojima. Comparing BDDs and ZDDs via Categorical Properties of Boolean Functions and Combination Sets (non-refereed article, in Japanese). SIG-FPAI, B5(3):57--62, 2018.
• VeriCUDA, a CUDA program verifier (presented in VSTTE 2016).
• 蓮尾 一郎，奥殿 貴仁，木戸 肩吾，末永 幸平，小島 健介，西田 雄気．自動証明装置、及びプログラム．特願2017-137949，2017年7月14日
• 樹下稔，小島健介，末永幸平．不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法．PCT/JP2017/003295，2017年1月31日
• 末永 幸平，樹下 稔，小島 健介．不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法．特願2016-017441，2016年2月1日，特開2017-138679，2017年08月10日．
• 末永 幸平，樹下 稔，小島 健介．不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法．特願2016-017419，2016年2月1日，特開2017-138677，2017年08月10日．

Links

• Center of Innovative Research and Education in Data Science
• Computational Intelligence Group (Yamamoto Laboratory)
• Computer Software Group
• Department of Communications and Computer Engineering
• Graduate School of Informatics
• Kyoto University
• Some more information is available at researchmap.