C와 유사한 언어에서 정수-포인터 변환 지원을 위한 메모리 모델 설계: 이중 비결정성을 사용하여 


51권  7호, pp. 643-654, 7월  2024
10.5626/JOK.2024.51.7.643


PDF

  요약

시스템 프로그래밍에서 포인터는 매우 중요한 요소이며, 정수-포인터 변환(Integer-Pointer Casting)을 포함한 프로그램에 정형 검증을 적용하는 것은 중요한 과제이다. 정수-포인터 변환을 포함한 프로그램을 정형 검증하기 위해서는 정수-포인터 변환을 지원하는 수학적으로 정의된 메모리 모델과 검증 에 사용할 증명 방법이 필요하다. 우리는 Coq 증명 도구 안에서 정수-포인터 변환을 지원하는 메모리 모델을 정의했다. 이 모델은 끝에서 한 칸 벗어난 포인터(one-past-the-end pointer)를 포함한 정수-포인터 연산과 관련된 패턴을 제대로 지원한다. 또한 우리가 정의한 모델을 프로그램 검증에 사용할 수 있도록 시뮬레이션 기반 증명 방법론을 새로 정의하고 적합성(Adequacy)을 증명했다. 마지막으로 우리의 접근 방법 이 타당함을 확인하기 위해 검증된 C 컴파일러인 CompCert의 메모리 모델과 의미 구조를 우리가 정의한 것으로 변경한 후 시뮬레이션을 통해서 CompCert의 최적화 검증 증명 중 두 개를 업데이트했다. 우리는 이 메모리 모델이 컴파일러와 정수-포인터 연산을 포함하는 프로그램 검증에 적용되기를 기대하고 있다.


  통계
2022년 11월부터 누적 집계
동일한 세션일 때 여러 번 접속해도 한 번만 카운트됩니다. 그래프 위에 마우스를 올리면 자세한 수치를 확인하실 수 있습니다.
  논문 참조

[IEEE Style]

Y. Kim and C. Hur, "Memory Model Design for Integer-Pointer Casting Support in C-like languages Via Dual Non-determinism," Journal of KIISE, JOK, vol. 51, no. 7, pp. 643-654, 2024. DOI: 10.5626/JOK.2024.51.7.643.


[ACM Style]

Yonghyun Kim and Chung-Kil Hur. 2024. Memory Model Design for Integer-Pointer Casting Support in C-like languages Via Dual Non-determinism. Journal of KIISE, JOK, 51, 7, (2024), 643-654. DOI: 10.5626/JOK.2024.51.7.643.


[KCI Style]

김용현, 허충길, "C와 유사한 언어에서 정수-포인터 변환 지원을 위한 메모리 모델 설계: 이중 비결정성을 사용하여," 한국정보과학회 논문지, 제51권, 제7호, 643~654쪽, 2024. DOI: 10.5626/JOK.2024.51.7.643.


[Endnote/Zotero/Mendeley (RIS)]  Download


[BibTeX]  Download



Search




Journal of KIISE

  • ISSN : 2383-630X(Print)
  • ISSN : 2383-6296(Electronic)
  • KCI Accredited Journal

사무국

  • Tel. +82-2-588-9240
  • Fax. +82-2-521-1352
  • E-mail. chwoo@kiise.or.kr