Pith. sign in

REVIEW 3 major objections 4 minor 34 references

Finding $\forall\exists$ Hyperbugs using Symbolic Execution

T0 review · 3 major / 4 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A symbolic execution method can automatically detect violations of ∀∃ hyperproperties by pairing a universal trace with a proof that no matching trace exists.

desk verdict Useful approach and honest evaluation, but the finite-observability condition is vacuously satisfiable and the termination/completeness theorems as stated are false. read the letter →

arxiv 2501.07918 v1 pith:PKNMCZTQ submitted 2025-01-14 cs.PL

Arthur Correnson , Tobias Niessen , Bernd Finkbeiner , Georg Weissenbacher This is my paper · ORCID
classification cs.PL MSC 68Q60
keywords hyperpropertiessymbolicexecution∀∃quantificationboundedsemanticsfiniteobservabilitybugfindingrefinementgeneralizednon-interference
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper presents the first symbolic execution method that automatically checks whether one or more programs satisfy a given ∀∃ hyperproperty—a property that requires every execution trace to have some related partner trace. Such properties are notoriously hard to refute because disproving them requires both finding a troublesome trace and proving that no matching trace exists. The paper's key contribution is a combination of a bounded semantics for a logic called OHyperLTLsafe with a symbolic encoding of that semantics, so that bug-finding can be reduced to checking satisfiability of formulas. On benchmarks drawn from refinement, generalized non-interference, and delimited information release, the prototype finds counterexamples in under a second without requiring loop invariants. If the paper is right, this paves the way for fully automatic testing of a broad class of relational properties in software systems.

What carries the argument

The central device is the bounded semantics of OHyperLTLsafe (Definition 3.4) together with its symbolic encoding (Definition 4.6). OHyperLTLsafe is a temporal logic with trace quantifiers and observation points, restricted to invariant formulas □φ. The bounded semantics evaluates formulas on finite prefixes of exactly k observations; the upper-bounded semantics |=≤k checks all k′≤k and is monotone. For infinitely observable programs, a counterexample at bound k implies a real violation (Theorem 3.10). Algorithm 3 then iterates over symbolic universal traces one by one; for each it builds a formula C2 asserting that no existentially quantified trace matches, and an SMT satisfiability check decides whether that pair of conditions is realizable. A model of the formula yields a concrete universal trace and an explanation of why no partner exists. Relative completeness relies on finite observability (Definition 4.13): for every k, all traces with k observations have a prefix of bounded length containing them.

What would settle it

Take a finitely observable program known to violate a ∀∃ property, run the tool in its default automatic mode with increasing bound n, and check whether it eventually reports a violation; failure to do so for any n would contradict the relative-completeness theorem. Conversely, if the tool ever reports a violation on a non-finitely-observable program, the soundness boundary stated in the paper would need revision.

Watch

Extended reading notes

Core claim

The paper claims that violations of ∀∃ hyperproperties can be detected by combining two symbolic execution engines: one that enumerates candidates for the universally quantified trace, and one that encodes the absence of any matching trace. The detection is sound (reported bugs are real violations) and relatively complete for a class of programs called finitely observable, meaning that if the bounded semantics fails at some depth, the unbounded semantics also fails. The paper introduces OHyperLTLsafe, a fragment of OHyperLTL restricted to invariant properties, with observation points to synchronize traces, and gives it a bounded semantics that agrees with the standard infinite-trace semantics for infinitely observable programs while also handling terminating programs. The prototype implementation finds counterexamples for refinement, generalized non-interference, and delimited information release benchmarks, often in fractions of a second, without needing user-supplied loop invariants.

Load-bearing premise

For the algorithm to terminate and be complete, every program with a given number of observation points must have all its traces reaching those points within a fixed number of computation steps; programs that can loop arbitrarily long before being observed can make it diverge.

Editorial extensions

