Pith. sign in

REVIEW 4 major objections 5 minor 72 references

A Modular Program-Transformation Framework for Reducing Specifications to Reachability

T0 review · 4 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 The paper claims that composing an instrumentation-automaton-based program transformation with a reachability verifier preserves the specification, and makes off-the-shelf reachability verifiers effective on termination, no-overflow, and…

desk verdict A genuinely useful engineering paper that packages known specification-to-reachability transformations as input-level rewrites, with a strong but restricted evaluation; the unproved equivalence claim is the main weakness. read the letter →

arxiv 2501.16310 v1 pith:C3XLGRAM submitted 2025-01-27 cs.PL

Dirk Beyer , Marek Jankola , Marian Lingsch-Rosenfeld , Tian Xia , Xiyue Zheng This is my paper · ORCID
classification cs.PL
keywords softwareverificationprogramtransformationreachabilityinstrumentationautomataterminationno-overflowmemorycleanupliveness
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

This paper tries to establish that specification checking can be decoupled from verification algorithms: instead of teaching a verifier a new property, transform the input C program so the property becomes an ordinary reachability check, and reuse any existing reachability verifier unchanged. The authors build a framework around instrumentation automata, which specify how to insert monitoring code (ghost variables, assertions, state-saving) into a program, and implement three concrete instantiations: termination, no-overflow, and memory cleanup. On standard benchmarks, reachability verifiers applied to the transformed programs solve about as many tasks as verifiers with native support, and in the termination case the transformed composition solved more tasks than the native termination tool. The broader claim is modularity: because the transformation outputs a C program, any tool that can check reachability—verifier, tester, or fuzzer—inherits support for every specification expressible in the framework.

What carries the argument

The load-bearing mechanism is the instrumentation automaton (IA): a small automaton whose states carry annotations (init, loop_head, true, end) and whose transitions match CFA edges by C-expression patterns and emit operations—assertions, ghost-variable updates, nondeterministic state-saving—to be inserted before or after the matched edge. Two operators drive the transformation: the sequentialization operator ⊗ synchronously traverses the CFA and the IA and produces an instrumented CFA, and the instrumentation operator ⊎ splices those new operations back into the original C program while preserving its structure. This is what lets an arbitrary reachability verifier consume the result as ordinary C with assertions.

What would settle it

Run the termination transformation on a terminating program whose loop traverses a linked list created with malloc, so each iteration visits a fresh heap address; if the instrumented program passes the reachability check (reports no repeated state), then the transformation has wrongly certified termination. Equivalently, search the benchmark set for any program where a reachability verifier on the transformed program gives a different verdict than a trusted native verifier on the original program, and confirm the difference is caused by the transformation rather than verifier imprecision.

Watch

Extended reading notes

Core claim

The central discovery is that three practically important specifications—termination, no-overflow, and memory cleanup—can be reduced to reachability by a program transformation that is independent of any particular verifier, and that doing the transformation at the source level rather than inside the verifier does not cost efficiency. The reduction is exact on the supported subset: for the sequentialization operator ⊗ and the instrumentation operator ⊎, the paper asserts P |= phi iff P' |= reachability for the transformed program P'. The experimental comparison shows that reachability verifiers on transformed programs are competitive with, and sometimes better than, verifiers that natively implement the original specification, and that the framework's expressiveness extends to general liveness properties via an explicit-liveness construction.

Load-bearing premise

The transformations are assumed to preserve the verification problem exactly—P satisfies phi if and only if the transformed program satisfies reachability—and this equivalence is not proven for the full supported subset; the termination transformation is explicitly unsound for programs with dynamic heap structures, and one memory-cleanup verdict was wrong because of function pointers.

Editorial extensions

If this is right

  • Any reachability verifier for C can be pointed at the transformed program to check termination, no-overflow, or memory cleanup, with no changes to the verifier itself.
  • In the experiments, the transformed reachability composition solved more termination tasks than a verifier with native termination support, and matched native no-overflow support within a few tasks.
  • Encoding the transformation in the input program rather than inside the verifier does not cause a systematic efficiency loss; the overhead is small relative to the 900-second time limit.
  • Because the framework can express general liveness as explicit liveness, any LTL property—decomposed into safety and liveness parts—can in principle be checked by a reachability-only verifier.

Reading between the lines

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

  • A testable corollary the paper does not chase: since the output is plain C, coverage-guided fuzzers and concolic testers can be pointed at the instrumented program, turning any property in the IA language into a fuzzable assertion.
  • The framework suggests a standardization opportunity: if specification authors publish instrumentation automata as an interchange format, verifier competitions could decouple property support from algorithm tuning, making the 'specification library' a shared artifact.
  • The 17 benchmark tasks with hidden signed-overflow behavior found during termination experiments indicate the transformation can double as an undefined-behavior sanitizer during benchmark curation, a side effect worth exploiting deliberately.
  • The termination transformation's state-repetition check is inherently finite-state; extending it to heap-manipulating programs would require combining it with heap summaries or ranking-function synthesis, which the paper leaves open.
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

