論文 - 中澤　巧爾

Function Pointer Eliminator for C Programs 査読有り 国際共著 国際誌

Kimura, D; Al Ameen, MF; Tatsuta, M; Nakazawa, K

PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2021   13008 巻   頁： 23 - 37   2021年

　詳細を見る

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)  

Verification of memory safety such as absence of null pointer dereferences and memory leaks in system software is important in practice. O’Hearn’s group proposed a new method of memory safety analysis/verification by modular abstract interpretation with separation logic and biabduction. To realize this method, one has to construct a call graph before the modular abstract interpretation. This paper aims to analyze/verify memory safety of system software written in C programming language by this method, and as the first step this paper provides a function pointer eliminator tool to eliminate function pointer calls in order to construct a call graph. The tool uses SVF for pointer analysis. First C programs are translated into LLVM programs by Clang and then SVF analyses the LLVM programs. The tool given in this paper finds correspondence between function pointer calls in C programs and those in LLVM programs, and transforms the C programs into C programs with the same functionality and without any function pointer calls. The experimental results for gzip, git, and OpenSSL using this function pointer eliminator are presented and they show that this tool is sufficiently efficient and precise for the purpose.

DOI： 10.1007/978-3-030-89051-3_2

Web of Science

Scopus

Restriction on cut in cyclic proof system for symbolic heaps 査読有り

Kenji Saotome, Koji Nakazawa, Daisuke Kimura

The 15th International Symposium on Functional and Logic Programming (FLOPS 2020)     頁： .   2020年9月

　詳細を見る

記述言語：英語  

古典論理に対する汎用的自然演繹の証明正規化 査読有り

福井 康介, 中澤 巧爾, 石井 沙織, 結縁 祥治

第22回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2020)     頁： .   2020年3月

　詳細を見る

記述言語：日本語  

Failure of Cut-Elimination in Cyclic Proofs of Separation Logic 査読有り

Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno

  37 巻 ( 1 ) 頁： 39-52   2020年2月

　詳細を見る

記述言語：英語   掲載種別：研究論文（学術雑誌）  

Spatial Factorization in Cyclic-Proof System for Separation Logic 査読有り

Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, and Mitsuru Yamamura

    頁： .   2020年

　詳細を見る

担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（学術雑誌）  

Failure of Cut-Elimination in Cyclic Proofs of Separation Logic 査読有り

Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno

    頁： .   2019年3月

　詳細を見る

記述言語：英語  

Spatial Factorization in Cyclic-Proof System for Separation Logic 査読有り

Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, and Mitsuru Yamamura

    頁： .   2019年3月

　詳細を見る

担当区分：筆頭著者   記述言語：英語  

高階契約に対するトレース意味論の完全抽象性 査読有り

井上 鉄也, 中澤 巧爾

第20回プログラミングおよびプログラミング言語ワークショップ(PPL2018)論文集     頁： .   2018年3月

　詳細を見る

記述言語：日本語  

Z for call-by-value 査読有り

Koji Nakazawa, Ken-etsu Fujita, Yuta Imagawa

6th International Workshop on Cofluence (IWC 2017),     頁： 57–61   2017年9月

　詳細を見る

担当区分：筆頭著者   記述言語：英語  

帰納的述語定義を含む分離論理における循環証明による半自動証明

仲田 壮佑, 中澤 巧爾

日本ソフトウェア科学会第33回大会講演論文集     頁： .   2016年9月

　詳細を見る

記述言語：日本語  

DOI： .

Church-Rosser theorem and compositional Z-property

Ken-etsu Fujita, Koji Nakazawa

    頁： .   2016年9月

　詳細を見る

記述言語：英語  

DOI： .

Intersection and Union Type Assignment and Polarised Lambda-Bar-Mu-Mu-Tild 査読有り

Takeshi Tsukada, Koji Nakazawa

    頁： .   2016年3月

　詳細を見る

記述言語：英語  

DOI： .

Compositional Z: Confluence proofs for permutative conversion

K. Nakazawa, K. Fujita

    頁： .   2015年9月

　詳細を見る

担当区分：筆頭著者   記述言語：英語  

DOI： .

Strong reduction of combinatory logic with streams 査読有り

K. Nakazawa, H. Naya

Studia Logica   103 巻   頁： 375-387   2015年4月

　詳細を見る

担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（学術雑誌）  

DOI： 10.1007/s11225-014-9570-3

高階契約を持つプログラミング言語に対するトレース意味論 査読有り

村井 涼, 五十嵐 淳, 中澤 巧爾

第17回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2015)     頁： .   2015年3月

　詳細を見る

記述言語：日本語  

DOI： .

Reduction system for extensional lambda-mu calculus 査読有り

Koji Nakazawa and Tomoharu Nagai

Lecture Notes in Computer Science (RTA-TLCA 2014)   8560 巻   頁： 340-363   2014年7月

　詳細を見る

担当区分：筆頭著者   記述言語：英語  

DOI： 10.1007/978-3-319-08918-8_24

Confluence for classical logic through the distinction between values and computation 査読有り

J. Espírito Santo, R. Matthes, K. Nakazawa, L. Pinto.

Electric Proceedings in Theoretical Computer Science (CL&C 2014)   164 巻   頁： 63-77   2014年7月

　詳細を見る

記述言語：英語  

DOI： 10.4204/EPTCS.164.5

Extensional models of untyped lambda-mu calculus 査読有り

Koji Nakazawa and Shin-ya Katsumata

Electric Proceedings in Theoretical Computer Science (CL&C 2012)   97 巻   頁： 35-47   2012年10月

　詳細を見る

担当区分：筆頭著者   記述言語：英語  

DOI： 10.4204/EPTCS.97.3

Combinators for streams

K. Nakazawa

    頁： CD-ROM   2011年9月

　詳細を見る

担当区分：筆頭著者   記述言語：英語  

DOI： CD-ROM

Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems 査読有り

    頁： Article 7   2010年

　詳細を見る

担当区分：筆頭著者   記述言語：日本語   掲載種別：研究論文（学術雑誌）