제약 조건이 있는 호른 절의 기호적 실행

제약 조건이 있는 호른 절(Constrained Horn clauses, CHCs)은 검증을 위한 중간 언어로 널리 사용되는 일차 논리의 한 조각입니다. 우리는 CHC 세트의 만족 가능성에 대한 추론을 위한 계산으로서 제약 조건이 있는 분해(constrained resolution)를 연구합니다. 제약 조건이 있는 분해는 CEGAR나 IC3와 같은 모델 검사 알고리즘에 간단한 대안을 형성하며, 여기서는 상보적인 특징을 나타내는 것으로 보여집니다. CHCs가 프로그램을 인코딩할 때, 순방향 기호적 실행(forward symbolic execution)은 양의 단위 초분해(positive unit hyper-resolution)에 대응하고, 역방향 기호적 실행(backward symbolic execution)은 제약 조건이 있는 분해의 특수한 경우인 SLD 분해에 대응함을 보여줍니다. 우리는 선형 및 비선형 CHCs와 전이 시스템(transition systems)에 대한 순방향 및 역방향 추론을 형식화하고, 공정한 전략 하에서 반증적 완전성(refutational completeness)을 증명하며, 중복된 도출을 가지치기하기 위한 포섭 기준(subsumption criteria)을 개발합니다. 나아가, 포섭을 이용한 역분해는 $k$-유도(k-induction)를 비선형 CHCs로 일반화하고, 순방향 제약 조건이 있는 분해는 부정성 논리(incorrectness logic)에서 증명을 구성하는 문제와 관련되어 있음을 보여줍니다. 마지막으로, 우리는 CHC-COMP의 벤치마크에서 Eldarica CHC 솔버를 이용한 실험적 평가를 제공합니다.