pith. sign in

arxiv: 2512.12024 · v2 · submitted 2025-12-12 · 💻 cs.SE · cs.CR

Model checking of hyperproperties for high-level relational models

Nuno Macedo , Hugo Pacheco This is my paper

Pith reviewed 2026-05-16 22:35 UTC · model grok-4.3

classification 💻 cs.SE cs.CR
keywords hyperpropertiesmodel checkingAlloyrelational modelsPardinustemporal logicsecurity verificationdesign models
0
0 comments X

The pith

HyperPardinus extends Alloy to automatically verify hyperproperties over relational design models using low-level checkers.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces HyperPardinus to add hyperproperty verification to Alloy, a lightweight language for early-stage relational modeling of systems. Hyperproperties capture behaviors across multiple traces, such as information-flow security or concurrency properties, which single-trace checks cannot address. The approach builds on Pardinus, Alloy's temporal backend, by translating high-level models into inputs for existing low-level hyperproperty model checkers. This preserves semantics and adds support for specification, automated checking, and high-level visualization of counterexamples. If the translation works as intended, it lets practitioners catch complex alternating-quantifier properties during design rather than later implementation stages.

Core claim

HyperPardinus is a new model finding procedure that extends Pardinus, the temporal logic backend of Alloy, to automatically verify hyperproperties over relational models by relying on existing low-level model checkers for hyperproperties. It conservatively extends Alloy to support the specification and automatic verification of hyperproperties over design models, as well as the visualization of counterexamples at a higher level of abstraction.

What carries the argument

HyperPardinus, a translation layer that maps high-level Alloy relational models annotated with hyperproperties to equivalent inputs for low-level hyperproperty model checkers.

If this is right

  • Enables modeling and finding counterexamples for complex hyperproperties with alternating quantifiers directly in Alloy.
  • Makes verification of relevant state-of-the-art hyperproperty scenarios feasible for software engineering practitioners.
  • Supports visualization of counterexamples at the same high level of abstraction as the original design models.
  • Bridges early-stage relational modeling with rigorous multi-trace property checking without requiring new low-level languages.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The extension could allow Alloy users to incorporate hyperproperty checks into existing workflows with minimal changes to their modeling practice.
  • Similar translation techniques might be adapted to other high-level modeling languages to widen access to hyperproperty verification.
  • It could support earlier detection of information-flow and non-interference issues in concurrent or distributed system designs.

Load-bearing premise

The translation from high-level Alloy relational models to the low-level hyperproperty checker inputs preserves the original semantics without introducing spurious behaviors or losing expressiveness.

What would settle it

A case where a hyperproperty holds in the original Alloy model but the translated low-level input produces a counterexample, or vice versa, demonstrating semantic mismatch.

Figures

Figures reproduced from arXiv: 2512.12024 by Hugo Pacheco, Nuno Macedo.

