Skip to content

Releases: rfago/hyperAlloy

HyperAlloy v0.1-beta — Initial public release

13 Oct 16:54
@rfago rfago
version
bff071d
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

Choose a tag to compare

View all tags
HyperAlloy v0.1-beta — Initial public release Pre-release
Pre-release

🚀 HyperAlloy v0.1-beta — Initial public release

This is the first public version of HyperAlloy, an extension of the Alloy Analyzer that enables the verification of Hyperproperties expressed in HyperLTL.

✨ Key features

  • Added support for specifying HyperLTL formulas directly in Alloy models using the hyperltl { ... } block.
  • Integrated the HyperQB backend for bounded model checking of hyperproperties.
  • Added optional integration with AutoHyper (for simple explicit-state verification).
  • Compatible with Alloy 6, Java 8+, Docker, and HyperQB.
  • Introduced example models, including Observational Determinism and Non-Interference.

⚙️ Requirements

  • Java 8+ (JDK 1.8 or higher)
  • Docker (non-root execution)
  • Environment variable HYPERQB_HOME set to the HyperQB installation path
  • NuSMV / nuXmv and Electrod (optional)

📘 Notes

  • This version is experimental and marked as pre-release.
  • The AutoHyper backend is still in early development.
  • Feedback, issues, and contributions are very welcome!
Loading