If this is right

  • If the central claim is correct, fully automatic bug-finding for ∀∃ hyperproperties becomes possible for infinite-state reactive systems, not just finite-state models.
  • The produced counterexample—a concrete universal trace plus an encoding showing no partner exists—provides a human-checkable explanation of the violation.
  • Properties with multiple universal or existential quantifiers can be handled by an asynchronous product construction, so the method extends beyond single ∀∃ pairs.
  • Because the algorithm does not need loop invariants, it complements deductive verifiers that require annotations and can find bugs in programs that are hard to verify.
  • The lazy per-trace query structure is naturally parallelizable, which could scale the approach to larger state spaces.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same trace-witness structure could be adapted to probabilistic or timed hyperproperties by replacing SMT satisfiability with model counting or a suitable solver for the underlying theory.
  • The per-universal-trace queries are independent, so a parallel implementation could achieve near-linear speedup, making deeper unwinding depths practical.
  • The finite-observability restriction might be relaxed by combining this symbolic execution with invariant synthesis for loops that delay observation, potentially covering benchmarks like loop-nonrefinement that currently cause divergence.
  • The concrete universal trace plus impossibility proof could be turned into a regression test oracle for future versions of the analyzed program.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper introduces OHyperLTLsafe, a fragment of OHyperLTL for expressing ∀∃ hyperproperties such as refinement and generalized non-interference, together with a bounded semantics |=≤k and a symbolic-execution-based method for detecting violations. It proves that for infinitely observable specifications, unbounded satisfaction implies bounded satisfaction, develops a symbolic encoding of the bounded semantics, and presents two bug-finding algorithms (a naive SMT-based one and a lazy counterexample-producing one). The lazy algorithm is implemented in a prototype and evaluated on benchmarks from ORHLE, on new reactive benchmarks, and on a parameterized case study against HyperQB and HyHorn.

Significance. If the results held as stated, this would be a valuable contribution: it is the first fully automatic symbolic-execution approach to finding violations of ∀∃ hyperproperties in infinite-state software, it produces concrete universal traces plus an explanation of why no matching existential trace exists, and the evaluation is reproducible (the artifact is linked) and shows strong performance on a range of benchmarks. The bounded semantics and the symbolic encoding are useful ideas in their own right. However, the central relative-completeness theorem for the symbolic interpreter is false as stated, and the paper overstates the agreement between the bounded and unbounded semantics. These issues are fixable, but they currently undermine the claimed characterization of when the algorithm terminates and succeeds.

major comments (3)
  1. [Definition 4.13 / Theorem 4.14] The finite-observability condition is vacuous for programs whose traces can avoid observation points forever, so Theorem 4.14 is false as stated. Let G have L={ℓ0,ℓ1}, E={(ℓ0,ℓ0)}, initial location ℓ0, observation set O={ℓ1}, and a trivial guard/effect on the self-loop. For every k≥1 there is no finite trace τ with |τ|_O=k, so the implication in Definition 4.13 is vacuously true and Observable^k_O(G) holds. Yet Observe(G,O,k) starts at ℓ0 with zero observations, calls Extend on the self-loop, and never terminates because no trace ever reaches k observations. Thus the algorithm diverges on an FO=Yes input, contradicting Theorem 4.14 and, through Theorem 4.19, the claimed relative completeness of Algorithm 3. The definition needs an additional non-vacuity condition, e.g., a uniform bound on the position of the k-th observation for every trace that has one, plus a condition ruling out infinite exploration of traces with fewer than k observations; the claim in Section 5.1 that the circumstances of success are characterized precisely is therefore too strong.
  2. [Abstract and Section 3] The paper claims that the bounded semantics 'agrees' with the unbounded semantics, but only |=ω ψ ⇒ |=≤k ψ is proved. The converse fails even for infinitely observable specifications: a violation that first appears after k observations is invisible to |=≤k. This overstatement appears in the abstract, in the introduction, and in the sentence before Theorem 3.10 ('it is easy to see that |=≤k still agrees with |=ω'). The theorem itself is sound and is the direction needed for bug finding; the text should explicitly state the one-way nature of the result and avoid the term 'agrees' without qualification.
  3. [Section 4.1, Theorem 4.7] The theorem states that for any OHyperLTLsafe formula ψ, JψK^k_∅ is a closed first-order formula and |=k ψ iff |=T JψK^k_∅. This is not well-defined when SymTraces^k_O(G) is infinite, as in the factorial example of Section 4.2, because Definition 4.6 then produces an infinite conjunction or disjunction, which is not a formula of the first-order theory T. The theorem should be restricted to k-encodable specifications, or the semantics of the encoding must be defined for infinitary formulas; as written, the scope of the encoding result is overstated. Theorem 4.10 already provides the needed finiteness condition.
