Pith. sign in

REVIEW 3 major objections 5 minor 16 references

Checkification: A Practical Approach for Testing Static Analysis Truths

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

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

Pith's one-line read Run the analyzer's claims at runtime to find its bugs.

desk verdict Honest, useful engineering: applies a known cross-checking idea to Ciao and finds 21 real bugs; the main weaknesses are missing artifacts and an over-broad framing. read the letter →

arxiv 2501.12093 v3 pith:JZCHC6YT submitted 2025-01-21 cs.SE cs.PL

Daniela Ferreiro , Ignacio Casso , Jose F. Morales , Pedro López-García , Manuel V. Hermenegildo This is my paper · ORCID
classification cs.SEcs.PL
keywords staticanalysistestingruntimeassertionsabstractinterpretationassertion-basedrandomtestgenerationlogicprogrammingCiaoPPsoundnessvalidation
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

Checkification is a way to test an abstract-interpretation static analyzer by checking its own conclusions at run time. The paper claims that if analyzer-emitted assertions are re-labeled from proven (`true`) to unproven (`check`), instrumented as runtime tests, and exercised with random test inputs that satisfy the assertions' preconditions, then any violation proves that the analyzer's inferred property is false for a concrete execution. Because the method only reuses components that already exist in the paper's assertion-based framework, the testing harness is mostly glue code; over a benchmark suite plus real tools, it found 21 diverse bugs across domains, fixpoint algorithms, runtime-check instrumentation, and third-party library integration. A clean run gives practical confidence but not proof of soundness, since test coverage is finite.

What carries the argument

The mechanism is the assertion-status flip: the analyzer's output `true pred ...` and `true(...)` assertions are rewritten as `check` assertions, which the existing runtime-checking framework compiles into executable tests executed at the corresponding program points. The correctness argument is an under-approximation containment check: the collecting semantics $S_P$ of a program is contained in the analyzer's over-approximation $S^+_P$; since $S_P$ is undecidable, checkification substitutes a set of concrete runs $S^-_P$ obtained by random test-case generation and verifies $S^-_P \subseteq S^+_P$ pointwise. The paper's Algorithm 1 orchestrates this loop, non-deterministically choosing programs and domains until an error, timeout, or coverage limit is reached, and reports `Error(input, l)` with the failing input and program-point location for shrinking and diagnosis.

What would settle it

Take an abstract domain known to be sound on a small benchmark, instrument it with checkification, and run a large set of random tests: a single reported violation must mean the runtime check is wrong, which would overturn the method's automatic attribution of failures to the analyzer. Conversely, seed a deliberate error into a transfer function of a domain and confirm that checkification reports it at the expected program point; if the seeded error goes unnoticed, the method's coverage is too weak to be relied on.

Watch

Extended reading notes

Core claim

The central discovery is that a static analyzer can be tested almost for free when its output format is the same assertion language its runtime system understands. The paper's procedure, AnaTest(P,D), analyzes a program P with domain D, replaces the status of every `true` assertion in the annotated output with `check`, instruments those checks, and runs random test cases generated from precondition properties. A runtime error at a program point means the concrete execution reached a state outside the analyzer's over-approximation, so the analyzer is unsound at that point—or, alternatively, the runtime-checking component is wrong. The paper demonstrates the method on CiaoPP across a large number of abstract domains, finding bugs in five classes: abstract domain implementations, fixpoint algorithms, semantic inconsistencies between framework components, runtime-check instrumentation, and third-party library or solver integration. Most detected bugs were new and have since been fixed or confirmed, and the approach also detects wrong user-supplied `trust` assertions, since a sound analyzer can still produce unsound results when it trusts an untrue assumption.

Load-bearing premise

The method assumes the runtime-checking mechanism is faithful enough that a failed check means the analyzer's inferred property is actually false for that run; the paper itself documents cases where the runtime checker, not the analyzer, was the source of the error.

Editorial extensions

If this is right

  • New abstract domains become testable as soon as their native properties have runnable definitions, so checkification lowers the barrier to integrating experimental analyses.
  • Because failures can be traced to a program point and shrunk to small inputs, developers can locate the faulty transfer function or fixpoint step without building a separate oracle.
  • The same harness tests the whole framework, not just domains: it caught missing built-in abstract descriptions, inconsistent property semantics, and bugs in run-time checking itself, so every flagged error improves the system even when the analyzer was right.
  • A clean run over many benchmarks and domains yields practical, not formal, confidence in soundness, complementing ongoing formal verification of the top-down solver's algorithm.
  • The method extends to computational properties such as determinacy and (non)failure, and the paper argues cost and termination are reachable with specialized checks like timeout-based nontermination detection.