Figure 1
Figure 1. Figure 1: Overview of the proposed toolchain. Rectangles are interchangeable formats, rounded rectangles software components, [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The CMS system in extended Alloy The rest of the paper is organized as follows. Section 2 motivates the approach with an example. Section 3 discusses related work on hyperproperties. Section 4 formalizes the notion of hyper model finding problem, and Section 5 presents the HyperPardinus model finder for such problems. Section 6 presents the lower-level model checker HyperSMV. Section 7 presents the extende… view at source ↗
Figure 3
Figure 3. Figure 3: Hyperproperties in extended Alloy over the [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Possible counter-example for the NI property of CMS all reviews and decisions of articles assigned to him. Let us model an optimistic editor that always chooses the best decision from those submitted by reviewers to the given article a, which could be expressed as follows. fun criteria[a:Article,s:CMS] : set Decision { max[Reviewer.(a.(s.reviews))] } Expression a.(s.reviews) retrieves decisions submitted b… view at source ↗
Figure 5
Figure 5. Figure 5: Formula and expression semantics, 𝑎, 𝑏, 𝑐 are atoms from an implicitly defined A. trace variable being evaluated. A trace instance of a hyper problem 𝐻 is a valuation 𝐼 for the variables declared in 𝐻 such that the bounds and constraint hold. Definition 4.4. A trace 𝐼 : N → R ↦→ P(A∗ ) is an instance of an hyper model finding problem over problems 𝑃𝑖 and 𝐻 = ⟨A, D, Φ⟩, 𝐼 |= 𝐻, iff 𝐼 |= D and 𝜋0 ↦→ 𝐼, 𝜋0, 0… view at source ↗
read the original abstract

Many properties related to security or concurrency must be encoded as so-called hyperproperties, temporal properties that allow reasoning about multiple traces of a system. However, despite recent advances on model checking hyperproperties, there is still a lack of higher-level specification languages that can effectively support software engineering practitioners in verifying properties of this class at early stages of system design. Alloy is a lightweight formal method with a high-level specification language that is supported by automated analysis procedures, making it particularly well-suited for the verification of design models at early development stages. It does not natively support, however, the verification of hyperproperties. This work proposes HyperPardinus, a new model finding procedure that extends Pardinus -- the temporal logic backend of the Alloy language -- to automatically verify hyperproperties over relational models by relying on existing low-level model checkers for hyperproperties. It then conservatively extends Alloy to support the specification and automatic verification of hyperproperties over design models, as well as the visualization of (counter-)examples at a higher-level of abstraction. Evaluation shows that our approach enables modeling and finding (counter-)examples for complex hyperproperties with alternating quantifiers, making it feasible to address relevant scenarios from the state of the art.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces HyperPardinus, a conservative extension of Pardinus (Alloy's temporal backend) that translates high-level relational Alloy models to inputs for existing low-level hyperproperty model checkers, thereby enabling specification, verification, and visualization of hyperproperties (including those with alternating quantifiers) directly in Alloy.

Significance. If the translation is shown to preserve semantics, the work would allow practitioners to check complex security and concurrency hyperproperties at the design-model level using familiar Alloy syntax and analysis, rather than requiring direct use of low-level hyperproperty tools.

major comments (2)
  1. [HyperPardinus translation] The translation algorithm (described in the section introducing HyperPardinus): the manuscript provides no theorem, bisimulation relation, or inductive argument establishing that every satisfying trace (and counterexample) in the high-level relational model corresponds exactly to one in the low-level encoding for formulas with alternating quantifiers; without this, the central claim that the approach finds (counter-)examples for state-of-the-art scenarios cannot be considered fully supported.
  2. [Evaluation] Evaluation section: the abstract asserts successful evaluation on state-of-the-art scenarios, yet the manuscript supplies neither quantitative performance data (e.g., runtimes, memory) nor details of the translation steps or semantic-preservation argument, leaving the feasibility claim only partially evidenced.
minor comments (2)
  1. [Introduction] The introduction should explicitly state the scope of the conservative extension (e.g., which Alloy constructs are supported and which are excluded) to avoid ambiguity for readers.
  2. [Background] Notation for hyperproperty quantifiers and relational joins should be clarified with a small running example early in the paper.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments, which help strengthen the presentation of HyperPardinus. We address each major comment below and commit to revisions that directly respond to the concerns raised.

read point-by-point responses

  1. Referee: [HyperPardinus translation] The translation algorithm (described in the section introducing HyperPardinus): the manuscript provides no theorem, bisimulation relation, or inductive argument establishing that every satisfying trace (and counterexample) in the high-level relational model corresponds exactly to one in the low-level encoding for formulas with alternating quantifiers; without this, the central claim that the approach finds (counter-)examples for state-of-the-art scenarios cannot be considered fully supported.

    Authors: We agree that a formal semantic-preservation argument is necessary to fully support the central claim, especially for hyperproperties with alternating quantifiers. The current manuscript relies on the conservative nature of the extension and the correctness of the underlying low-level checkers, but does not supply an explicit theorem or inductive argument. In the revised version we will add a dedicated subsection containing (i) a bisimulation relation between high-level relational traces and the low-level hyperproperty encodings and (ii) an inductive proof sketch that covers the translation of formulas with alternating quantifiers. This will be placed immediately after the description of the translation algorithm. revision: yes

  2. Referee: [Evaluation] Evaluation section: the abstract asserts successful evaluation on state-of-the-art scenarios, yet the manuscript supplies neither quantitative performance data (e.g., runtimes, memory) nor details of the translation steps or semantic-preservation argument, leaving the feasibility claim only partially evidenced.

    Authors: We acknowledge that the evaluation section currently emphasizes feasibility through modeling examples rather than quantitative metrics. In the revision we will (a) report runtimes and memory consumption for all state-of-the-art scenarios, (b) expand the description of the translation steps with concrete examples, and (c) integrate the semantic-preservation argument described in the response to the first comment. These additions will be presented in a new subsection of the evaluation. revision: yes

Circularity Check

0 steps flagged

No significant circularity; core verification delegated to external checkers

full rationale

The paper's central procedure extends Pardinus by translating relational models to inputs for independent low-level hyperproperty model checkers. No equations or self-citations reduce the claimed semantic preservation or verification results to a fitted parameter or self-referential definition by construction. The translation is presented as a conservative extension relying on external tools, with evaluation against state-of-the-art scenarios providing independent content. This matches the default expectation of non-circularity for papers that delegate to external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on the assumption that Alloy's relational logic can be soundly mapped to hyperproperty checkers and that the mapping preserves counterexamples at the model level; no new free parameters or invented entities beyond the procedure itself are introduced.

axioms (1)
  • standard math Alloy relational models have well-defined semantics under first-order logic with relations and transitive closure
    The paper builds directly on the established semantics of Alloy and Pardinus without re-deriving them.
invented entities (1)
  • HyperPardinus no independent evidence
    purpose: New model finding procedure that extends Pardinus to interface with hyperproperty checkers
    The procedure is introduced by the paper; no independent evidence outside the described evaluation is provided.

pith-pipeline@v0.9.0 · 5508 in / 1266 out tokens · 36865 ms · 2026-05-16T22:35:14.109200+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

33 extracted references · 33 canonical work pages

  1. [1]

    Raven Beutner. 2024. Automated Software Verification of Hyperliveness. InTACAS (2) (LNCS, Vol. 14571). Springer, 196–216

    work page 2024

  2. [2]

    Raven Beutner and Bernd Finkbeiner. 2022. Prophecy variables for hyperproperty verification. In2022 IEEE 35th Computer Security Foundations Symposium (CSF). IEEE, 471–485

    work page 2022

  3. [3]

    Raven Beutner and Bernd Finkbeiner. 2022. Software Verification of Hyperproperties Beyond k-Safety. InCA V (1) (LNCS, Vol. 13371). Springer, 341–362

    work page 2022

  4. [4]

    Raven Beutner and Bernd Finkbeiner. 2023. AutoHyper: Explicit-State Model Checking for HyperLTL. InTools and Algorithms for the Construction and Analysis of Systems. Springer Nature Switzerland, Cham, 145–163

    work page 2023

  5. [5]

    Raven Beutner and Bernd Finkbeiner. 2023. Model Checking Omega-Regular Hyperproperties with AutoHyperQ. InLPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023 (EPiC Series in Computing, Vol. 94). EasyChair, 23–35. doi:10.29007/1XJT

    work page doi:10.29007/1xjt 2023

  6. [6]

    Clarke, and Yunshan Zhu

    Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. 1999. Symbolic Model Checking without BDDs. InTACAS (LNCS, Vol. 1579). Springer, 193–207

    work page 1999

  7. [7]

    Michael R Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K Micinski, Markus N Rabe, and César Sánchez. 2014. Temporal logics for hyperproperties. InPrinciples of Security and Trust: Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13,...

    work page 2014

  8. [8]

    Michael R Clarkson and Fred B Schneider. 2010. Hyperproperties.Journal of Computer Security18, 6 (2010), 1157–1210

    work page 2010

  9. [9]

    Norine Coenen, Raimund Dachselt, Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Tom Horak, Niklas Metzger, and Julian Siber. 2022. Explaining Hyperproperty Violations. InCA V (1) (LNCS, Vol. 13371). Springer, 407–429

    work page 2022

  10. [10]

    Arthur Correnson, Tobias Nießen, Bernd Finkbeiner, and Georg Weissenbacher. 2024. Finding ∀∃ Hyperbugs using Symbolic Execution.Proc. ACM Program. Lang.8, OOPSLA2 (2024), 1420–1445

    work page 2024

  11. [11]

    Thibault Dardinier, Anqi Li, and Peter Müller. 2024. Hypra: A Deductive Program Verifier for Hyper Hoare Logic.Proc. ACM Program. Lang.8, OOPSLA2, Article 316 (Oct. 2024), 30 pages. doi:10.1145/3689756

    work page doi:10.1145/3689756 2024

  12. [12]

    Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, and Henrich Lauko. 2022. From Spot 2.0 to Spot 2.10: What’s New?. InCA V (2) (LNCS, Vol. 13372). Springer, 174–187

    work page 2022

  13. [13]

    Andreas Fellner, Mitra Tabaei Befrouei, and Georg Weissenbacher. 2021. Mutation testing with hyperproperties.Softw. Syst. Model.20, 2 (2021), 405–427

    work page 2021

  14. [14]

    Bernd Finkbeiner. 2023. Logics and Algorithms for Hyperproperties.ACM SIGLOG News10, 2 (2023), 4–23. doi:10.1145/3610392.3610394

    work page doi:10.1145/3610392.3610394 2023

  15. [15]

    Bernd Finkbeiner, Christian Müller, Helmut Seidl, and Eugen Zălinescu. 2017. Verifying Security Policies in Multi-agent Workflows with Loops. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (CCS ’17). Association for Computing Machinery, New York, NY, USA, 633–645. doi:10.1145/3133956.3134080

    work page doi:10.1145/3133956.3134080 2017

  16. [16]

    Rabe, and César Sánchez

    Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. 2015. Algorithms for Model Checking HyperLTL and HyperCTL. InComputer Aided Verification. Springer International Publishing, Cham, 30–48

    work page 2015

  17. [17]

    Tom Horak, Norine Coenen, Niklas Metzger, Christopher Hahn, Tamara Flemisch, Julián Méndez, Dennis Dimov, Bernd Finkbeiner, and Raimund Dachselt. 2022. Visual Analysis of Hyperproperties for Understanding Model Checking Results.IEEE Transactions on Visualization and Computer Graphics28, 1 (2022), 357–367. doi:10.1109/TVCG.2021.3114866

    work page doi:10.1109/tvcg.2021.3114866 2022

  18. [18]

    Tzu-Han Hsu, Borzoo Bonakdarpour, and César Sánchez. 2024. HyperQB: A QBF-Based Bounded Model Checker for Hyperproperties. arXiv:2109.12989 [cs.LO] https://arxiv.org/abs/2109.12989

    work page arXiv 2024

  19. [19]

    Tzu-Han Hsu, César Sánchez, and Borzoo Bonakdarpour. 2021. Bounded Model Checking for Hyperproperties. InTools and Algorithms for the Construction and Analysis of Systems. Springer International Publishing, Cham, 94–112

    work page 2021

  20. [20]

    Tzu-Han Hsu, César Sánchez, Sarai Sheinvald, and Borzoo Bonakdarpour. 2023. Efficient Loop Conditions for Bounded Model Checking Hyperprop- erties. InTools and Algorithms for the Construction and Analysis of Systems. Springer Nature Switzerland, Cham, 66–84

    work page 2023

  21. [21]

    Shachar Itzhaky, Sharon Shoham, and Yakir Vizel. 2024. Hyperproperty Verification as CHC Satisfiability. InESOP (2) (LNCS, Vol. 14577). Springer, 212–241

    work page 2024

  22. [22]

    2006.Software abstractions: Logic, language, and analysis(revised ed.)

    Daniel Jackson. 2006.Software abstractions: Logic, language, and analysis(revised ed.). MIT Press

    work page 2006

  23. [23]

    Daniel Jackson. 2019. Alloy: A language and tool for exploring software designs.Commun. ACM62, 9 (2019), 66–76

    work page 2019

  24. [24]

    Jure Kukovec, Thanh-Hai Tran, and Igor Konnov. 2020. Extracting symbolic transitions from TLA+ specifications.Science of Computer Programming 187 (2020), 102361. doi:10.1016/j.scico.2019.102361 Hyper model checking for high-level relational models 23

    work page doi:10.1016/j.scico.2019.102361 2020

  25. [25]

    Tomas Kulik, Brijesh Dongol, Peter Gorm Larsen, Hugo Daniel Macedo, Steve Schneider, Peter W. V. Tran-Jørgensen, and James Woodcock. 2022. A Survey of Practical Formal Methods for Security.Form. Asp. Comput.34, 1, Article 5 (2022), 39 pages. doi:10.1145/3522582

    work page doi:10.1145/3522582 2022

  26. [26]

    Leslie Lamport. 1994. The Temporal Logic of Actions.ACM Trans. Program. Lang. Syst.16, 3 (1994), 872–923

    work page 1994

  27. [27]

    Schneider

    Leslie Lamport and Fred B. Schneider. 2021. Verifying Hyperproperties With TLA. InCSF. IEEE, 1–16

    work page 2021

  28. [28]

    Nuno Macedo, Julien Brunel, David Chemouil, and Alcino Cunha. 2022. Pardinus: A temporal relational model finder.Journal of Automated Reasoning66, 4 (2022), 861–904

    work page 2022

  29. [29]

    Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha, and Denis Kuperberg. 2016. Lightweight specification and analysis of dynamic systems with rich configurations. InSIGSOFT FSE. ACM, 373–383

    work page 2016

  30. [30]

    McMillan

    Kenneth L. McMillan. 1993.Symbolic model checking. Kluwer

    work page 1993

  31. [31]

    Christian Müller, Helmut Seidl, and Eugen Zălinescu. 2018. Inductive Invariants for Noninterference in Multi-agent Workflows. In2018 IEEE 31st Computer Security Foundations Symposium (CSF). 247–261

    work page 2018

  32. [32]

    Andrei Popescu, Peter Lammich, and Ping Hou. 2021. CoCon: A conference management system with formally verified document confidentiality. Journal of Automated Reasoning65 (2021), 321–356

    work page 2021

  33. [33]

    Emina Torlak and Daniel Jackson. 2007. Kodkod: A relational model finder. InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 632–647

    work page 2007