[Paper] SV-LIB 1.0: 소프트웨어 검증 작업을 위한 표준 교환 형식

Source: arXiv - 2511.21509v1

Overview

지난 20년 동안 C, C++, Java와 같은 개별 언어를 위한 검증 도구 개발에 상당한 연구 및 개발 노력이 투입되었습니다. 사용된 많은 검증 접근법은 실제로 언어에 구애받지 않으며, 기술 이전을 위해 이러한 구현을 다른 프로그래밍 및 모델링 언어에도 사용할 수 있도록 하는 것이 유익합니다. 이 문제를 해결하기 위해 우리는 SV‑LIB을 제안합니다. SV‑LIB은 소프트웨어 검증 작업(프로그램, 사양, 검증 증거)을 위한 교환 형식이자 중간 언어이며, 명령형 프로그래밍 언어의 잘 알려진 개념을 기반으로 하고 프로그램에서 사용되는 표현식과 정렬을 나타내기 위해 SMT‑LIB을 사용합니다. 이는 많은 검증 도구가 이미 SMT 솔버를 기반으로 하고 있기 때문에 파싱과 기존 인프라에 통합하기 쉽습니다. 또한 SV‑LIB은 올바른 프로그램과 잘못된 프로그램 모두에 대한 증거 형식을 정의하고, 증거 검증 작업을 지정하는 방법을 제공합니다. 이를 통해 독립적인 증거 검증기를 구현하고, 일부 검증기를 증거 검증기로 재사용하는 것이 가능해집니다. 본 논문은 SV‑LIB 형식의 버전 1.0을 소개하며, 설계 목표, 구문, 비공식 의미론을 포함합니다. 형식 의미론 및 동시성에 대한 추가 확장은 향후 버전에서 계획되고 있습니다.

Authors

• Dirk Beyer
• Gidon Ernst
• Martin Jonáš
• Marian Lingsch‑Rosenfeld

Categories

cs.PL, cs.SC, cs.SE

Paper Information

• arXiv ID: 2511.21509v1
• Categories: cs.PL, cs.SC, cs.SE
• Published: November 27, 2025
• PDF: Download PDF