Reading between the lines

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

  • If another analyzer could emit its results in an executable assertion language, the same status-flip procedure would apply; the main porting cost is a runnable property language plus a generator for precondition states, not a new testing theory.
  • The method's reach is bounded by the coverage of generated test cases, so coupling the random generator with coverage-guided search or concolic execution of the check-instrumented program could expose assertion violations that random inputs miss.
  • Because a violation indicts either the analyzer or the checker, running two independent analyzers against the same runtime assertions could localize faults without assuming either side is correct, a mutual-validation variant the paper does not explore.
  • Applying checkification to a hand-written `trust` assertion that is intentionally wrong suggests a general use: validating user-supplied specifications and custom transfer functions before they are relied on in production.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. This paper presents checkification, a technique for testing the CiaoPP abstract-interpretation-based static analyzer. The method rewrites the analyzer's inferred assertions (status true) to check assertions, compiles them into run-time checks, and exercises the transformed programs with randomly generated or user-provided test cases. The paper argues that a run-time violation of an inferred assertion shows that the analyzer's over-approximation is contradicted by a concrete execution, thus revealing a bug in the analyzer or in some other framework component. The technique is evaluated on a suite of classic benchmarks and several real systems across many abstract domains, reporting 21 categorized bugs (Table 7), most of which are said to have been fixed or confirmed during the study. The central claimed advantage is simplicity: the approach reuses the existing Ciao assertion framework, run-time checking, test generation, and unit-test components with little glue code.