4 major / 5 minor

Summary. The paper proposes a modular program-transformation framework, TransVer, that turns a C verification task P |= phi into a reachability task P' |= reachability by instrumenting the input program rather than a verifier's internal representation. Specifications are written as instrumentation automata (IA), and two operators, sequentialization (⊗) and instrumentation (⊎), are defined operationally in Section 4. The framework is instantiated for three SV-COMP specifications: no-overflow, termination, and memory cleanup; Section 6 sketches an explicit-liveness transformation. The evaluation compares reachability-only verifiers applied to transformed programs against native verifiers on SV-COMP 2024 benchmark subsets, and reports that the compositions are competitive in both effectiveness and efficiency.

Significance. If the central equivalence P |= phi iff P' |= reachability holds on the claimed input class, this is a practically useful contribution: it makes specification support a black-box preprocessing step, leverages mature reachability engines for other properties, and is backed by an open-source implementation and a broad experimental comparison over official SV-COMP tasks. The paper also credits prior work for the liveness-to-safety idea and carefully removes tasks with undefined behavior from the termination comparison. However, the correctness of the central operators is not demonstrated, and the paper itself records known limitations (termination on dynamic structures, one memory-cleanup verdict involving function pointers). The experimental claims therefore currently support the framework's usefulness only for the restricted, finite-state fragment of C that the paper actually evaluates.

major comments (4)
  1. [Section 4, Algorithm 1 and Eqs. (1)-(4)] The load-bearing claim of the paper is that composing the sequentialization operator ⊗ and the instrumentation operator ⊎ preserves the verification question: P |= phi iff P' |= reachability. No correctness theorem is stated or proved. Algorithm 1 and Eqs. (1)-(4) define the construction operationally, but there is no argument that (a) pattern matching is total on the supported subset, (b) an IA operation is inserted exactly once per matched CFA edge in the intended order, (c) unmatched edges are passed through without changing semantics, and (d) new locations introduced by NE do not affect program behavior. Since all research questions in Section 7 depend on this equivalence, the paper needs a formal theorem with a proof, or at minimum a precise statement of the supported input class together with a correctness argument for that class.
  2. [Section 5, termination IA (Fig. 6) and Section 7 benchmark subset] The paper states that the termination transformation is 'complete but not sound' for dynamic structures such as linked lists, because an infinite execution can avoid revisiting the same full state. The evaluation then removes tasks containing structures and arrays from the termination and no-overflow subsets. This means the headline claim that the framework 'can extend existing verifiers to be effective on specifications that they do not support natively' is demonstrated only for programs whose variables range over finite domains, not for general C programs. The paper should either prove soundness for the exact supported subset and state that subset prominently, include the excluded program classes in the evaluation, or narrow the abstract and conclusion claims.
  3. [Section 5, memory cleanup IA (Fig. 7) and Table 5] The memory-cleanup transformation is described as sound and complete because 'we handle all the relevant standard functions for memory allocation'. Table 5, however, reports one incorrect CPAchecker-R alarm, and the text attributes it to incomplete handling of function pointers. Function pointers are part of the C language and appear in the evaluated benchmark set, so the claimed soundness is overbroad as written. The paper should qualify the supported input class for memory cleanup, state what happens to function-pointer calls, and either exclude such tasks from the claim or handle them in the transformation.
  4. [Section 7.5, Internal Validity] The threat-to-validity paragraph asserts that all incorrect results were inspected and none were caused by the transformation, but no procedure or evidence is given. Because incorrect verdicts appear in the results for the composed verifiers (e.g., 8 incorrect CPAchecker-R verdicts for no-overflow in Table 3), the reader cannot evaluate whether these lie inside the supported subset or whether they indicate a transformation bug. Please describe the inspection methodology, report the task categories of the incorrect verdicts, and make the transformed programs and inputs available so the claim is checkable.
minor comments (5)
  1. [Section 4, example] The text contains a typo: 'initeliaze_automata' should be 'initialize_automata'.
  2. [Table 3] The first data column mixes row labels with benchmark totals ('Correct 890', 'Proofs 615', 'Alarms 275'), which is confusing. Please reformat the table so the row labels are separated from the per-tool counts, and explicitly state that 615 and 275 are the ground-truth proof and alarm counts in the benchmark set.
  3. [Section 5, no-overflow IA] The soundness statement for no-overflow is conditional on decomposing complex arithmetic expressions and tracking signed-integer types, but the decomposition is not described. A short example of how a multi-operation line is split would make the supported input class clearer.
  4. [Section 7.1] The choice of the 'third-best tool' as a baseline is explained informally ('still competitive ... unlikely to contain bugs'). Please state the exact ranking criterion and why the third-best tool is more appropriate than the best or second-best tool for the comparison.
  5. [Section 6] The reference to 'Biere and Schuppan' should be checked against the bibliography entry [68], which lists Schuppan and Biere as authors.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the transformations are genuine reductions evaluated on external benchmarks, with acknowledged correctness limitations that are not circular.

