A Satisfiability Solver for Hyperproperties
-
Updated
Apr 29, 2024 - C++
A Satisfiability Solver for Hyperproperties
Prototype implementation of a hyperbug finder for ∀∃-safety hyperproperties to accompany the OOPSLA 2024 paper "Finding ∀∃ Hyperbugs using Symbolic Execution" by Arthur Correnson, Tobias Nießen, Bernd Finkbeiner, and Georg Weissenbacher.
Prototypical Implementation for the Research Paper "Attack Resilience Hyperproperties: Formal Security Analysis of (Automotive) Network Architectures under Active Compromise"
A BeepBeep palette to evaluate hyperqueries on event logs
Runtime verification of hypernode logic and automata
Monitoring hyperproperties with Multi-trace prefix transducers
Go PoC for ASM-based behavioral attestation of information-flow non-interference in a concurrent multi-level stack. Companion artifact for our MEMOCODE 2026 paper.
Extension of Alloy Analyzer for Hyperproperties (HyperLTL) via HyperQB and AutoHyper integration.
To associate your repository with the hyperproperties topic, visit your repo's landing page and select "manage topics."