프로그램 분석

양적 약한 초과 전제: 술어 변환기를 통한 정확성과 부정확성 초과 속성의 통합

이 논문은 비결정적 및 확률적 프로그램에 대한 양적 초과 속성을 추론하기 위한 새로운 약한 전제 계산을 제시합니다. 기존 계산은 단일 초기 상태에서 종료 후 수량의 기대값을 추론할 수 있지만, 이 논문의 계산은 초기 상태 집합 또는 초기 확률 분포에 대해 이를 수행할 수 있습니다. 이를 통해 (i) 초과 Hoare 논리에 대한 약한 전제 계산을 얻고 (ii) 기대값뿐만 아니라 분산과 같은 이전 연구 범위를 벗어난 수량에 대한 추론을 가능하게 합니다. 부산물로, 기존 가장 강력한 후행 및 가장 강력한 자유 후행 계산을 확장하는 새로운 가장 강력한 후행 계산을 얻습니다. 이 프레임워크는 전방 및 후방 변환기, 정확성 및 부정확성, 그리고 비종료와 도달 불가능성 사이의 새로운 이중성을 드러냅니다.

양적 약한 초과 전제: 술어 변환기를 통한 정확성과 부정확성 초과 속성의 통합

확률적 분기 동등성 분석