T2 Temporal Prover

T2 Temporal Prover
Originalförfattare	Microsoft Research
Utvecklare	Microsoft
Stabil frisättning	CADE_2017 / 30 maj 2017 ; 5 år sedan
Förvar	github .com /mmjb /T2
Skrivet i	F#
Operativ system	Windows , Linux ( Debian , Ubuntu ), macOS
Plattform	.NET Framework , Mono
Typ	Programanalysator
Licens	MIT-licens
Hemsida	www .microsoft .com /en-us /research /publication /t2-temporal-property-verification /

T2 Temporal Prover är en automatiserad programanalysator utvecklad i forskningsprojektet Terminator på Microsoft Research .

Översikt

T2 syftar till att ta reda på om ett program kan köras oändligt (kallad avslutningsanalys ). Den stöder kapslade loopar och rekursiva funktioner, pekare och bieffekter och funktionspekare samt samtidiga program. Liksom alla program för avslutningsanalys försöker den lösa stoppproblemet för särskilda fall, eftersom det generella problemet är oavgörbart . Det ger en lösning som är sund , vilket innebär att när den säger att ett program alltid avslutas, är resultatet pålitligt.

Källkoden är licensierad under MIT License och värd på GitHub .

Vidare läsning

Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, Nir Piterman (2016). "T2: Verifiering av temporär egendom". TACAS:s förfarande16 . Springer . arXiv : 1512.08689 . {{ citera journal }} : CS1 underhåll: använder författarens parameter ( länk )

externa länkar

T2 Temporal Logic Prover på GitHub
T2: Publikation för temporär egendomsverifiering på Microsoft Research
Terminator Research Project at the Wayback Machine (arkiverad 4 oktober 2013)