full rationale

The paper does not fit parameters to target data, does not define the specification in terms of the reachability result, and does not rely on a load-bearing self-citation chain. The central equivalence P |= phi iff P' |= reachability is asserted operationally for the sequentialization and instrumentation operators, but the absence of a proof is a soundness gap, not circularity. The termination and liveness reductions explicitly build on the external published work of Schuppan and Biere [68], and the paper itself flags that the termination transformation is 'complete but not sound' for dynamic structures such as linked lists, which is an honest correctness limitation rather than a circular step. The experimental evaluation uses the external SV-COMP benchmark set and compares transformed reachability verifiers against native-support verifiers, so the empirical claims are not manufactured from the transformation's own assumptions. No 'prediction' reduces by construction to a fitted input, and no uniqueness theorem is imported from the authors' prior work. The paper's main weakness is under-proving the correctness of the transformations and restricting the benchmark subset to avoid known unsound cases; these are correctness risks, not circularity.

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

No fitted parameters or invented entities. The paper's axioms are unproved correctness and soundness premises for the transformations and the CFA model.

assumptions (5)
  • ad hoc to paper The sequentialization operator ⊗ and instrumentation operator ⊎ preserve the verification question: P |= phi iff P' |= reachability for every input program and correctly specified IA.
    Invoked throughout Section 4 and used to justify all three transformations in Section 5, but no correctness proof is supplied; a counterexample for dynamic structures is acknowledged for termination.
  • domain assumption The CFA built by CPAchecker faithfully represents every behavior of the C program, including operations on function pointers and calls through function pointers.
    The framework assumes the CFA together with stored type information captures all relevant operations; memory cleanup misses function-pointer calls, causing an incorrect verdict (Section 7.2, Table 5).
  • domain assumption For termination, every non-terminating execution of the supported subset revisits a state; equivalently, all variables have finite ranges and dynamic heap structures are absent.
    Stated in Section 5: the termination transformation is 'complete but not sound' for dynamic structures like linked lists, so the claim holds only for finite-state programs.
  • domain assumption For no-overflow, programs are decomposed so each CFA edge contains at most one signed-integer operation, and the guard plus decomposition covers all overflow behaviors.
    Stated in Section 5: 'let us assume that a program consists only of signed integer variables and, at most, one arithmetic operation per line.'
  • domain assumption The set of standard memory functions (malloc, calloc, realloc, free) is sufficient to track all allocations and frees in evaluated programs.
    Stated in Section 5 for memory cleanup: 'Since we handle all the relevant standard functions for memory allocation, this transformation is sound and complete.' Function pointers are not covered.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Modular Program-Transformation Framework for Reducing Specifications to Reachability." pith.science (2026). https://pith.science/paper/C3XLGRAM

@misc{pith2026250116310,
  author       = {Pith},
  title        = {Pith review of: A Modular Program-Transformation Framework for Reducing Specifications to Reachability},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/C3XLGRAM}},
  note         = {Machine review of arXiv:2501.16310}
}
read the original abstract

Software verification is a complex problem, and verification tools need significant tuning to achieve high performance. Due to this, many verifiers choose to specialize on reachability properties, or invest the time to implement known transformations from the given specification to reachability on their internal representations. To improve this situation, we provide transformations as stand-alone components, modifying the input program instead of the internal representation, enabling their usage as a preprocessing step by other verifiers. This way, we separate two concerns: improving the performance of reachability analyses and implementing efficient transformations of arbitrary specifications to reachability. We implement the transformations in a framework that is based on instrumentation automata, inspired by the BLAST query language. In our initial study, we support three important concrete specifications for C programs: termination, no-overflow, and memory cleanup. Moreover, we discuss the broader expressiveness of our framework and show how general liveness properties can be transformed to reachability. We demonstrate the effectiveness and efficiency of our transformations by comparing verifiers that support the specifications natively with verifiers for reachability applied on the transformed programs. The results are very promising: Our transformations can extend existing verifiers to be effective on specifications that they do not support natively, and that the efficiency is often similar to verifiers that natively support the considered specifications.

Figures

Figures reproduced from arXiv: 2501.16310 by the authors.

