Skip to content

Embedded specification language & model checker in Haskell

License

Notifications You must be signed in to change notification settings

agentultra/spectacle

This branch is 6 commits behind awakesecurity/spectacle:main.

Folders and files

NameName
Last commit message
Last commit date
Jun 10, 2021
Mar 19, 2021
Mar 30, 2021
Apr 29, 2021
Aug 20, 2021
Aug 20, 2021
Mar 19, 2021
Mar 19, 2021
Mar 19, 2021
Aug 16, 2021
Mar 19, 2021
Apr 29, 2021
Apr 29, 2021
Apr 29, 2021
Aug 20, 2021

Repository files navigation

spectacle

ci

Language.Spectacle defines an embedded language for writing formal specifications of software in the temporal logic of actions. Specifications written in spectacle can be model-checked and shown to either be correct with respect to temporal properties or refuted by a counterexample. Examples of specifications written in spectacle are provided under test/integration.

About

Embedded specification language & model checker in Haskell

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Haskell 99.4%
  • Other 0.6%