Sign In
insight - 프로그램 논리 및 검증
프로그램 하이퍼프로퍼티 증명 및 반증을 위한 하이퍼 호어 로직
하이퍼 호어 로직은 프로그램 하이퍼프로퍼티를 증명하거나 반증할 수 있는 일반적이고 강력한 프로그램 논리이다.
프로그램 실행 경로 정렬을 통한 일반적인 관계 Hoare 논리의 완전성 증명
이 논문은 모든(∀∀) 및 일부(∀∃) 관계 속성에 대한 관계 Hoare 논리의 정렬 완전성을 증명한다. 이를 위해 일반적인 정렬 자동 장치를 사용하고, 프로그램을 정규 형태로 변환하는 기술을 개발한다. 또한 기존 관계 Hoare 논리로는 증명하기 어려운 예제들을 다룰 수 있는 추가 규칙을 제시한다.
효과를 가진 프로그램의 정확성과 부정확성에 대한 국소적 추론을 위한 결과 분리 논리
결과 분리 논리(OSL)는 다양한 효과를 가진 프로그램에서 정확성과 부정확성 추론을 모두 지원하는 프로그램 논리이다. OSL은 분리 논리의 구성성과 국소적 추론 특성을 활용하여, 단일 논리 체계 내에서 정확성과 부정확성 분석을 통합할 수 있다.
프로그램 정확성과 부정확성을 위한 국소적 추론을 지원하는 결과 분리 논리
결과 분리 논리(OSL)는 다양한 계산 효과를 가진 프로그램에서 정확성과 부정확성 추론을 모두 지원하는 프로그램 논리이다. OSL은 분리 논리와 유사한 프레임 규칙을 가지지만, 더 넓은 범위의 속성에 대한 국소적 추론을 가능하게 하는 다른 기본 가정을 사용한다.