Significance. If the central claim is read as 'checkification is a lightweight differential-testing technique that reliably discovers inconsistencies between static analysis results and the run-time semantics of assertions,' then this is a solid and useful contribution. The construction in Algorithm 1 is genuinely simple, the evaluation spans a wide range of abstract domains and realistic programs, and the Section 4.3 case studies show that the technique surfaces real defects in a mature analyzer, including subtle issues such as mshare/1 variable-ordering sensitivity (Bug #3) and the interaction between clique/1 and mshare/1 (Bug #8). The discovery that several defects reside in the run-time checking framework itself is a valuable and non-circular result: dynamic execution is an independent check against the analyzer's output. However, the stronger claim that a run-time violation automatically identifies an analyzer error is not supported by the paper's own evidence, because several violations originated in the very run-time checking base on which the method relies. The absence of a reproducibility artifact also limits independent verification of the empirical claims.

major comments (3)
  1. [Section 1 and Algorithm 1, with Table 7] The central inference from a run-time check failure to an analyzer defect is a trust assumption, not a consequence of the method. Section 1 states that 'if any assertion violation is reported, assuming that the run-time checks are correct, it means that the assertion was incorrectly inferred by the analyzer,' and Algorithm 1 returns Error(input, l) whenever p(input) produces a run-time error. This inference is load-bearing and is contradicted by the paper's own results: Table 7 lists Bugs #3, #8, #9, #16, and #18 as Class IV (run-time check instrumentation) defects and Bug #7 as a Class III (semantic inconsistency) defect. A violation caused by a checker-side defect is observationally identical, at the point Algorithm 1 fires, to one caused by an analyzer defect; only manual root-cause analysis (Section 4.3) separates them. The statement that 'typically run-time checking is simpler than inference' is not a correctness argument, and the distribution in Table 7 suggests such failures are not rare. Please reframe the main claim as detecting disagreements between static and dynamic assertion semantics, or add a mechanism that validates the run-time checking base before attributing failures to the analyzer.
  2. [Section 3.3, with Bugs #7 and #16] The correctness argument in Section 3.1 requires that the run-time check for a property be a faithful implementation of the same property that the analyzer over-approximates, but Section 3.3 requires only that some run-time check 'be available for those properties.' The paper's own evidence shows that the static and dynamic semantics can diverge: Bug #7 is an inconsistency between the analyzer semantics and the run-time semantics of linear/1, and Bug #16 is an incorrect run-time definition of constraint/1. Please make the semantic-equivalence requirement explicit, state how the framework enforces or tests it, and discuss how the results in Tables 3-6 change when only analyzer-side defect classes (I and II) are counted as analyzer bugs.
  3. [Section 4.1-4.3 and Table 7] The empirical claims rest on the manual classification in Table 7 and on the statement that most bugs have been fixed or confirmed, but the paper provides no artifact, no bug-tracker identifiers, no exact CiaoPP commit hashes, and no minimized reproduction scripts beyond the distilled examples in Section 4.3. Since the bug classification is a post-hoc manual interpretation rather than an output of Algorithm 1, an independent reader cannot verify that a given failed check corresponds to the claimed root cause. Please make the tool, benchmark suite, exact software versions, and generated checkified programs available, or explicitly limit the paper's claims to the reported manual case studies.
minor comments (5)
  1. [Section 3.1] The relation SP⊂P S+P is used before it is defined; please define the approximation order on collecting semantics explicitly.
  2. [Section 4.2] The statement 'No bugs were found for the most mature domains' is reported without giving the number of generated test cases or any coverage metric; the observation is meaningful only relative to how much of the execution space was exercised.
  3. [Section 3.3] The proposed run-time approximation of termination by detecting repeated identical calls or using timeouts is only a heuristic warning mechanism; please state clearly that such checks cannot provide the same evidential weight as the property checks used elsewhere in the paper.
  4. [Table 7] The Status column separates 'new' from 'known' bugs, but no supporting links or dates are given for the 'known' entries; adding references to the relevant issue trackers would strengthen the reproducibility of the reported bug table.
  5. [Section 1 and Abstract] The title and abstract use 'static analysis truths' in a stronger sense than the method's actual guarantee; consider aligning the terminology with 'inconsistency detection between static and dynamic assertion semantics' to avoid overstating the automated part of the diagnostic process.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the runtime execution is an independent oracle for the analyzer's inferred assertions, and the paper's own reporting of checker-side bugs is a trusted-base caveat, not a circular derivation.

full rationale

The derivation chain is not circular. The paper's core inference, formalized in Section 3.1, is that a static analyzer computes an over-approximation S+_P of the collecting semantics S_P; if a concrete execution (an under-approximation S−_P) reaches a state not contained in S+_P, then S_P is not contained in S+_P, so the analyzer's result is incorrect. This implication is valid by the definition of over-approximation and does not presuppose the analyzer's correctness. The dynamic execution and the run-time checks are an independent oracle: they test whether the analyzer's output holds on actual runs, rather than being fitted to that output. The paper explicitly acknowledges that a violation can also be caused by bugs in the run-time checking framework itself (Section 4.3, Table 7, Classes III and IV, e.g., Bugs #3, #8, #16), which weakens the attribution to 'analyzer bug' but is a soundness or trusted-base concern, not circularity: the method still discovers a genuine inconsistency between static and dynamic semantics, and the root-cause classification is manual. The framework components are cited from prior work, including by the authors, but no load-bearing step reduces to an unverified self-citation or imposes a unique conclusion by fiat; moreover, the paper credits prior non-self work (Wu et al. 2013) for the underlying idea of checking inferred properties dynamically and positions its contribution as framework reuse and simplicity. No equation or algorithm output is equivalent to its input by construction, and no fitted parameter is renamed as a prediction. Therefore the appropriate finding is no significant circularity.

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

The method builds on standard abstract interpretation and on the existing Ciao assertion framework. No fitted parameters are used, and the paper introduces no new entities. The key assumptions are the reliability of the runtime-checking and test-generation components, both of which are fallible and indeed are shown to contain bugs.

assumptions (4)
  • domain assumption The static analyzer computes an over-approximation of the collecting semantics.
    Invoked in Section 3.1 to justify that a concrete violation implies unsoundness.
  • domain assumption The runtime assertion checking mechanism is correct, i.e., a failing check means the assertion does not hold for that execution.
    This is the trusted base in Section 3.1 and 3.2; the paper later finds runtime-checker bugs, showing the assumption is fallible.
  • domain assumption The random test case generator produces inputs satisfying the assertion preconditions.
    Stated in Section 2; incorrect generation would undermine the relevance of test executions.
  • domain assumption The properties of interest are representable as runnable runtime checks.
    Section 3.3 lists this as a requirement for applying the method; it excludes properties such as termination.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Checkification: A Practical Approach for Testing Static Analysis Truths." pith.science (2026). https://pith.science/paper/JZCHC6YT

@misc{pith2026250112093,
  author       = {Pith},
  title        = {Pith review of: Checkification: A Practical Approach for Testing Static Analysis Truths},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/JZCHC6YT}},
  note         = {Machine review of arXiv:2501.12093}
}
read the original abstract

Static analysis is an essential component of many modern software development tools. Unfortunately, the ever-increasing complexity of static analyzers makes their coding error-prone. Even analysis tools based on rigorous mathematical techniques, such as abstract interpretation, are not immune to bugs. Ensuring the correctness and reliability of software analyzers is critical if they are to be inserted in production compilers and development environments. While compiler validation has seen notable success, formal validation of static analysis tools remains relatively unexplored. In this paper, we propose a method for testing abstract interpretation-based static analyzers. Broadly, it consists in checking, over a suite of benchmarks, that the properties inferred statically are satisfied dynamically. The main advantage of our approach lies in its simplicity, which stems directly from framing it within the Ciao assertion-based validation framework, and its blended static/dynamic assertion checking approach. We demonstrate that in this setting, the analysis can be tested with little effort by combining the following components already present in the framework: 1) the static analyzer, which outputs its results as the original program source with assertions interspersed; 2) the assertion run-time checking mechanism, which instruments a program to ensure that no assertion is violated at run time; 3) the random test case generator, which generates random test cases satisfying the properties present in assertion preconditions; and 4) the unit-test framework, which executes those test cases. We have applied our approach to the CiaoPP static analyzer, resulting in the identification of many bugs with reasonable overhead. Most of these bugs have been either fixed or confirmed, helping us detect a range of errors not only related to analysis soundness but also within other aspects of the framework.