minor comments (4)
  1. [Theorem 3.7 proof sketch] In the existential case, the goal should be 'Π′ |=k ψ' and the hypothesis should be 'Π |=ω ψ'; the current text writes ψ′ in both places.
  2. [Theorem 4.4 heading] The heading reads 'Eqivalence' and should be 'Equivalence'.
  3. [Section 4.2, first paragraph] The phrase 'the set of symbolic traces of length exactly k' should be qualified as concrete symbolic traces of concrete length k, to avoid confusion with SymTraces^k_O(G), which is the observed-length-k set and may be infinite.
  4. [Section 1 and Section 7] The phrase 'checks automatically whether ... satisfy' overstates the method, which finds violations of the bounded semantics but does not prove satisfaction; 'detect violations of' would be more accurate.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity found: the bounded semantics, symbolic encoding, and bug-finding algorithms are derived from explicit definitions, and the few self-citations are contextual rather than load-bearing.

full rationale

The derivation chain is self-contained. Section 3 defines OHyperLTLsafe with infinite, bounded, and upper-bounded semantics from program graphs; Theorem 3.7 uses the infinitely-observable assumption to show that satisfiability in the unbounded semantics implies satisfiability in the bounded semantics, and the contrapositive is what bug-finding uses. Definition 4.6 gives a symbolic encoding that syntactically mirrors the semantics, and Theorem 4.7 proves the equivalence by induction over formulas using the concrete/symbolic trace correspondence. That correspondence (Theorem 4.4) is attributed both to [17] and to [14]; although [14] is by one of the present authors, the independent support from [17] and the standard proof structure mean the self-citation is not load-bearing. Algorithms 2 and 3 are soundness and completeness statements about those encodings; the counterexample formulas C1 and C2 are directly the path condition and the negated existential-witness encoding, not a fitted or renamed quantity. The evaluation is against external tools (ORHLE, HyperQB, HyHorn) and independent benchmarks. The paper's disclosed failure on loop-nonrefinement (Table 1: FO=No, runtime ∞) is a completeness boundary for the finite-observability condition, not a circular step. No parameter is fitted to a target result, no uniqueness theorem is imported from the authors' prior work, and no ansatz is smuggled in via citation.

Assumptions & free parameters 1 free parameters · 4 assumptions · 0 invented entities

The central claim rests on the finite observability condition (Definition 4.13), the correctness of symbolic execution from prior work, and the decidable satisfiability of the generated formulas. The only user-chosen control parameter is the observation bound k/n. No data-fitted constants, no hidden entities, and no target results assumed as input.

free parameters (1)
  • Observation bound k (maximum n)
    Algorithms 2 and 3 iterate k = 1..n. Bugs whose counterexample requires more than n observation points are not found, so completeness is relative to this user-supplied bound.
assumptions (4)
  • domain assumption Symbolic execution soundly and completely represents concrete trace sets: γ(SymTraces*(G)) = Traces*(G), as established in [17,14].
    The symbolic encoding in Definition 4.6 and Theorem 4.7 depend on this prior result, which the paper cites but does not re-prove.
  • domain assumption The underlying first-order theory T is decidable (or the SMT solver Yices decides the generated formulas) and the Sat procedure is sound.
    Algorithm 1 and the relative completeness theorems (4.14, 4.17, 4.19) explicitly assume a decidable theory T and call a Sat procedure.
  • domain assumption Programs are modeled as finite program graphs with a fixed initial memory, finite locations and edges, guarded assignments, and nondeterministic inputs.
    All definitions, the symbolic interpreter, and the product construction operate on this model; the prototype restricts to a structured imperative language with observe instructions.
  • domain assumption For each analyzed bound k, every quantified program is (k,O)-observable in the sense of Definition 4.13, so Observe terminates and returns SymTraces^k.
    This is the hypothesis of Theorem 4.14 and the relative completeness theorems; the evaluation's loop-nonrefinement benchmark violates it and the tool diverges.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Finding $\forall\exists$ Hyperbugs using Symbolic Execution." pith.science (2026). https://pith.science/paper/PKNMCZTQ

