ACL2
ACL2 | |
| 패러다임 | 기능, 메타 |
|---|---|
| 설계자 | 로버트 S. 보이어, J Strother Moore 및 Matt Kaufmann |
| 개발자 | 맷 카우프만과 J 스트로터 무어 |
| 처음 등장한 | 1990년(한정배포), 1996년(공중배포) |
| 안정된 릴리스 | 8.5 / 2022년 7월 ( |
| 타이핑 분야 | 역학 |
| OS | 크로스 플랫폼 |
| 면허증. | BSD |
| 웹 사이트 | www |
| 영향을 받다 | |
| 공통 리스프, Nqthm | |
ACL2(A Computational Logic for Application Common Lisp)는 프로그래밍 언어, 1차 로직의 확장 가능 이론 및 자동 정리 프로버로 구성된 소프트웨어 시스템입니다.ACL2는 주로 소프트웨어와 하드웨어 검증을 목적으로 유도 논리 이론의 자동 추론을 지원하도록 설계되어 있습니다.ACL2의 입력 언어 및 실장은 Common Lisp로 기술되어 있습니다.ACL2는 프리 오픈소스 소프트웨어입니다.
개요
ACL2 프로그래밍 언어는 Common Lisp의 적용 가능한(부작용이 없는) 변형입니다.ACL2는 입력되지 않았습니다.모든 ACL2 함수는 합계입니다.즉, 모든 함수는 ACL2 유니버스 내의 각 오브젝트를 유니버스 내의 다른 오브젝트에 매핑합니다.
ACL2의 기본 이론은 프로그래밍 언어와 내장 함수의 의미론을 공리화한다.정의 원리를 만족시키는 프로그래밍 언어의 사용자 정의는 이론의 논리적 일관성을 유지하는 방식으로 이론을 확장합니다.
ACL2의 정리 프로버의 핵심은 용어 개서를 기반으로 하며, 이 코어는 사용자가 발견한 이론이 후속 추측을 위한 임시 증명 기술로 사용될 수 있다는 점에서 확장 가능합니다.
ACL2는 Boyer-Moore 정리프로버(NQTHM)의 "산업 강도" 버전이 되는 것을 의도하고 있습니다.이 목표를 위해 ACL2는 흥미로운 수학 및 계산 이론의 클린 엔지니어링을 지원하는 많은 기능을 갖추고 있습니다.또한 ACL2는 Common Lisp를 기반으로 구축되는 것으로부터 효율성을 얻을 수 있습니다.예를 들어 유도 검증의 기반이 되는 동일한 사양을 네이티브하게 컴파일하여 실행할 수 있습니다.
2005년에 ACL2를 포함한 Boyer-Moore 프로세서 패밀리의 저자들은 "안전에 중요한 하드웨어와 소프트웨어를 [1][2]검증하기 위한 공식 방법 도구로서 가장 효과적인 정리 프로세서(...)"를 개척하고 엔지니어링한 공로로 ACM 소프트웨어 시스템 상을 받았다.
증명서
ACL2에는 많은 산업용 [3][4]어플리케이션이 있습니다.1995년 J Strother Moore, Matt Kaufmann 및 Tom Lynch는 Pentium FDIV [5]버그가 발생한 후 ACL2를 사용하여 AMD K5 마이크로프로세서의 부동소수점 분할 동작의 정확성을 증명했습니다.ACL2 문서의 대상 응용 프로그램 페이지에는 시스템의 몇 가지 용도가 요약되어 있습니다.
ACL2의 산업 사용자에는 AMD, Arm, Centaur Technology, IBM, Intel, Oracle 및 Collins Aerospace가 포함됩니다.
레퍼런스
- ^ ACM: 프레스 릴리즈, 2006년 3월 15일
- ^ "Software System Award". ACM Awards. Association for Computing Machinery. Archived from the original on 2012-04-02. Retrieved January 14, 2012.
- ^ ACL2와 그 응용 프로그램에 관한 서적과 문서
- ^ ACL2 워크숍 시리즈
- ^ Moore, J. Strother; Lynch, Tom; Kaufmann, Matt (1996). "A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating point division algorithm". IEEE Transactions on Computers. 47. CiteSeerX 10.1.1.43.3309.
