Kojima Kensuke

Profile Information

Degree: 博士（情報学）(京都大学)

J-GLOBAL ID: 201101027486642825
researchmap Member ID: B000002643

数学・論理学・計算機科学の境界あたりに興味があります。
最近の主な研究内容はプログラムの形式的検証に関連する話題です。
アルゴリズムや計算量、最適化、機械学習などにも興味を持っています。

Research Interests

Research Areas

Papers

Extension of Formal Concept Analysis for (k,l)-Plex in Bipartite Graphs

Kojima, Kensuke, Wu, Ketian

45-49, Jan, 2019
Algorithms and Hardness Results for the Maximum Balanced Connected Subgraph Problem

Yasuaki Kobayashi, Kensuke Kojima, Norihide Matsubara, Taiga Sone, Akihiro Yamamoto

Combinatorial Optimization and Applications, 303-315, 2019 Peer-reviewed
Comparing BDDs and ZDDs via Categorical Properties of Boolean Functions and Combination Sets

Kojima, Kensuke

SIG-FPAI, B5(03) 57-62, Mar, 2018
Automated Verification of Functional Correctness of Race-Free GPU Programs

Kensuke Kojima, Akifumi Imanishi, Atsushi Igarashi

Journal of Automated Reasoning, 60(3) 279-298, Mar 1, 2018 Peer-reviewed
Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis

Kensuke Kojima, Minoru Kinoshita, Kohei Suenaga

Theoretical Computer Science, 2018 Peer-reviewed
A Hoare Logic for GPU Kernels

Kensuke Kojima, Atsushi Igarashi

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 18(1) 3:1-3:43, Apr, 2017 Peer-reviewed
Sharper and Simpler Nonlinear Interpolants for Program Verification.

Takamasa Okudono, Yuki Nishida, Kensuke Kojima, Kohei Suenaga, Kengo Kido, Ichiro Hasuo

CoRR, abs/1709.00314, 2017 Peer-reviewed
A nonstandard functional programming language

Hirofumi Nakamura, Kensuke Kojima, Kohei Suenaga, Atsushi Igarashi

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 10695 514-533, 2017 Peer-reviewed
Sharper and simpler nonlinear interpolants for program verification

Takamasa Okudono, Yuki Nishida, Kensuke Kojima, Kohei Suenaga, Kengo Kido, Ichiro Hasuo

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 10695 491-513, 2017 Peer-reviewed
SIMTのためのHoare論理のCoqを用いた形式化と並列prefix-sumアルゴリズムの検証

奥村健太郎, 小島健介, 五十嵐淳

第18回プログラミングおよびプログラミング言語ワークショップ論文集, Mar, 2016 Peer-reviewed
Automated Verification of Functional Correctness of Race-Free GPU Programs

Kensuke Kojima, Akifumi Imanishi, Atsushi Igarashi

Verified Software: Theories, Tools, and Experiments, VSTTE 2016, 9971 90-106, 2016 Peer-reviewed
Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis

Kensuke Kojima, Minoru Kinoshita, Kohei Suenaga

STATIC ANALYSIS, (SAS 2016), 9837 278-299, 2016 Peer-reviewed
A hoare logic for SIMT programs

Kensuke Kojima, Atsushi Igarashi

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8301 58-73, 2013 Peer-reviewed
Which classical correspondence is valid in intuitionistic modal logic?

Kensuke Kojima

LOGIC JOURNAL OF THE IGPL, 20(1) 331-348, Feb, 2012 Peer-reviewed
RELATIONAL AND NEIGHBORHOOD SEMANTICS FOR INTUITIONISTIC MODAL LOGIC

Kensuke Kojima

REPORTS ON MATHEMATICAL LOGIC, 47 87-113, 2012 Peer-reviewed
Constructive linear-time temporal logic: Proof systems and Kripke semantics

Kensuke Kojima, Atsushi Igarashi

INFORMATION AND COMPUTATION, 209(12) 1491-1503, Dec, 2011 Peer-reviewed
On Constructive Linear-Time Temporal Logic

Kensuke Kojima, Atsushi Igarashi

Proceedings of the Workshop on Intuitionistil Modal Logic and Applications (IMLA'08), Jun, 2008
Semantical study of intuitionistic modal logics

Kojima, Kensuke

Peer-reviewed

Misc.

Towards the Fixed-Parameter Tractability of the Commutative Matching Problem

112 61-66, Mar 8, 2020

Presentations

Formal Verification of the Correctness of CUDA Programs Using Hoare Logic

Kojima, Kensuke, Igarashi, Atsushi

International Symbosium on Post Petascale System Software, Dec 2, 2014
103

Towards Generic GluonJ (in Japanese)

Kojima, Kensuke, Igarashi, Atsushi

PPL 2014, Mar 5, 2014
122

A Hoare logic for SIMT programs (in Japanese)

Kojima, Kensuke, Igarashi, Atsushi

PPL 2013, Mar 4, 2013
Birelational Kripke semantics for an intuitionistic LTL

Kensuke Kojima

Topology, algebra and categories in logic (TACL) 2009, Jul, 2009
On Constructive Linear-Time Temporal Logic

Kensuke Kojima

Intuitionistic modal logic and applications (IMLA) '08, Jun, 2008

Profile Information

Research Interests

Research Areas

Papers

Misc.

Presentations

Teaching Experience

Professional Memberships

Menu

Coauthors

Following