T2 is a tool created for the purpose of answering sophisticated questions about the universal temporal behaviour of programs. It automatically synthesizes execution environments that impose temporal properties that would not otherwise hold. Using F#, we are able to properly express, model, and verify temporal properties of infinite-state transition systems.
YOU MAY ALSO LIKE:
- Lightning Talk: Lessons from F#: From Academic Prototypes to Safety-Critical Systems (SkillsCast recorded in April 2018)
- Applied Domain-Driven Design — Full-Stack Event Sourcing (in Online Event on 9th July 2020)
- Intro to OCaml (SkillsCast recorded in June 2020)
- What’s New in .NET Core 3.0 and .NET 5.0 for Performance and Memory-Aware Folks? (SkillsCast recorded in October 2019)
T2: A Temporal Property Verifier in F#
Heidy Khlaaf is a Research Consultant at Adelard LLP where she evaluates, specifies, and verifies the implementations of safety-critical systems. She received her PhD from University College London where she developed novel research methodologies, in part with Microsoft Research, to fully-automate the verification of temporal properties over software systems.