T2 시간 프로베러

T2 Temporal Prover
T2 시간 프로베러
원본 작성자마이크로소프트 리서치
개발자마이크로소프트
안정적 해제
CADE_2017 / 2017년 5월 30일; 4년 전(2017-05-30)
리포지토리github.com/mmjb/T2
기록 위치F#
운영 체제Windows, Linux(Debian, Ubuntu), MacOS
플랫폼.NET Framework, Mono
유형프로그램 분석기
면허증MIT 라이선스
웹사이트www.microsoft.com/en-us/research/publication/t2-temporal-property-verification/

T2 T2 Temporary Prover는 마이크로소프트 리서치의 터미네이터 연구 프로젝트에서 개발된 자동화 프로그램 분석기다.

개요

T2는 프로그램이 무한정 실행될 수 있는지 여부(종료 분석이라고 함)를 알아내는 것을 목표로 한다.중첩된 루프 및 재귀 기능, 포인터와 부작용, 기능 포인터는 물론 동시 프로그램을 지원한다.종단 분석을 위한 모든 프로그램과 마찬가지로, 일반적인 문제는 이해할 수 없기 때문에 특정 사례의 중단 문제를 해결하려고 한다.[1]그것은 프로그램이 항상 종료된다고 말할 때 그 결과는 신뢰할 수 있다는 것을 의미하는 건전한 해결책을 제공한다.

소스 코드는 MIT 라이센스에 따라 라이센스가 부여되며 GitHub에서 호스팅된다.[2]

참조

  1. ^ Rob Knies. "Terminator Tackles an Impossible Task". Retrieved 2010-05-25.
  2. ^ "GitHub - mmjb/T2: T2 Temporal Prover". December 4, 2019 – via GitHub.

추가 읽기

  • Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, Nir Piterman (2016). "T2 : Temporal Property Verification". Proceedings of TACAS'16. Springer. arXiv:1512.08689.{{cite journal}}: CS1 maint: 작성자 매개변수 사용(링크)

외부 링크

Stub icon

이 마이크로소프트 윈도우즈 소프트웨어 관련 기사는 단조롭다.위키피디아를 확장하여 도울 수 있다.

Stub icon

이 과학 소프트웨어 기사는 단조롭다.위키피디아를 확장하여 도울 수 있다.