Z3 정리 프로베라
Z3 Theorem Prover | |
| 원본 작성자 | 마이크로소프트 리서치 |
|---|---|
| 개발자 | 마이크로소프트 |
| 초기 릴리즈 | 2012; 전( |
| 안정적 해제 | z3-4.8.14 / 2021년 12월 23일; 전[1] |
| 리포지토리 | github |
| 기록 위치 | C++ |
| 운영 체제 | Windows, FreeBSD, Linux(Debian, Ubuntu), MacOS |
| 플랫폼 | IA-32, x86-64 |
| 유형 | 정리프로베라 |
| 면허증 | MIT 라이선스 |
| 웹사이트 | github |
Z3 Orgion Prober라고도 알려진 Z3는 마이크로소프트가 제안한 교차 플랫폼 만족도 모듈로 이론(SMT) 해결사다.[2]
개요
Z3는 마이크로소프트 리서치사의 소프트웨어 엔지니어링(RSE) 그룹에서 개발됐으며 소프트웨어 검증과 소프트웨어 분석에서 발생하는 문제를 해결하는 것을 목표로 하고 있다.Z3은 산술, 고정 크기 비트 벡터, 확장 배열, 데이터 유형, 해석되지 않은 함수 및 정량자를 지원한다.그것의 주요 적용 분야는 확장된 정적 확인, 테스트 사례 생성, 술어 추상화다.
2015년에는 ACM SIG플랜으로부터 프로그래밍 언어 소프트웨어상을, 2018년에는 Z3가 유럽공동 소프트웨어 이론 및 실무회의(ETAPS)로부터 Test of Time Award를 받았다.[3][4][5]마이크로소프트의 연구원인 니콜라즈 비외르너와 레오나르도 드 모우라는 Z3로 증명된 정리를 진전시킨 공로를 인정받아 2019년 헤르브랜드상을 수상하였다.[6][7]
Z3는 2015년 초에 오픈 소싱되었다.[8]소스 코드는 MIT 라이센스에 따라 라이센스가 부여되며 GitHub에서 호스팅된다.[9]해결사는 Visual Studio, Makefile 또는 CMake를 사용하여 빌드할 수 있으며 Windows, FreeBSD, Linux 및 MacOS에서 실행된다.
C, C++, Java, Julia, Haskell, OCaml, Python, WebAssembly, 등 다양한 프로그래밍 언어의 바인딩을 가지고 있다.NET/Mono.기본 입력 형식은 SMTLIB2이다.
예
명제적 및 술어적 논리학
이 예에서 명제 논리 주장은 명제 a와 b를 나타내는 함수를 사용하여 점검한다.다음 Z3 스크립트는 의 b이(가) 표시되는지 점검한다
(선언-fun a) bool)(선언-fun b) bool)(assert (=(및 b)가 아님(또는 (a)가 아님)) (check-sat))
결과:
언스태트의
이 대본은 관심 제안의 부정을 주장한다는 점에 유의한다.그 결과는 부정된 명제가 만족스럽지 못함을 의미하므로, 원하는 결과(De Morgan의 법칙)를 증명한다.
풀림 방정식
다음 스크립트는 변수 a와 b에 적합한 값을 찾아 주어진 두 방정식을 해결한다.
(선언-수치-수치-수치-수치-수치-수치-수치-수치-수치-수치-b) (수치(=+ b) 20) (수치 (+2 b) 10) (수치-수치-수치-수치) (get-모형)
결과:
sat (모델 정의-fun b) Int -10)(define-fun a ()Int 30) )
참고 항목
참조
- ^ "Release z3-4.8.14 · Z3Prover/Z3".
- ^ "Archived copy" (PDF). Archived from the original (PDF) on 2020-11-17. Retrieved 2019-12-01.
{{cite web}}: CS1 maint: 타이틀로 보관된 사본(링크) - ^ "Programming Languages Software Award". www.sigplan.org.
- ^ 마이크로소프트 Z3 정리 프로베러상 수상
- ^ ETAPS 2018 Test of Time Award
- ^ Z3 정리 프로베렐 뒤에 숨겨진 내면의 마술 - 마이크로소프트 리서치
- ^ 허브랜드상
- ^ "Microsoft's Visual Studio timeline and Z3 Theorem Prover, Google Cloud Launcher, Facebook's Fresco—SD Times news digest: March 27, 2015". March 27, 2015.
- ^ "GitHub - Z3Prover/z3: The Z3 Theorem Prover". December 1, 2019 – via GitHub.
추가 읽기
- Leonardo De Moura, Nikolaj Bjørner (2008). "Z3: an efficient SMT solver". Tools and Algorithms for the Construction and Analysis of Systems. 4963: 337–340.
{{cite journal}}: CS1 maint: 작성자 매개변수 사용(링크) - Dennis Yurichev - SAT/SMT by 예 - Z3Py를 사용하는 많은 예와 함께.
- SMT(Integer)를 사용하여 클래식, 자이언트 및 기타 스도쿠 문제 해결 Z3과 같은 SMT(Integer) 해결사 사용
- 체스 보드에 퀸즈 배치 퍼즐 풀기 Z3 같은 SMT(Integer) 해결사를 사용한다.