Figures

Figures reproduced from arXiv: 2501.12093 by the authors.

Figure 1
Figure 1. The Ciao assertion framework (CiaoPP’s verification/testing architecture). Static Program Analysis. Abstract interpretation is a formal framework for static anal￾ysis that allows inferring program properties that hold for all possible program executions. Different abstractions, called abstract domains, are used in this process for approximat￾ing sets of concrete run-time states. The CiaoPP analyzer is abstract inter… view at source ↗
Figure 2
Figure 2. An incorrect simple mode analysis. 3 The Checkification Algorithm This section provides a detailed overview of the proposed algorithm for testing the static analyzer, which incorporates all the components mentioned above. Illustrative example. Let us start by sketching the main idea of our approach with a motivating example. Assume we have the following simple Prolog program, where we use an entry assertion to defin… view at source ↗
Figure 3
Figure 3. The instrumented program. to the different capabilities of the Ciao model presented previously, this can be achieved by (1) turning the status of the true assertions produced by the analyzer into check, as shown in [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

16 extracted references · 16 canonical work pages

  1. [1]

    Andreasen, E. S. , Møller, A. , and Nielsen, B. B. Systematic approaches for increasing soundness and precision of static analyzers. In Proceedings of the 6th ACM SIGPLAN Interna- tional Workshop on State Of the Art in Program Analysis 2017, SOAP 2017, 31–36, New York, NY, USA. Association for Computing Machinery. 28 Arias, J. , Carro, M., Salazar, E. , M...

    work page 2017

  2. [1982]

    American Journal of Computational Linguistics , 8, 3-4, 110–122

    An Efficient, Easily Adaptable System For Interpret- ing Natural Language Queries. American Journal of Computational Linguistics , 8, 3-4, 110–122. 14 Wu, J. , Hu, G. , Tang, Y. , and Yang, J. Effective dynamic detection of alias analysis errors. In Proceedings of the 2013 9th Joint Meeting on Foundations of S oftware Engineering 2013, ESEC/FSE 2013, 279–289...

    work page 2013

  3. [1991]

    1991, pp. 49–63. MIT Press. 14 Muthukumar, K. and Hermenegildo, M

    work page 1991

  4. [1992]

    Journal of Logic Programming , 13, 2/3, 315–347

    Compile-time Derivation of Variable Depen- dency Using Abstract Interpretation. Journal of Logic Programming , 13, 2/3, 315–347. 2, 6, 14 Na v as, J., Bueno, F. , and Hermenegildo, M. V. Efficient Top-Down Set-Sharing Analysis Using Cliques. In 8th International Symposium on Practical Aspects of Declar ative Languages (PADL’06) 2006, number 2819 in LNCS, pp...

    work page 2006

  5. [1996]

    ACM Transactions on Programming Languages and Systems , 18, 5, 564–615

    Global Analysis of Constraint Logic Programs. ACM Transactions on Programming Languages and Systems , 18, 5, 564–615. 14 Guarnieri, M. , Köpf, B. , Morales, J. F. , Reineke, J. , and Sánchez, A. Spectector: Prin- cipled Detection of Speculative Information Flows. In 2020 IEEE Symposium on Security and Privacy (SP) 2020, pp. 1–19. 15 He, W. , Di, P. , Ming...

    work page 2020

  6. [1997]

    The Ciao System Documentation Ser ies–TR CLIP5/97.3, Facultad de Informática, UPM

    An Automatic Documentation Generator for (C)LP – Reference Manual. The Ciao System Documentation Ser ies–TR CLIP5/97.3, Facultad de Informática, UPM. Online at https://ciao-lang.org. 15 Hermenegildo, M. V. , Puebla, G. , and Bueno, F. Using Global Analysis, Partial Specifica- tions, and an Extensible Assertion Language for Program Val idation and Debugging...

    work page 1999

  7. [2000]

    ACM Transactions on Programming Languages and Systems, 22, 2, 187–223

    Incremental Analysis of Constraint Logic Programs. ACM Transactions on Programming Languages and Systems, 22, 2, 187–223. 2 Jourdan, J.-H., Lapor te, V., Blazy, S. , Leroy, X., and Pichardie, D. A Formally-Verified C Static Analyzer. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposiu m on Principles of Programming Languages 2015, POPL ’15, 247–2...

    work page 2015

  8. [2002]

    SIGPLAN Not

    A type system for certified binaries. SIGPLAN Not. , 37, 1, 217–232. 28 Søndergaard, H. An Application of Abstract Interpretation of Logic Program s: Occur Check Reduction. In European Symposium on Programming, LNCS 123 1986, pp. 327–338. Springer. 14 Stade, Y., Tilscher, S., and Seidl, H

    work page 1986

Show all 16 references
  1. [2005]

    Lecture Notes in Computer Science , 3444, 21–30

    The ASTRÉE analyzer. Lecture Notes in Computer Science , 3444, 21–30. 14th European Symposium on Programming, ESOP 2005, held as part o f the Joint European Confer- ences on Theory and Practice of Software, ETAPS 2005 ; Confer ence date: 04-04-2005 Through 08-04-2005. 28 Cuoq,...

    2005

  2. [2006]

    Technical Report CLIP2/06, Technical University of Madrid (UPM), Facultad d e Informática, 28660 Boadilla del Monte, Madrid, Spain

    A Tutorial on Program Development and Optimization using the Ciao Prep rocessor. Technical Report CLIP2/06, Technical University of Madrid (UPM), Facultad d e Informática, 28660 Boadilla del Monte, Madrid, Spain. 14 Bugariu, A. , Wüstholz, V. , Christakis, M., and Müller, P. A...

    2018

  3. [2010]

    New Generation Computing , 28, 2, 117–206

    Automatic Inference of De- terminacy and Mutual Exclusion for Logic Programs Using Mod e and Type Analyses. New Generation Computing , 28, 2, 117–206. 14 Mera, E. , Lopez-Garcia, P. , and Hermenegildo, M. V. Integrating Software Testing and Run-Time Checking in an Assertion Ve...

    2009

  4. [2015]

    Theory and Practice of Logic Programming, 31st Int’l

    Practical Run-time Checking via Unobtrusive Property Caching. Theory and Practice of Logic Programming, 31st Int’l. Conference on Logic Programming (ICLP’15) Spec ial Issue , 15, 04-05, 726–741. https://arxiv.org/abs/1507.05986. 2, 15 Stulov a, N., Morales, J. F. , and Hermene...

    2016 arXiv

  5. [2017]

    2017, pp. 590–600. 29 Klinger, C., Christakis, M., and Wüstholz, V. Differentially testing soundness and precision of program analyzers. In Proceedings of the 28th ACM SIGSOFT International Symposiu m on Software Testing and Analysis 2019, ISSTA 2019, 239–250, New York, NY, USA...

    2017

  6. [2018]

    Theory and Practice of Logic Programming, 18, 3-4, 337–354

    Constraint Answer Set Programming without Grounding. Theory and Practice of Logic Programming, 18, 3-4, 337–354. 15 Bagnara, R. , Ricci, E. , Zaff anella, E., and Hill, P. M. Possibly not closed convex poly- hedra and the Parma Polyhedra Library. In Hermenegildo, M. V. and Pue...

    2002

  7. [2023]

    2023, volume 385 of Electronic Proceedings in Theoretical Computer Science (EPTCS), pp. 324–330. Open Publishing Association (OPA). See also a ssociated poster at https://cliplab.org/papers/hald-poster-iclp.pdf . 14 For tz, S., Mesnard, F. , P a yet, É., Perrouin, G. , V anhoo...

    2023

  8. [2024]

    28 Hermenegildo, M. V. A System for Automatically Generating Documentation for (C )LP Pro- 31 grams. In Special Issue on Parallelism and Implementation of (C)LP Sy stems 2000, volume 30 of Electronic Notes in Theoretical Computer Science . 15 Hermenegildo, M. V. , Bueno, F. , ...

    2000

Pith tools

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