SkillsCast
Designing and Verifying Programs with Formal Specification
SkillsCast
About the Speaker
Please log in to watch this conference skillscast.
Specifications languages have demonstrated themselves as an effective tool for designing and reasoning about complex software systems by capturing a high-level description of the system behavior in temporal logic. Declarative specifications of the intent of a system also serve models that can be checked in a fully automatic way, giving engineers formal guarantees on the correctness of their designs according to their specifications.
In this talk, I will give an overview of Spectacle, a Haskell EDSL for writing formal specifications in the temporal logic of actions, and how specifications written in Spectacle can mechanically verify real-world Haskell programs.
YOU MAY ALSO LIKE:
Thank you to our sponsors and partners
Gold
Bronze