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)
- Functional Concurrency in .NET with C# and F# with Riccardo Terrell (Online Course on 1st - 4th December 2020)
- F# eXchange 2020 (Online Conference on 21st October 2020)
- Haskell eXchange 2020 (Online Conference on 4th - 5th November 2020)
- Build High Performance Stream Processing and Workflows with TPL Dataflow (SkillsCast recorded in October 2020)
- Applied Domain-Driven Design — Full-Stack Event Sourcing (SkillsCast recorded in July 2020)
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.