Figure 1
Figure 1. An example program (left) with a corresponding CFA (right) [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Workflow of the program transformation Instrumentation Automata. An instrumentation automaton specifies how an input program needs to be instrumented in order to make the original property explicit using assertions. It is inspired by the observer automata from the BLAST query language [17]. The observer automata are expressive enough for all temporal safety and liveness properties, and their syntax resembles C progr… view at source ↗
Figure 3
Figure 3. An example IA (left) and the corresponding CFA after sequentialization with the CFA from [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figures from the paper (9 more)
Figure 4
Figure 4. Figure 4: An example of an instrumented program 5 Specifications as Instrumentation Automata To study the performance of reachability analyzers when applied to different specifications, we focus our experiments to the transformation of three specifications from SV-COMP [15]. Thi…
Figure 5
Figure 5. Figure 5: An excerpt of the IA for the no-overflow property 𝑞2 𝑜𝑝 ≡ if(nondet() ∧ saved = 0){ 𝑥 ′ 0 = 𝑥0; . . . ; 𝑥 ′ 𝑛 = 𝑥𝑛;saved = 1; } 𝜋 ≡ (saved = 1) ⇒ (𝑥 ′ 0 ≠ 𝑥0 ∨ 𝑥 ′ 1 ≠ 𝑥1 ∨ · · · ∨ 𝑥 ′ 𝑛 ≠ 𝑥𝑛) loop_head 𝑞0 init cond | assert(𝜋); 𝑜𝑝; | 𝐴 true | int 𝑠𝑎𝑣𝑒𝑑 = 0; int 𝑥 ′ 0 …
Figure 6
Figure 6. Figure 6: An example of an IA for the termination property results [PITH_FULL_IMAGE:figures/full_fig_p010_6.png]
Figure 7
Figure 7. Figure 7: An example of an IA for the memory cleanup property Memory Cleanup [PITH_FULL_IMAGE:figures/full_fig_p011_7.png]
Figure 8
Figure 8. Figure 8: An example of an IA for the explicit liveness property infinite execution. However, in this case, the infinite execution must not satisfy at least one of the assert_live conditions. Such execution would violate the liveness property because there is an infinite executi…
Figure 9
Figure 9. Figure 9: Quantile plots for (a) no-overflow and (b) termination tasks showing verifiers not supporting the [PITH_FULL_IMAGE:figures/full_fig_p014_9.png]
Figure 10
Figure 10. Figure 10: Quantile plots for (a) no-overflow and (b) termination tasks comparing verifiers on the original and [PITH_FULL_IMAGE:figures/full_fig_p016_10.png]
Figure 11
Figure 11. Figure 11: Quantile plot for all correct results on memcleanup tasks [PITH_FULL_IMAGE:figures/full_fig_p017_11.png]
Figure 12
Figure 12. Figure 12: Comparison of the CPU time of CPAchecker when transforming the properties internally and when doing the transformation in the input program for no-overflow and termination tasks External Validity. The conclusions about the benefit of the transformations might not hold…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

72 extracted references · 48 canonical work pages

  1. [1]

    [n. d.]. INT32-C. Ensure that operations on signed integers do not result in overflow. https://wiki.sei.cmu.edu/ confluence/display/c/INT32-C.+Ensure+that+operations+on+signed+integers+do+not+result+in+overflow. [Accessed 28-08-2024]

    work page 2024

  2. [2]

    Afzal, A

    M. Afzal, A. Asia, A. Chauhan, B. Chimdyalwar, P. Darke, A. Datar, S. Kumar, and R. Venkatesh. 2019. VeriAbs: Verification by Abstraction and Test Generation. InProc. ASE. IEEE, 1138–1141. https://doi.org/10.1109/ASE.2019.00121

    arXiv 2019

  3. [3]

    A. V. Aho, R. Sethi, and J. D. Ullman. 1986. Compilers: Principles, Techniques, and Tools . Addison-Wesley. ISBN: 978-0-201-10088-4 https://www.worldcat.org/isbn/978-0-201-10088-4

    work page 1986

  4. [4]

    Alglave, A

    J. Alglave, A. F. Donaldson, D. Kröning, and M. Tautschnig. 2011. Making Software Verification Tools Really Work. In Proc. ATV A (LNCS 6996). Springer, 28–42. https://doi.org/10.1007/978-3-642-24372-1_3

    work page doi:10.1007/978-3-642-24372-1_3 2011

  5. [5]

    K. M. Alshmrany, M. Aldughaim, A. Bhayat, and L. C. Cordeiro. 2021. FuSeBMC: An energy-efficient test generator for finding security vulnerabilities in C programs. In Proc. TAP. Springer, 85–105. https://doi.org/10.1007/978-3-030- 79379-1_6

    doi:10.1007/978-3-030- 2021

  6. [6]

    Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, and Philipp Rümmer. 2023. Automatic Program Instrumentation for Automatic Verification. In Proc. CA V. 281–304. ISBN: 978-3-031-37709-9

    work page 2023

  7. [7]

    Ayaziová, D

    P. Ayaziová, D. Beyer, M. Lingsch-Rosenfeld, M. Spiessl, and J. Strejček. 2024. Software Verification Witnesses 2.0. In Proc. SPIN. Springer

    work page 2024

  8. [8]

    Baier, D

    D. Baier, D. Beyer, P.-C. Chien, M.-C. Jakobs, M. Jankola, M. Kettl, N.-Z. Lee, T. Lemberger, M. Lingsch-Rosenfeld, H. Wachowitz, and P. Wendler. 2024. Software Verification withCPAchecker 3.0: Tutorial and User Guide. In Proc. FM (LNCS 14934). Springer. https://doi.org/10.1007/978-3-031-71177-0_30

    work page doi:10.1007/978-3-031-71177-0_30 2024

Show all 72 references
  1. [9]

    Baier, D

    D. Baier, D. Beyer, P.-C. Chien, M. Jankola, M. Kettl, N.-Z. Lee, T. Lemberger, M. Lingsch-Rosenfeld, M. Spiessl, H. Wachowitz, and P. Wendler. 2024. CPAchecker 2.3 with Strategy Selection (Competition Contribution). In Proc. TACAS (3) (LNCS 14572). Springer, 359–364. https://...

    2024 doi

  2. [10]

    Bajczi, D

    L. Bajczi, D. Szekeres, M. Mondok, Z. Ádám, M. Somorjai, C. Telbisz, M. Dobos-Kovács, and V. Molnár. 2024.Emergen- Theta: Verification Beyond Abstraction Refinement (Competition Contribution). In Proc. TACAS (3) (LNCS 14572) . Springer, 371–375. https://doi.org/10.1007/978-3-0...

    2024 doi

  3. [11]

    Bajczi, C

    L. Bajczi, C. Telbisz, M. Somorjai, Z. Ádám, M. Dobos-Kovács, D. Szekeres, M. Mondok, and V. Molnár. 2024.Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution). InProc. TACAS (3) (LNCS 14572). Springer, 412–417. https://doi.org/10.1007/978-3-...

    2024 doi

  4. [12]

    Ball and S

    T. Ball and S. K. Rajamani. 2002. SLIC: A Specification Language for Interface Checking (of C) . Technical Report MSR-TR-2001-21. Microsoft Research. https://www.microsoft.com/en-us/research/publication/slic-a-specification- language-for-interface-checking-of-c/

    2002

  5. [13]

    Ball and S

    T. Ball and S. K. Rajamani. 2002. The Slam project: Debugging System Software via Static Analysis. In Proc. POPL. ACM, 1–3. https://doi.org/10.1145/503272.503274

    2002

  6. [14]

    D. Beyer. 2024. Automatic Testing of C Programs: Test-Comp 2024. In TBA. Springer

    2024

  7. [15]

    D. Beyer. 2024. State of the Art in Software Verification and Witness Validation: SV-COMP 2024. InProc. TACAS (3) (LNCS 14572). Springer, 299–329. https://doi.org/10.1007/978-3-031-57256-2_15

    2024 doi

  8. [16]

    D. Beyer. 2024. SV-Benchmarks: Benchmark Set for Software Verification (SV-COMP 2024). Zenodo. https://doi.org/ 10.5281/zenodo.10669723

    2024 doi

  9. [17]

    Beyer, A

    D. Beyer, A. J. Chlipala, T. A. Henzinger, R. Jhala, and R. Majumdar. 2004. TheBlast Query Language for Software Verification. In Proc. SAS (LNCS 3148) . Springer, 2–18. https://doi.org/10.1007/978-3-540-27864-1_2

    2004 doi

  10. [18]

    Beyer, M

    D. Beyer, M. Dangl, D. Dietsch, M. Heizmann, T. Lemberger, and M. Tautschnig. 2022. Verification Witnesses.ACM Trans. Softw. Eng. Methodol. 31, 4 (2022), 57:1–57:69. https://doi.org/10.1145/3477579

    2022 doi

  11. [19]

    Beyer, M

    D. Beyer, M. Dangl, and P. Wendler. 2018. A Unifying View on SMT-Based Software Verification. J. Autom. Reasoning 60, 3 (2018), 299–335. https://doi.org/10.1007/s10817-017-9432-6

    2018 doi

  12. [20]

    Beyer, S

    D. Beyer, S. Gulwani, and D. Schmidt. 2018. Combining Model Checking and Data-Flow Analysis. In Handbook of Model Checking. Springer, 493–540. https://doi.org/10.1007/978-3-319-10575-8_16

    2018 doi

  13. [21]

    Beyer, T

    D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar. 2005. Checking Memory Safety with Blast. In Proc. FASE (LNCS 3442). Springer, 2–18. https://doi.org/10.1007/978-3-540-31984-9_2

    2005 doi

  14. [22]

    Beyer, T

    D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar. 2007. The Software Model CheckerBlast. Int. J. Softw. Tools Technol. Transfer 9, 5-6 (2007), 505–525. https://doi.org/10.1007/s10009-007-0044-z

    2007 doi

  15. [23]

    Beyer and M

    D. Beyer and M. E. Keremoglu. 2011. CPAchecker: A Tool for Configurable Software Verification. In Proc. CA V (LNCS 6806). Springer, 184–190. https://doi.org/10.1007/978-3-642-22110-1_16

    2011 doi

  16. [24]

    Beyer and N.-Z

    D. Beyer and N.-Z. Lee. 2024. The Transformation Game: Joining Forces for Verification. Springer. https://www.sosy- lab.org/research/pub/2024-Katoen60.The_Transformation_Game_Joining_Forces_for_Verification.pdf

    2024

  17. [25]

    Beyer, M

    D. Beyer, M. Lingsch-Rosenfeld, and M. Spiessl. 2022. A Unifying Approach for Control-Flow-Based Loop Abstraction. In Proc. SEFM (LNCS 13550) . Springer, 3–19. https://doi.org/10.1007/978-3-031-17108-6_1 20 D. Beyer, M. Jankola, M. Lingsch-Rosenfeld, T. Xia and X. Zheng

    2022 doi

  18. [27]

    Beyer, S

    D. Beyer, S. Löwe, and P. Wendler. 2019. Reliable Benchmarking: Requirements and Solutions. Int. J. Softw. Tools Technol. Transfer 21, 1 (2019), 1–29. https://doi.org/10.1007/s10009-017-0469-y

    2019 doi

  19. [28]

    Beyer and M

    D. Beyer and M. Spiessl. 2020. MetaV al: Witness Validation via Verification. In Proc. CA V (LNCS 12225). Springer, 165–177. https://doi.org/10.1007/978-3-030-53291-8_10

    2020 doi

  20. [29]

    Clarke, Ofer Strichman, and Yunshan Zhu

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

    2003 doi

  21. [30]

    Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, and Virgile Prevosto. 2017. RPP: Automatic Proof of Relational Properties by Self-composition. In Tools and Algorithms for the Construction and Analysis of Systems . 391–397. ISBN: 978-3-662-54577-5

    2017

  22. [31]

    Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto, and Guillaume Petiot. 2018. Static and Dynamic Verification of Relational Properties on Self-composed C Code. In Tests and Proofs. 44–62. ISBN: 978-3-319-92994-1

    2018

  23. [32]

    Eric Bodden and Laurie Hendren. 2012. The Clara framework for hybrid typestate analysis. International Journal on Software Tools for Technology Transfer 14, 3 (01 Jun 2012), 307–326. https://doi.org/10.1007/s10009-010-0183-5

    2012 doi

  24. [33]

    Böhme, V.-T

    M. Böhme, V.-T. Pham, and A. Roychoudhury. 2016. Coverage-Based Greybox Fuzzing as Markov Chain. In Proc. SIGSAC. ACM, New York, NY, USA, 1032–1043. https://doi.org/10.1145/2976749.2978428

    2016

  25. [34]

    A. R. Bradley. 2011. SAT-Based model checking without unrolling. In Proc. VMCAI (LNCS 6538) . Springer, 70–87. https://doi.org/10.1007/978-3-642-18275-4_7

    2011 doi

  26. [35]

    Chalupa, J

    M. Chalupa, J. Strejček, and M. Vitovská. 2018. Joint Forces for Memory Safety Checking. In Proc. SPIN. Springer, 115–132. https://doi.org/10.1007/978-3-319-94111-0_7

    2018 doi

  27. [36]

    Chien and N.-Z

    P.-C. Chien and N.-Z. Lee. 2024. CPV: A Circuit-Based Program Verifier (Competition Contribution). InProc. TACAS (3) (LNCS 14572). Springer, 365–370. https://doi.org/10.1007/978-3-031-57256-2_22

    2024 doi

  28. [37]

    E. M. Clarke, D. Kröning, and F. Lerda. 2004. A Tool for Checking ANSI-C Programs. In Proc. TACAS (LNCS 2988) . Springer, 168–176. https://doi.org/10.1007/978-3-540-24730-2_15

    2004 doi

  29. [38]

    Condit, M

    J. Condit, M. Harren, S. McPeak, G. C. Necula, and W. Weimer. 2003. CCured in the real world. In Proc. PLDI. ACM, 232–244

    2003

  30. [39]

    Darke, B

    P. Darke, B. Chimdyalwar, S. Agrawal, R. Venkatesh, S. Chakraborty, and S. Kumar. 2023. VeriAbsL: Scalable Verification by Abstraction and Strategy Prediction (Competition Contribution). In Proc. TACAS (2) (LNCS 13994) . Springer, 588–593. https://doi.org/10.1007/978-3-031-30820-8_41

    2023 doi

  31. [40]

    Dietsch, M

    D. Dietsch, M. Heizmann, D. Klumpp, F. Schüssele, and A. Podelski. 2023. Ultimate Taipan 2023 (Competition Contribution). In Proc. TACAS (2) (LNCS 13994) . Springer, 582–587. https://doi.org/10.1007/978-3-031-30820-8_40

    2023 doi

  32. [41]

    A. F. Donaldson, L. Haller, D. Kröning, and P. Rümmer. 2011. Software Verification Using k-Induction. InProc. SAS (LNCS 6887). Springer, 351–368. https://doi.org/10.1007/978-3-642-23702-7_26

    2011 doi

  33. [42]

    Alexandre Duret-Lutz and Denis Poitrenaud. 2004. SPOT: An Extensible Model Checking Library Using Transition- Based Generalized Büchi Automata. In Proc. MASCOTS. IEEE, 76–83. https://doi.org/10.1109/MASCOT.2004.1348184

    2004 arXiv

  34. [43]

    Bernd Fischer, Omar Inverso, and Gennaro Parlato. 2013. CSeq: A concurrency pre-processor for sequential C verification tools. In Proc. ASE. IEEE, 710–713. https://doi.org/10.1109/ASE.2013.6693139

    2013

  35. [44]

    F. Frohn. 2020. A Calculus for Modular Loop Acceleration. In Proc. TACAS (1) (LNCS 12078) . Springer, 58–76. https: //doi.org/10.1007/978-3-030-45190-5_4

    2020 doi

  36. [45]

    Paul Gastin and Denis Oddoux. 2001. Fast LTL to Büchi Automata Translation. In Proc. CA V. Springer, 53–65. https://doi.org/10.1007/3-540-44585-4_6

    2001 doi

  37. [46]

    Griggio and M

    A. Griggio and M. Jonáš. 2023. Kratos2: An SMT-Based Model Checker for Imperative Programs. In Proc. CA V. Springer, 423–436. ISBN: 978-3-031-37708-2 https://doi.org/10.1007/978-3-031-37709-9_20

    2023 doi

  38. [47]

    Mark Harman. 2018. We Need a Testability Transformation Semantics. In Proc. SEFM (LNCS 10886) . Springer, 3–17. https://doi.org/10.1007/978-3-319-92970-5_1

    2018 doi

  39. [48]

    Harman, L

    M. Harman, L. Hu, R. M. Hierons, J. Wegener, H. Sthamer, A. Baresel, and M. Roper. 2004. Testability Transformation. IEEE Trans. Softw. Eng. 30, 1 (2004), 3–16. https://doi.org/10.1109/TSE.2004.1265732

    2004 arXiv

  40. [49]

    Heizmann, M

    M. Heizmann, M. Bentele, D. Dietsch, X. Jiang, D. Klumpp, F. Schüssele, and A. Podelski. 2024. Ultimate Automizer and the Abstraction of Bitwise Operations (Competition Contribution). In Proc. TACAS (3) (LNCS 14572) . Springer, 418–423. https://doi.org/10.1007/978-3-031-57256-2_31

    2024 doi

  41. [50]

    Omar Inverso, T. L. Nguyen, Bernd Fischer, S. La Torre, and Gennaro Parlato. 2015. Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-threaded C Programs. InProc. ASE. IEEE, 807–812. https://doi.org/10.1109/ASE.2015.108

    2015 doi

  42. [51]

    Arvid Jakobsson, Nikolai Kosmatov, and Julien Signoles. 2015. Fast as a shadow, expressive as a tree: hybrid memory monitoring for C. In Proceedings of the 30th Annual ACM Symposium on Applied Computing (SAC ’15) . ACM, 1765–1772. ISBN: 9781450331968 https://doi.org/10.1145/26...

    2015

  43. [52]

    Jeannet, P

    B. Jeannet, P. Schrammel, and S. Sankaranarayanan. 2014. Abstract acceleration of general linear loops. In Proc. POPL. ACM, 529–540. https://doi.org/10.1145/2535838.2535843

    2014

  44. [53]

    Jonáš, K

    M. Jonáš, K. Kumor, J. Novák, J. Sedláček, M. Trtík, L. Zaoral, P. Ayaziová, and J. Strejček. 2024. Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution (Competition Contribution). In Proc. TACAS (3) (LNCS 14572) . Springer, 406–411. https://doi.org/10.1007/...

    2024 doi

  45. [54]

    S. Julien. 2022. E-ACSL: Executable ANSI/ISO C Specification Language. Available at http://frama-c.com/download/e- acsl/e-acsl.pdf

    2022

  46. [55]

    Madhukar, B

    K. Madhukar, B. Wachter, D. Kröning, M. Lewis, and M. K. Srivas. 2015. Accelerating Invariant Generation. InProc. FMCAD. IEEE, 105–111

    2015

  47. [56]

    Malík, P

    V. Malík, P. Schrammel, T. Vojnar, and F. Nečas. 2023.2LS: Arrays and Loop Unwinding (Competition Contribution). In Proc. TACAS (2) (LNCS 13994) . Springer, 529–534. https://doi.org/10.1007/978-3-031-30820-8_31

    2023 doi

  48. [57]

    K. L. McMillan. 2003. Interpolation and SAT-Based Model Checking. In Proc. CA V (LNCS 2725) . Springer, 1–13. https://doi.org/10.1007/978-3-540-45069-6_1

    2003 doi

  49. [58]

    Metta, H

    R. Metta, H. Karmarkar, K. Madhukar, R. Venkatesh, and S. Chakraborty. 2024.Proton: Probes for Non-termination and Termination (Competition Contribution). In Proc. TACAS (3) (LNCS 14572) . Springer, 393–398. https://doi.org/10. 1007/978-3-031-57256-2_27

    2024

  50. [59]

    G. C. Necula. 1997. Proof-Carrying Code. In Proc. POPL. ACM, 106–119. https://doi.org/10.1145/263699.263712

    1997

  51. [60]

    G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. 2002.Cil: Intermediate Language and Tools for Analysis and Transformation of C Programs. In Proc. CC (LNCS 2304) . Springer, 213–228. https://doi.org/10.1007/3-540-45937-5_16

    2002 doi

  52. [61]

    G. C. Necula, S. McPeak, and W. Weimer. 2002. CCured: Type-Safe Retrofitting of Legacy Code. In Proc. POPL. ACM, 128–139. https://doi.org/10.1145/503272.503286

    2002

  53. [62]

    Helmuth Partsch and Ralf Steinbrüggen. 1983. Program Transformation Systems. ACM Comput. Surv. 15, 3 (1983), 199–236. https://doi.org/10.1145/356914.356917

    1983

  54. [63]

    Peringer, V

    P. Peringer, V. Šoková, and T. Vojnar. 2020.PredatorHP Revamped (Not Only) for Interval-Sized Memory Regions and Memory Reallocation (Competition Contribution). In Proc. TACAS (2) (LNCS 12079). Springer, 408–412. https: //doi.org/10.1007/978-3-030-45237-7_30

    2020 doi

  55. [64]

    Grgur Petric Maretić, Mohammad Torabi Dashti, and David Basin. 2014. LTL is closed under topological closure. Inform. Process. Lett. 114, 8 (2014), 408–413. https://doi.org/10.1016/j.ipl.2014.03.001

    2014 doi

  56. [65]

    Nir Piterman and Amir Pnueli. 2018. Temporal Logic and Fair Discrete Systems. In Handbook of Model Checking . Springer, 27–73. https://doi.org/10.1007/978-3-319-10575-8_2

    2018 doi

  57. [66]

    Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, and Pascale Le Gall. 2021. Methodology for Speci- fication and Verification of High-Level Requirements with MetAcsl. In FormaliSE. 54–67. https://doi.org/10.1109/ FormaliSE52586.2021.00012

    2021

  58. [67]

    2019.MetAcsl: Specification and Verification of High-Level Properties

    Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, and Pascale Le Gall. 2019.MetAcsl: Specification and Verification of High-Level Properties. In Tools and Algorithms for the Construction and Analysis of Systems . Springer, 358–364. ISBN: 978-3-030-17462-0

    2019

  59. [68]

    Viktor Schuppan and Armin Biere. 2006. Liveness Checking as Safety Checking for Infinite State Spaces. Electr. Notes Theor. Comput. Sci. 149, 1 (2006), 79–96. https://doi.org/10.1016/j.entcs.2005.11.018

    2006 doi

  60. [69]

    O. ˆSerý. 2009. Enhanced Property Specification and Verification inBlast. In Proc. FASE (LNCS 5503). Springer, 456–469. https://doi.org/10.1007/978-3-642-00593-0_32

    2009 doi

  61. [70]

    Silverman and Z

    J. Silverman and Z. Kincaid. 2019. Loop Summarization with Rational Vector Addition Systems. In Proc. CA V, Part 2 (LNCS 11562). Springer, 97–115. https://doi.org/10.1007/978-3-030-25543-5_7

    2019 doi

  62. [71]

    Eelco Visser. 2001. A Survey of Strategies in Program Transformation Systems. In Proc. WRS (ENTCS 57) . Elsevier, 109–143. https://doi.org/10.1016/S1571-0661(04)00270-1

    2001 doi

  63. [72]

    Kostyantyn Vorobyov, Julien Signoles, and Nikolai Kosmatov. 2017. Shadow state encoding for efficient monitoring of block-level properties. In Proceedings of the 2017 ACM SIGPLAN International Symposium on Memory Management . ACM, 47–58. ISBN: 9781450350440 https://doi.org/10....

    2017

  64. [73]

    Yao Zhang, Xiaofei Xie, Yi Li, Sen Chen, Cen Zhang, and Xiaohong Li. 2023. EndWatch: A Practical Method for Detecting Non-Termination in Real-World Software. InProc. ASE. 686–697. https://doi.org/10.1109/ASE56229.2023.00061

    2023

Pith tools

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