위상 구조(Topologies) 상의 매개변수화된 프로그램에 대한 완전한 국소 추론

본 논문은 풍부한 통신 위상 구조(communication topologies) 집합 위에서 동작하는 무한 상태 매개변수화된 병행 프로그램(infinite-state parameterized concurrent programs)의 알고리즘적 안전성 검증(safety verification) 문제를 조사합니다. 목표는 위상 구조 내의 노드(nodes)들에 대해 전칭 정량화(universally quantified)된 귀납적 불변량(inductive invariant)의 형태로 정당성 증명을 자동으로 생성하는 것입니다. 우리는 기저 위상 구조(underlying topology)에 대한 합리적인 가정 하에, 이 문제가 구성적 방식(compositional scheme)으로 환원되어 해결될 수 있음을 보여줍니다. 즉, 매개변수화된 제품군(parameterized family)의 검증이 완전한 방식으로 일련의 국소적 증명(local proofs)들로 환원됩니다. 우리는 도구로 구현된 검증 알고리즘을 제안하며, 여러 다양한 위상 구조에 대한 벤치마크 세트를 통해 우리의 접근 방식이 매개변수화된 프로그램의 안전성을 증명하는 데 효과적임을 입증합니다.