@misc{pith2026250107918,
  author       = {Pith},
  title        = {Pith review of: Finding $\forall\exists$ Hyperbugs using Symbolic Execution},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PKNMCZTQ}},
  note         = {Machine review of arXiv:2501.07918}
}
abstract

Many important hyperproperties, such as refinement and generalized non-interference, fall into the class of $\forall\exists$ hyperproperties and require, for each execution trace of a system, the existence of another trace relating to the first one in a certain way. The alternation of quantifiers renders $\forall\exists$ hyperproperties extremely difficult to verify, or even just to test. Indeed, contrary to trace properties, where it suffices to find a single counterexample trace, refuting a $\forall\exists$ hyperproperty requires not only to find a trace, but also a proof that no second trace satisfies the specified relation with the first trace. As a consequence, automated testing of $\forall\exists$ hyperproperties falls out of the scope of existing automated testing tools. In this paper, we present a fully automated approach to detect violations of $\forall\exists$ hyperproperties in software systems. Our approach extends bug-finding techniques based on symbolic execution with support for trace quantification. We provide a prototype implementation of our approach, and demonstrate its effectiveness on a set of challenging examples.

Figures

Figures reproduced from arXiv: 2501.07918 by the authors.

Figure 1
Figure 1. Two versions of a simple voting protocol with a bug underlined [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. A simple program and a possible translation as a program graph [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. A simple program, and a specification of GNI in OHyperLTL [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Two programs, and a specification of refinement in OHyperLTL [PITH_FULL_IMAGE:figures/full_fig_p007_4.png]
Figure 5
Figure 5. Figure 5: Median runtimes of our approach, HyperQB [ [PITH_FULL_IMAGE:figures/full_fig_p021_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

34 extracted references · 10 canonical work pages

  1. [1]

    Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2011. Relational Verification Using Product Programs. In FM 2011: Formal Methods (Lecture Notes in Computer Science) , Michael Butler and Wolfram Schulte (Eds.). Springer, Berlin, Heidelberg, 200–214. https://doi.org/10.1007/978-3-642-21437-0_17

    doi:10.1007/978-3-642-21437-0_17 2011

  2. [2]

    Barthe, P.R

    G. Barthe, P.R. D’Argenio, and T. Rezk. 2004. Secure information flow by self-composition. In Proceedings. 17th IEEE Computer Security Foundations Workshop, 2004. IEEE, Pacific Grove, CA, USA, 100–114. https://doi.org/10.1109/CSFW. 2004.1310735

    arXiv 2004

  3. [4]

    Jon Barwise. 1977. An Introduction to First-Order Logic. In Handook of Mathematical Logic , Jon Barwise (Ed.). Studies in Logic and the Foundations of Mathematics, Vol. 90. Elsevier, 5–46

    work page 1977

  4. [5]

    Raven Beutner. 2024. Automated Software Verification of Hyperliveness. InTools and Algorithms for the Construction and Analysis of Systems, Bernd Finkbeiner and Laura Kovács (Eds.). Springer, Cham, 196–216. https://doi.org/10.1007/978- 3-031-57249-4_10

    doi:10.1007/978- 2024

  5. [6]

    Raven Beutner and Bernd Finkbeiner. 2022. Prophecy Variables for Hyperproperty Verification. In 2022 IEEE 35th Computer Security Foundations Symposium (CSF) . 471–485. https://doi.org/10.1109/CSF54842.2022.9919658

    arXiv 2022

  6. [7]

    Raven Beutner and Bernd Finkbeiner. 2022. Software Verification of Hyperproperties Beyond k-Safety. In Computer Aided Verification (Lecture Notes in Computer Science) , Sharon Shoham and Yakir Vizel (Eds.). Springer International Publishing, Cham, 341–362. https://doi.org/10.1007/978-3-031-13185-1_17

    doi:10.1007/978-3-031-13185-1_17 2022

  7. [8]

    Raven Beutner and Bernd Finkbeiner. 2023. AutoHyper: Explicit-State Model Checking for HyperLTL. In Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science) , Sriram Sankaranarayanan and Natasha Sharygina (Eds.). Springer, Cham, 145–163. https://doi.org/10.1007/978-3-031-30823-9_8

    doi:10.1007/978-3-031-30823-9_8 2023

  8. [9]

    Clarke, Ofer Strichman, and Yunshan Zhu

    Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, and Yunshan Zhu. 2003. Bounded model checking. Adv. Comput. 58 (2003), 117–148. https://doi.org/10.1016/S0065-2458(03)58003-2

    doi:10.1016/s0065-2458(03)58003-2 2003

Show all 34 references
  1. [10]

    Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX conference on Operating systems design and implementation (OSDI’08). USENIX Association, USA,...

    2008

  2. [11]

    Swarat Chaudhuri, Sumit Gulwani, and Roberto Lublinerman. 2012. Continuity and robustness of programs. Commun. ACM 55, 8 (2012), 107–115. https://doi.org/10.1145/2240236.2240262

    2012

  3. [12]

    Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K

    Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez

  4. [13]

    Clarkson and Fred B

    Michael R. Clarkson and Fred B. Schneider. 2010. Hyperproperties. Journal of Computer Security 18, 6 (Sept. 2010), 1157–1210. https://doi.org/10.3233/JCS-2009-0393

    2010 doi

  5. [14]

    Arthur Correnson and Dominic Steinhöfel. 2023. Engineering a Formally Verified Automated Bug Finder. InProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (<conf-loc>, <city>San Francisco</city>, <...

    2023

  6. [15]

    Lesly-Ann Daniel, Sébastien Bardin, and Tamara Rezk. 2021. Hunting the Haunter - Efficient Relational Symbolic Execution for Spectre with Haunted RelSE. Proceedings 2021 Network and Distributed System Security Symposium (2021). https://doi.org/10.14722/ndss.2021.24286

    2021

  7. [16]

    Lesly-Ann Daniel, Sébastien Bardin, and Tamara Rezk. 2023. Binsec/Rel: Symbolic Binary Analyzer for Security with Applications to Constant-Time and Secret-Erasure. ACM Trans. Priv. Secur. 26, 2, Article 11 (April 2023), 42 pages. https://doi.org/10.1145/3563037

    2023 doi

  8. [17]

    de Boer and Marcello Bonsangue

    Frank S. de Boer and Marcello Bonsangue. 2019. On the Nature of Symbolic Execution. In Formal Methods – The Next 30 Years (Lecture Notes in Computer Science) , Maurice H. ter Beek, Annabelle McIver, and José N. Oliveira (Eds.). Springer International Publishing, Cham, 64–80. h...

    2019 doi

  9. [18]

    Zhang, and Benjamin Delaware

    Robert Dickerson, Qianchuan Ye, Michael K. Zhang, and Benjamin Delaware. 2022. RHLE: Modular Deductive Verification of Relational∀∃ Properties. In Programming Languages and Systems (Lecture Notes in Computer Science) , Ilya Sergey (Ed.). Springer, Cham, 67–87. https://doi.org/...

    2022 doi

  10. [19]

    Bruno Dutertre. 2014. Yices 2.2. In Computer Aided Verification (Lecture Notes in Computer Science) , Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham, 737–744. https://doi.org/10.1007/978-3-319-08867- 9_49

    2014 doi

  11. [20]

    Azadeh Farzan and Anthony Vandikas. 2019. Automated Hypersafety Verification. In Computer Aided Verification (Lecture Notes in Computer Science) , Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing, Cham, 200–218. https://doi.org/10.1007/978-3-030-25540-4_11

    2019 doi

  12. [21]

    Azadeh Farzan and Anthony Vandikas. 2019. Reductions for safety proofs. Proc. ACM Program. Lang. 4, POPL, Article 13 (Dec. 2019), 28 pages. https://doi.org/10.1145/3371081

    2019 doi

  13. [22]

    Patrice Godefroid. 2005. The soundness of bugs is what matters (position statement). InBUGS’2005 (PLDI’2005 Workshop on the Evaluation of Software Defect Detection Tools)

    2005

  14. [23]

    Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: directed automated random testing. ACM SIGPLAN Notices 40, 6 (June 2005), 213–223. https://doi.org/10.1145/1064978.1065036

    2005

  15. [24]

    Tzu-Han Hsu, César Sánchez, and Borzoo Bonakdarpour. 2021. Bounded Model Checking for Hyperproperties. In Tools and Algorithms for the Construction and Analysis of Systems , Jan Friso Groote and Kim Guldstrand Larsen (Eds.). Vol. 12651. Springer International Publishing, Cham,...

    2021 doi

  16. [25]

    Shachar Itzhaky, Sharon Shoham, and Yakir Vizel. 2024. Hyperproperty Verification as CHC Satisfiability. In Program- ming Languages and Systems , Stephanie Weirich (Ed.). Springer, Cham, 212–241. https://doi.org/10.1007/978-3-031- 57267-8_9

    2024 doi

  17. [26]

    Ranjit Jhala, Andreas Podelski, and Andrey Rybalchenko. 2018. Predicate Abstraction for Program Verification: Safety and Termination. Handbook of Model Checking (2018), 447–491. https://doi.org/10.1007/978-3-319-10575-8_15

    2018 doi

  18. [27]

    James C. King. 1976. Symbolic execution and program testing. Commun. ACM 19, 7 (July 1976), 385–394. https: //doi.org/10.1145/360248.360252

    1976

  19. [28]

    Manes, HyungSeok Han, Choongwoo Han, Sang Kil Cha, Manuel Egele, Edward J

    Valentin J.M. Manes, HyungSeok Han, Choongwoo Han, Sang Kil Cha, Manuel Egele, Edward J. Schwartz, and Maverick Woo. 2021. The Art, Science, and Engineering of Fuzzing: A Survey. IEEE Transactions on Software Engineering 47, 11 (Nov. 2021), 2312–2331. https://doi.org/10.1109/T...

    2021

  20. [29]

    McCullough

    D. McCullough. 1988. Noninterference and the composability of security properties. InProceedings. 1988 IEEE Symposium on Security and Privacy . IEEE Comput. Soc. Press, Oakland, CA, USA, 177–186. https://doi.org/10.1109/SECPRI.1988. 8110

    1988 doi

  21. [30]

    J. McLean. 1994. A general theory of composition for trace sets closed under selective interleaving functions. In Proceedings of 1994 IEEE Computer Society Symposium on Research in Security and Privacy . 79–93. https://doi.org/10. 1109/RISP.1994.296590 Proc. ACM Program. Lang....

    1994

  22. [31]

    Andrei Sabelfeld and Andrew C. Myers. 2004. A Model for Delimited Information Release. In Software Security - Theories and Systems (Lecture Notes in Computer Science) , Kokichi Futatsugi, Fumio Mizoguchi, and Naoki Yonezaki (Eds.). Springer, Berlin, Heidelberg, 174–191. https:...

    2004 doi

  23. [32]

    Koushik Sen, Darko Marinov, and Gul Agha. 2005. CUTE: a concolic unit testing engine for C. ACM SIGSOFT Software Engineering Notes 30, 5 (Sept. 2005), 263–272. https://doi.org/10.1145/1095430.1081750

    2005

  24. [33]

    Ron Shemer, Arie Gurfinkel, Sharon Shoham, and Yakir Vizel. 2019. Property Directed Self Composition. In Computer Aided Verification (Lecture Notes in Computer Science) , Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing, Cham, 161–179. https://doi.org/1...

    2019 doi

  25. [34]

    Weikun Yang, Yakir Vizel, Pramod Subramanyan, Aarti Gupta, and Sharad Malik. 2018. Lazy Self-composition for Security Verification. In Computer Aided Verification (Lecture Notes in Computer Science) , Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publish...

    2018 doi

  26. [2014]

    InPrinciples of Security and Trust (Lecture Notes in Computer Science), Martín Abadi and Steve Kremer (Eds.)

    Temporal Logics for Hyperproperties. InPrinciples of Security and Trust (Lecture Notes in Computer Science), Martín Abadi and Steve Kremer (Eds.). Springer, Berlin, Heidelberg, 265–284. https://doi.org/10.1007/978-3-642-54792-8_15

    doi

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.