Pith. sign in

REVIEW 5 major objections 3 minor 97 references

This paper claims that a four-stage absorbing Markov chain with per-stage success probability δ predicts the latency of LLM-assisted verification pipelines: the process terminates almost surely and needs 4/δ attempts on average.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · deepseek-v4-flash

2026-08-03 19:17 UTC pith:2U3SD226

load-bearing objection The 4/δ mean is correct but textbook; the paper's advertised exponential tail bound is false and the 90k-trial 'stress test' is circular, so the core contribution does not survive scrutiny. the 5 major comments →

arxiv 2512.02080 v3 pith:2U3SD226 submitted 2025-11-30 cs.AI cs.FLcs.LGcs.SE

The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee

Pierre Dantas , Lucas Cordeiro , Youcheng Sun , Waldir Junior This is my paper
classification cs.AI cs.FLcs.LGcs.SE MSC 60J2068Q60
keywords formal verificationlarge language modelsabsorbing Markov chainconvergence theorembounded model checkingSMT solvingexpected iteration bounddynamic calibration
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

The paper claims that an LLM-plus-verifier repair loop, when decomposed into the four engineering stages CodeGen, Compilation, InvariantSynth, and SMTSolving, behaves like a sequential absorbing Markov chain: at each stage the next attempt succeeds with probability δ and otherwise retries the same stage. On that model, the paper proves a convergence theorem with three parts: the system reaches the absorbing Verified state almost surely for any δ>0; the expected number of iterations starting from the first stage is exactly 4/δ; and the probability that convergence takes more than k iterations decays exponentially. The paper supports the theorem with 90,000 vectorized Monte Carlo trials across δ values from 0.1 to 0.9, reporting that every run converges and that empirical means track 4/δ with a conservative factor near 1.0. If the theorem holds for real systems, verification pipelines stop being unpredictable black boxes: engineers could budget 4/δ attempts, set timeouts from the exponential tail, and choose models based on which operating region their δ falls into.

Core claim

The central claim is Theorem 1, the LLM-Verifier Convergence Theorem. For a five-state chain with transient states s1 through s4 and absorbing state s5 = Verified, where each attempted transition advances with probability δ and stays with probability 1−δ, the paper proves P(τ<∞)=1, E[τ | X0=s1]=4/δ, and P(τ>k) ≤ α(1−δ)^k with α=||(I−Q)^{-1}||. The proof treats the time in each stage as a geometric random variable with mean 1/δ and sums the four independent sojourn times; the tail bound uses the spectral radius of the upper-triangular transient matrix Q, whose diagonal entries are all 1−δ. The empirical campaign—10,000 trials per δ in {0.1,...,0.9}—finds 100% convergence, empirical means with

What carries the argument

The load-bearing object is the sequential absorbing Markov chain with the canonical transition matrix P = [[Q, R], [0, I]]. Q is a 4×4 upper-triangular matrix with diagonal 1−δ and superdiagonal δ; its fundamental matrix N=(I−Q)^{-1} gives expected visits, and the geometric sojourn time M_j ∼ Geom(δ) in each stage—mean 1/δ—makes E[τ]=4/δ by linearity of expectation. The spectral radius of Q, 1−δ, is used to claim the exponential tail bound. Supporting machinery includes a vectorized Monte Carlo simulator that samples the four geometric residence times directly and a sliding-window estimator of δ for runtime calibration.

Load-bearing premise

The whole theorem depends on the assumption—stated in Section 4.1 and conceded in Sections 6.2.1 and 6.2.2—that the LLM-verifier process is a time-homogeneous absorbing Markov chain with the same constant δ at every stage and independent, memoryless retries; if real LLM behavior is non-stationary or stage-correlated, E[τ]=4/δ no longer follows.

What would settle it

Compute P(τ>k) for the four-stage chain explicitly: τ is the sum of four independent Geom(δ) variables, so its survival function contains a k^3 polynomial factor alongside (1−δ)^k; if the claimed bound P(τ>k) ≤ α(1−δ)^k with a single constant α is checked numerically across all k, it fails for large k. A complementary experiment: instrument a real LLM-plus-verifier pipeline to log per-stage success rates and retry counts; if the measured δ_i differ across stages or correlate across attempts, the predicted mean 4/δ will not match.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Systems modeled this way are guaranteed to terminate almost surely; no infinite oscillation between syntax errors and logical failures under the stated assumptions.
  • Expected pipeline latency is 4/δ attempts, so δ becomes a budgeting parameter rather than a guess.
  • The exponential tail gives a principled way to set timeouts: choose k so that α(1−δ)^k is below the acceptable failure probability.
  • δ thresholds define operating regions (marginal below 0.3, practical 0.3–0.6, high-performance above 0.6), guiding model selection and effort allocation.
  • Runtime monitoring of δ with a sliding window lets engineers trigger corrective actions, such as context resets or temperature changes, when performance drifts.

Where Pith is reading between the lines

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

  • An analogous m-stage pipeline would have expected time m/δ, so splitting or merging verification stages is a direct design lever on latency, an implication the paper leaves implicit.
  • If per-stage success probabilities are unequal (δ1,...,δ4), the same argument gives E[τ]=Σ 1/δ_i; measuring stage-level success rates would let practitioners test whether the uniform-δ assumption matters in practice.
  • The model abstracts away token-level generation cost; converting 4/δ iterations into dollars or wall-clock time requires multiplying by per-attempt cost, a step the paper does not take.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

5 major / 3 minor

Summary. The paper models LLM-verifier refinement as a four-stage absorbing Markov chain with per-stage success probability δ and states an 'LLM-Verifier Convergence Theorem' (Section 4.2): almost-sure absorption, E[τ|X0=s1]=4/δ, and an exponential tail bound P(τ>k)≤α(1−δ)^k. It reports a 90,000-trial Monte Carlo campaign, claims the empirical ratio Cf≈1.0 confirms the 4/δ bound, and proposes operational regions and dynamic calibration.

Significance. The expectation and almost-sure parts of the theorem are correct for the stated abstract chain, and the paper is clear about the model and makes its simulator code available. However, the advertised exponential tail bound is false for the paper's own chain, and the empirical campaign is circular: the simulator generates M_{i,j}∼Geom(δ) and sums four such variables, exactly the quantity whose mean the theorem computes. Consequently, the paper's central claim of a provable, empirically confirmed convergence guarantee for LLM-verifier systems is not established. The value of the contribution, if the theorem were corrected, would be modest: a standard negative-binomial calculation for a stylized four-stage retry process.

major comments (5)
  1. [§4.2, Theorem 1, Part 3] The tail bound P(τ>k|X0=s1)≤α(1−δ)^k is false for the stated chain. The proof passes from the spectral radius of Q to a norm bound, but Q is non-normal, so ρ(Q)^k does not bound ||Q^k||. In fact τ is a sum of four independent Geom(δ) variables, so P(τ>k)=∑_{n=k+1}^{∞} C(n−1,3)δ^4(1−δ)^{n−4}; this negative-binomial tail is asymptotically c_δ k^3(1−δ)^k. No finite α can dominate this polynomial factor for all k. The exact statement is a polynomial-prefactor tail, not α(1−δ)^k.
  2. [Table 8 and §6.1.4] The paper's own data contradict Part 3 of Theorem 1. At δ=0.1, Table 8 reports P99=97, so roughly 1% of trials have τ>97. With α=||(I−Q)^{−1}||=4/δ=40, the claimed bound gives 40·(0.9)^97≈1.4×10^{−3}, an order of magnitude below the observed tail. Similar checks hold at δ=0.2 (P99=47). Thus the empirical tail analysis, which is used to justify reliable timeouts, actually refutes the stated bound.
  3. [§5.2.2, Eq. (8) and §6.2.2] The empirical 'stress test' is circular. Eq. (8) samples residence times M_{i,j}∼Geom(δ) and defines T_i as their sum over four stages; Theorem 1's E[τ]=4/δ is exactly the mean of that sum. Cf≈1.0 is therefore a property of the random-number generator, not evidence about LLM-verifier systems. Section 6.2.2 concedes that only simulated behavior was tested and real API validation is future work, yet the abstract and conclusions describe conclusive support for the framework's applicability to real systems.
  4. [§3.1.3, Eq. (7)] The paper contains an internal inconsistency in the central expected value. Eq. (7) states E[n]=(4−3δ)/δ=4/δ−3 for 'the specific chain structure analyzed in this paper', while Theorem 1 and Table 8 use E[τ]=4/δ. These cannot both describe the same chain. For the chain defined in §4.1, with each of four transient states occupied for a Geom(δ) sojourn, the correct mean is 4/δ; Eq. (7) should be corrected or removed.
  5. [§4.1 and §6.2.1] The theorem's applicability to actual LLM-verifier systems depends on assumptions that are asserted but never tested: time-homogeneous per-stage success probability δ, independence of sojourns across stages, and memoryless retries. Section 6.2.1 acknowledges non-stationarity and Section 8.1 defers real API validation to future work. This would be acceptable if the paper were framed purely as an analysis of a stylized retry model, but the title, abstract, and conclusions claim guarantees for 'LLM-verifier systems' and 'formal method guarantee'. That external-validity gap is load-bearing for the paper's stated contribution.
minor comments (3)
  1. [Table 8] The first row is typeset as '0.140.000'; it should presumably be '0.1 40.000'. The header alignment should be fixed.
  2. [§5.1 and §6.1.4] The methodology repeatedly states P(n>k)∝e^{−cδk} without defining c and without reconciling this form with the theorem's α(1−δ)^k or with the negative-binomial tail acknowledged in §7.3. These three tail statements should be unified.
  3. [§5.2.3] Defining 'Success' as τ≤1000 and reporting 100% success in Table 8 is uninformative because a sum of four geometric variables with δ≥0.1 has P(τ>1000) astronomically small; this metric cannot validate or illustrate almost-sure convergence.

Circularity Check

3 steps flagged

Empirical 'stress test' is the theorem's own generative model: Eq. (8) samples M_i,j ~ Geom(δ) and sums four per trial, so C_f≈1.0 is forced by construction; the paper itself concedes real LLM/API validation is future work.

specific steps
  1. self definitional [Section 5.2.2 (Eq. 8) vs. Section 4.2, Theorem 1 Part 2 (Eq. 4 and proof)]
    "Each element M_{i,j} represents the residence time in stage j for trial i, sampled independently from a Geometric distribution, as defined in Eq. (8). M_{i,j} ∼ Geom(δ) ∀i∈[1,N], j∈[1,4] ... The total convergence time T_i for the i-th trial is computed via row-wise summation, T_i = Σ_{j=1}^{4} M_{i,j}."

    Theorem 1 derives E[τ|X0=s1]=4/δ by writing τ=Σ_{j=1}^{4} M_j with M_j∼Geom(δ). The simulator generates exactly this: four independent Geom(δ) draws summed per trial. Therefore the empirical mean is produced by the same distributional identity the theorem states, and C_f=(4/δ)/µ≈1.0 is an artifact of the sampler rather than a test of any LLM-verifier system. The abstract calls this a 'stress-tested prediction' and Section 7.1 calls it 'decisive confirmation,' but no real system data enters the loop.

  2. self definitional [Section 7.3, RQ4 discussion]
    "The structure of the empirical data strongly confirms that the convergence time follows a Negative Binomial distribution with parameter r=4. Since a Negative Binomial(r, p) distribution describes the sum of r independent Geometric variables, this empirical fit mathematically validates our modeling assumption that the process consists of exactly four independent, sequential refinement stages."

    The empirical data were generated by Eq. (8) as row-wise sums of four independent Geom(δ) variables. A Negative Binomial fit is therefore guaranteed by the simulation construction. Citing that fit as 'mathematically validating' the four-stage independent-Geometric assumption restates the simulator's input rather than providing independent evidence for the Markovian model.

  3. other [Section 6.2.2, External Validity]
    "Experiments use modeled behavior (sum of independent Geometric distributions); validation with real LLM and application programming interfaces (APIs) is future work."

    This is the paper's own admission that the 90,000-trial campaign was not an empirical test of real LLM-verifier pipelines. Combined with Eq. (8), it confirms that the claimed validation of E[n]≤4/δ and C_f≈1.0 is a check of the model against itself: the 'prediction' and the 'data' share the same definitional distribution. This makes the central empirical claim circular by construction.

full rationale

The theoretical derivation itself is not circular: given a four-stage absorbing Markov chain with per-stage success δ, E[τ]=4/δ follows from E[Geom(δ)]=1/δ and linearity of expectation. That conditional statement is a standard mathematical result, and the paper's Markovian modeling assumptions are at least stated explicitly. The circularity is in the validation loop. Section 5.2.2's simulator instantiates M_{i,j}∼Geom(δ) and sums four such draws per trial, which is precisely the construction Theorem 1 uses to compute E[τ]=4/δ. Hence the empirical mean, C_f≈1.0, and the Negative Binomial fit are forced by the simulator's definition; they cannot confirm that real LLM-verifier behavior follows the model. Section 6.2.2 concedes exactly this: 'validation with real LLM and APIs is future work.' The false tail bound in Theorem 1 Part 3 is a genuine mathematical error—the negative-binomial tail has a k^3(1−δ)^k factor, so no constant α suffices—but I did not count it as circularity because it is unsoundness rather than a definitional reduction. The score of 8 reflects that the paper's headline empirical confirmation is equivalent, by construction, to its own input distribution, while the underlying Markov-chain calculation itself is not circular.

Axiom & Free-Parameter Ledger

1 free parameters · 4 axioms · 0 invented entities

The model's load-bearing input is a single fixed δ per stage, plus the Markov/stationarity assumptions. No new physical or mathematical entities are introduced. The false norm assumption in the tail bound is an ad hoc technical premise that breaks the theorem as stated.

free parameters (1)
  • δ
    Per-stage success probability; assumed identical across four stages and stationary. Not estimated from real LLM runs; swept 0.1-0.9 in simulation. The entire E=4/δ bound is inversely proportional to this one number.
axioms (4)
  • domain assumption LLM-verifier refinement is a time-homogeneous absorbing Markov chain with exactly four transient stages and self-loop retries (CodeGen, Compilation, InvariantSynth, SMTSolving).
    Invoked in Section 4.1 to define Theorem 1; no real-system data show transitions are memoryless or that retries stay in the same stage.
  • domain assumption A single fixed success probability δ governs all four stages and remains constant over time.
    Theorem 1 states 'fixed success probability δ∈(0,1]'; Section 6.2.1 concedes non-stationarity and stage differences are future work.
  • standard math Standard absorbing Markov chain facts: absorption is almost sure when the absorbing state is reachable, and expected absorption time is N1.
    Used in Section 3.1.3 and proof of Theorem 1 Parts 1-2.
  • ad hoc to paper The transient matrix Q satisfies ||Q^k|| ≤ ρ(Q)^k = (1−δ)^k.
    Assumed in Theorem 1 Part 3 proof; false for this non-normal upper-triangular Q, whose true tail has polynomial factor k^3(1−δ)^k.

pith-pipeline@v1.3.0-alltime-deepseek · 28956 in / 17390 out tokens · 167343 ms · 2026-08-03T19:17:25.237271+00:00 · methodology

0 comments
read the original abstract

The integration of Formal Verification tools with Large Language Models (LLMs) offers a path to scale software verification beyond manual workflows. However, current methods remain unreliable: without a solid theoretical footing, the refinement process acts as a black box that may oscillate, loop, or diverge. This work bridges this critical gap by developing an LLM-Verifier Convergence Theorem, providing the first formal framework with provable guarantees for termination in multi-stage verification pipelines. We model the interaction not as a generic loop, but as a sequential absorbing Markov Chain comprising four essential engineering stages: \texttt{CodeGen}, \texttt{Compilation}, \texttt{InvariantSynth}, and \texttt{SMTSolving}. We prove that for any non-zero stage success probability ($\delta > 0$), the system reaches the \texttt{Verified} state almost surely. Furthermore, because of the sequential nature of the pipeline, we derive a precise latency bound of $\mathbb{E}[n] \leq 4/\delta$. We stress-tested this prediction in an extensive empirical campaign comprising over 90,000 trials. The results match the theory with striking consistency: every run reached verification, and the empirical convergence factor clustered tightly around $C_f\approx 1.0$, confirming that the $4/\delta$ bound accurately mirrors system behavior rather than serving as a loose buffer. Based on this data, we identify three distinct operating zones -- marginal, practical, and high-performance -- and propose a dynamic calibration strategy to handle parameter drift in real-world environments. Together, these contributions replace heuristic guesswork with a rigorous architectural foundation, enabling predictable resource planning and performance budgeting for safety-critical software.

discussion (0)

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

Reference graph

Works this paper leans on

97 extracted references · 16 canonical work pages · 5 internal anchors

  1. [1]

    Computer51(11), 14–23 (2018) https://doi.org/10.1109/mc

    Cofer, D., Gacek, A., Backes, J., Whalen, M.W., Pike, L., Foltzer, A., Podhradsky, M., Klein, G., Kuz, I., Andronick, J., Heiser, G., Stuart, D.: A Formal Approach to Construct- ing Secure Air Vehicle Software. Computer51(11), 14–23 (2018) https://doi.org/10.1109/mc. 2018.2876051

    arXiv 2018

  2. [2]

    In: 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems, pp

    Hatcliff, J., King, A., Lee, I., Macdonald, A., Fernando, A., Robkin, M., Vasserman, E., Weininger, S., Goldman, J.M.: Rationale and Architecture Principles for Medical Application Platforms. In: 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems, pp. 3–12. IEEE, Beijing, China (2012). https://doi.org/10.1109/iccps.2012.9

    doi:10.1109/iccps.2012.9 2012

  3. [3]

    ACM Computing Surveys52(5), 1–41 (2019) https://doi.org/10.1145/3342355

    Luckcuck, M., Farrell, M., Dennis, L.A., Dixon, C., Fisher, M.: Formal Specification and Ver- ification of Autonomous Robotic Systems: A Survey. ACM Computing Surveys52(5), 1–41 (2019) https://doi.org/10.1145/3342355

    doi:10.1145/3342355 2019

  4. [4]

    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs, pp. 193–207. Springer, Berlin, Heidelberg (1999). https://doi.org/10.1007/3-540-49059-0_14

    doi:10.1007/3-540-49059-0_14 1999

  5. [5]

    In: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering

    Gadelha, M.R., Monteiro, F.R., Morse, J., Cordeiro, L.C., Fischer, B., Nicole, D.A.: ESBMC 5.0: an Industrial-Strength C Model Checker. In: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering. ASE’18, pp. 888–891. ACM, Manchester, UK (2018). https://doi.org/10.1145/3238147.3240481

    arXiv 2018

  6. [6]

    IEEE Transactions on Software Engineering38(4), 957–974 (2012) https://doi.org/10.1109/tse.2011.59

    Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-Based Bounded Model Checking for Embed- ded ANSI-C Software. IEEE Transactions on Software Engineering38(4), 957–974 (2012) https://doi.org/10.1109/tse.2011.59

    doi:10.1109/tse.2011.59 2012

  7. [7]

    Springer, Cham, Switzerland (2018)

    Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R.: Handbook of Model Checking. Springer, Cham, Switzerland (2018). https://doi.org/10.1007/978-3-319-10575-8

    doi:10.1007/978-3-319-10575-8 2018

  8. [8]

    ACM Computing Surveys41(4), 1–36 (2009) https://doi.org/10.1145/1592434

    Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal Methods: Practice and Experience. ACM Computing Surveys41(4), 1–36 (2009) https://doi.org/10.1145/1592434. 1592436

    doi:10.1145/1592434 2009

  9. [9]

    In: Proceedings 2025 Network and Distributed System Security Symposium (2025)

    Liu, Y., Xue, Y., Wu, D., Sun, Y., Li, Y., Shi, M., Liu, Y.: PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation. In: Proceedings 2025 Network and Distributed System Security Symposium (2025). https: //doi.org/10.14722/ndss.2025.241357 . Internet Society

    arXiv 2025

  10. [10]

    In: Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, pp

    Pirzada, M.A.A., Reger, G., Bhayat, A., Cordeiro, L.C.: LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling. In: Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, pp. 1395–1407 (2024). https: //doi.org/10.1145/3691620.3695512 . ACM

    arXiv 2024

  11. [11]

    In: 2025 IEEE/ACM International Conference on Automation of Software Test (AST), pp

    Tihanyi, N., Charalambous, Y., Jain, R., Ferrag, M.A., Cordeiro, L.C.: A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification. In: 2025 IEEE/ACM International Conference on Automation of Software Test (AST), pp. 136–147 (2025). https://doi.org/10.1109/ast66626.2025.00020 . IEEE

    arXiv 2025

  12. [12]

    arxiv (2017)

    Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A.N., Kaiser, L., Polosukhin, I.: Attention Is All You Need. arxiv (2017). https://doi.org/10.48550/arxiv.1706. 03762

    doi:10.48550/arxiv.1706 2017

  13. [13]

    arxiv (2022)

    Wei, J., Tay, Y., Bommasani, R., Raffel, et al.: Emergent Abilities of Large Language Models. arxiv (2022). https://doi.org/10.48550/arxiv.2206.07682 30

    Pith/arXiv arXiv doi:10.48550/arxiv.2206.07682 2022

  14. [14]

    Beckert, B., Klamroth, J., Pfeifer, W., Röper, P., Teuber, S.: Towards Combining the Cognitive Abilities of Large Language Models with the Rigor of Deductive Progam Verification, pp. 242–257. Springer, Cham, Switzerland (2024). https://doi.org/10.1007/978-3-031-75387-9_15

    doi:10.1007/978-3-031-75387-9_15 2024

  15. [15]

    arxiv (2023)

    Huang, X., Ruan, W., Huang, W., Jin, G., Dong, et al.: A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation. arxiv (2023). https: //doi.org/10.48550/arxiv.2305.11391

    Pith/arXiv arXiv doi:10.48550/arxiv.2305.11391 2023

  16. [16]

    Neural Information Processing Systems (2024) https://doi.org/10.48550/arxiv.2406.14408

    Lin, X., Cao, Q., Huang, Y., Wang, H., Lu, J., Liu, Z., Song, L., Liang, X.: FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving. Neural Information Processing Systems (2024) https://doi.org/10.48550/arxiv.2406.14408

    Pith/arXiv arXiv doi:10.48550/arxiv.2406.14408 2024

  17. [17]

    https://doi.org/10.48550/arxiv.2410.02724

    Zekri, O., Odonnat, A., Benechehab, A., Bleistein, L., Boullé, N., Redko, I.: Large Language Models as Markov Chains (2024). https://doi.org/10.48550/arxiv.2410.02724

    Pith/arXiv arXiv doi:10.48550/arxiv.2410.02724 2024

  18. [18]

    VerifierQ: Enhancing LLM Test Time Compute with Q-Learning-based Verifiers

    Qi, J., Tang, H., Zhu, Z.: VerifierQ: Enhancing LLM Test Time Compute with Q-Learning- based Verifiers (2024). https://doi.org/10.48550/arxiv.2410.08048

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2410.08048 2024

  19. [19]

    Software Testing, Verification and Reliability32(1) (2021) https://doi.org/10.1002/stvr.1793

    Monteiro, F.R., Gadelha, M.R., Cordeiro, L.C.: Model Checking C++ Programs. Software Testing, Verification and Reliability32(1) (2021) https://doi.org/10.1002/stvr.1793

    doi:10.1002/stvr.1793 2021

  20. [20]

    arxiv.org (2023) https://doi.org/10.48550/arxiv.2309.09437

    Orenes-Vera, M., Martonosi, M., Wentzlaff, D.: Using LLMs to Facilitate Formal Verification of RTL. arxiv.org (2023) https://doi.org/10.48550/arxiv.2309.09437

    Pith/arXiv arXiv doi:10.48550/arxiv.2309.09437 2023

  21. [21]

    In:Proceedings of the31st ACM JointEuropean Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp

    First, E., Rabe, M.N., Ringer, T., Brun, Y.: Baldur: Whole-Proof Generation and Repair with Large LanguageModels. In:Proceedings of the31st ACM JointEuropean Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 1229–1241 (2023). https://doi.org/10.1145/3611643.3616243 . ACM

    arXiv 2023

  22. [22]

    arxiv (2024) https://doi.org/10.48550/arxiv.2406.08467

    Loughridge, C., Sun, Q., Ahrenbach, S., Cassano, F., Sun, C., Sheng, Y., Mudide, A., Misu, M.R.H., Amin, N., Tegmark, M.: DafnyBench: A Benchmark for Formal Software Verification. arxiv (2024) https://doi.org/10.48550/arxiv.2406.08467

    Pith/arXiv arXiv doi:10.48550/arxiv.2406.08467 2024

  23. [23]

    Proceedings of the ACM on Software Engineering1, 812–835 (2024) https://doi.org/ 10.1145/3643763

    Misu, M.R.H., Lopes, C.V., Ma, I., Noble, J.: Towards AI-Assisted Synthesis of Verified Dafny Methods. Proceedings of the ACM on Software Engineering1, 812–835 (2024) https://doi.org/ 10.1145/3643763

    doi:10.1145/3643763 2024

  24. [24]

    https: //doi.org/10.48550/arxiv.2201.11903

    Wei, J., Wang, X., Schuurmans, D., Bosma, M., Ichter, B., Xia, F., Chi, E., Le, Q., Zhou, D.: Chain-of-Thought Prompting Elicits Reasoning in Large Language Models (2022). https: //doi.org/10.48550/arxiv.2201.11903

    Pith/arXiv arXiv doi:10.48550/arxiv.2201.11903 2022

  25. [25]

    arxiv (2024)

    Charalambous, Y., Manino, E., Cordeiro, L.C.: Automated Repair of AI Code with Large Language Models and Formal Verification. arxiv (2024). https://doi.org/10.48550/arxiv.2405. 08848

    doi:10.48550/arxiv.2405 2024

  26. [26]

    arxiv (2025)

    Fakih, M., Dharmaji, R., Bouzidi, H., Araya, G.Q., Ogundare, O., Faruque, M.A.A.: LLM4CVE: Enabling Iterative Automated Vulnerability Repair with Large Language Models. arxiv (2025). https://doi.org/10.48550/arxiv.2501.03446

    Pith/arXiv arXiv doi:10.48550/arxiv.2501.03446 2025

  27. [27]

    Supporting Software Formal Verification with Large Language Models: An Experimental Study

    Wang, W., Farrell, M., Cordeiro, L.C., Zhao, L.: Supporting Software Formal Verification with Large Language Models: An Experimental Study. arxiv.org (2025) https://doi.org/10.48550/ arxiv.2507.04857

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2507.04857 2025

  28. [28]

    Sensors 25(9), 2683 (2025) https://doi.org/10.3390/s25092683

    Deng, L., Zhong, Q., Song, J., Lei, H., Li, W.: LLM-Based Unknown Function Automated Modeling in Sensor-Driven Systems for Multi-Language Software Security Verification. Sensors 25(9), 2683 (2025) https://doi.org/10.3390/s25092683

    work page doi:10.3390/s25092683 2025

  29. [29]

    arxiv.org (2023) https://doi.org/10.48550/arxiv.2311.03739

    Yao, J., Zhou, Z., Chen, W., Cui, W.: Leveraging Large Language Models for Automated Proof 31 Synthesis in Rust. arxiv.org (2023) https://doi.org/10.48550/arxiv.2311.03739

    Pith/arXiv arXiv doi:10.48550/arxiv.2311.03739 2023

  30. [30]

    arxiv (2023)

    Jiang, H., Wu, Q., Lin, C.-Y., Yang, Y., Qiu, L.: LLMLingua: Compressing Prompts for Accel- erated Inference of Large Language Models. arxiv (2023). https://doi.org/10.48550/arxiv.2310. 05736

    doi:10.48550/arxiv.2310 2023

  31. [31]

    Transactions of the Association for Computational Linguistics12, 1556–1577 (2024) https://doi.org/10.1162/tacl_a_00704

    Zhu, X., Li, J., Liu, Y., Ma, C., Wang, W.: A Survey on Model Compression for Large Language Models. Transactions of the Association for Computational Linguistics12, 1556–1577 (2024) https://doi.org/10.1162/tacl_a_00704

    doi:10.1162/tacl_a_00704 2024

  32. [32]

    In: Findings of the Association for Computational Linguistics: EMNLP 2024, pp

    Wang, W., Mao, Y., Dongdong, T., Hongchao, D., Guan, N., Xue, C.J.: When Compression Meets Model Compression: Memory-Efficient Double Compression for Large Language Models. In: Findings of the Association for Computational Linguistics: EMNLP 2024, pp. 16973–16983. Association for Computational Linguistics, Miami, Florida, USA (2024). https://doi.org/10. 1...

    2024

  33. [33]

    Applied Intelligence54(22), 11804–11844(2024) https://doi.org/10.1007/s10489-024-05747-w

    Dantas, P.V., Silva, W., Cordeiro, L.C., Carvalho, C.B.: A Comprehensive Review of Model Compression Techniques in Machine Learning. Applied Intelligence54(22), 11804–11844(2024) https://doi.org/10.1007/s10489-024-05747-w

    doi:10.1007/s10489-024-05747-w 2024

  34. [34]

    ACM Computing Surveys57(10), 1–39 (2025) https: //doi.org/10.1145/3728636

    Kim, G.I., Hwang, S., Jang, B.: Efficient Compressing and Tuning Methods for Large Language Models: A Systematic Literature Review. ACM Computing Surveys57(10), 1–39 (2025) https: //doi.org/10.1145/3728636

    work page doi:10.1145/3728636 2025

  35. [35]

    Scientific Reports15(1) (2025) https://doi.org/10.1038/ s41598-025-92586-5

    Belhaouari, S.B., Kraidia, I.: Efficient Self-attention with Smart Pruning for Sustain- able Large Language Models. Scientific Reports15(1) (2025) https://doi.org/10.1038/ s41598-025-92586-5

    2025

  36. [36]

    Optimizing Singular Spectrum for Large Language Model Compression

    Li, D., Shen, T., Zhou, Y., Yang, B., Liu, Z., Yang, M., Ghanem, B., Yang, Y., Zhong, Y., Yang, M.-H.: Optimizing Singular Spectrum for Large Language Model Compression (2025). https://doi.org/10.48550/arxiv.2502.15092

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2502.15092 2025

  37. [37]

    Complex & Intelligent Systems11(9) (2025) https://doi.org/ 10.1007/s40747-025-02019-z

    Dantas, P.V., Cordeiro, L.C., Junior, W.S.S.: A Review of State-of-the-art Techniques for Large Language Model Compression. Complex & Intelligent Systems11(9) (2025) https://doi.org/ 10.1007/s40747-025-02019-z

    work page doi:10.1007/s40747-025-02019-z 2025

  38. [38]

    arxiv (2025)

    Tihanyi, N., Bisztray, T., Ferrag, M.A., Cherif, B., Dubniczky, R.A., Jain, R., Cordeiro, L.C.: Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview. arxiv (2025). https://doi.org/10.48550/arxiv.2503. 10784

    doi:10.48550/arxiv.2503 2025

  39. [39]

    https://doi.org/10.48550/arxiv.2310.04870

    Wu, H., Barrett, C., Narodytska, N.: Lemur: Integrating Large Language Models in Automated Program Verification (2023). https://doi.org/10.48550/arxiv.2310.04870

    Pith/arXiv arXiv doi:10.48550/arxiv.2310.04870 2023

  40. [40]

    Enhancing Large Language Model Efficiencyvia Symbolic Compression: A Formal Approach Towards Interpretability

    AI, L., School, T.N..M., Ji, S., Song, Z., Zhong, F., Jia, J., Wu, Z., Cao, Z., Xu, T.: Enhanc- ing Large Language Model Efficiencyvia Symbolic Compression: A Formal Approach Towards Interpretability (2025). https://doi.org/10.48550/arxiv.2501.18657

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2501.18657 2025

  41. [41]

    Proceedings of the AAAI Conference on Artificial Intelligence28(1) (2014) https://doi.org/ 10.1609/aaai.v28i1.8843

    Ermon, S., Gomes, C., Sabharwal, A., Selman, B.: Designing Fast Absorbing Markov Chains. Proceedings of the AAAI Conference on Artificial Intelligence28(1) (2014) https://doi.org/ 10.1609/aaai.v28i1.8843

    work page doi:10.1609/aaai.v28i1.8843 2014

  42. [42]

    Health Economics11(1), 33–42 (2002) https://doi.org/10.1002/hec.654

    Craig, B.A., Sendi, P.P.: Estimation of the Transition Matrix of a Discrete-Time Markov Chain. Health Economics11(1), 33–42 (2002) https://doi.org/10.1002/hec.654

    work page doi:10.1002/hec.654 2002

  43. [43]

    Clarke, E.M.: Model Checking, pp. 54–56. Springer, Berlin, Heidelberg, Germany (1997). https: //doi.org/10.1007/bfb0058022 32

    doi:10.1007/bfb0058022 1997

  44. [44]

    arxiv (2022) https://doi.org/10.48550/arxiv.2205.10625

    Zhou,D.,Schärli,N.,Hou,L.,Wei,J.,Scales,N.,Wang,X.,Schuurmans,D.,Cui,C.,Bousquet, O., Le, Q., Chi, E.: Least-to-Most Prompting Enables Complex Reasoning in Large Language Models. arxiv (2022) https://doi.org/10.48550/arxiv.2205.10625

    Pith/arXiv arXiv doi:10.48550/arxiv.2205.10625 2022

  45. [45]

    In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

    Staton, S., Yang, H., Wood, F., Heunen, C., Kammar, O.: Semantics for Probabilistic Program- ming: Higher-order Functions, Continuous Distributions, and Soft Constraints. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. LICS’16, pp. 525–534. ACM, New York, NY, USA (2016). https://doi.org/10.1145/2933575.2935313

    arXiv 2016

  46. [46]

    Communications of the ACM59(7), 107–115 (2016) https://doi.org/10.1145/2936726

    Gogate, V., Domingos, P.: Probabilistic theorem proving. Communications of the ACM59(7), 107–115 (2016) https://doi.org/10.1145/2936726

    work page doi:10.1145/2936726 2016

  47. [47]

    Springer, Berlin, Heidelberg, Germany (2016)

    Kroening, D., Strichman, O.: Decision Procedures. Springer, Berlin, Heidelberg, Germany (2016). https://doi.org/10.1007/978-3-662-50497-0

    doi:10.1007/978-3-662-50497-0 2016

  48. [48]

    Clarke, E., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs, pp. 168–176. Springer, Berlin, Heidelberg, Germany (2004). https://doi.org/10.1007/978-3-540-24730-2_15

    doi:10.1007/978-3-540-24730-2_15 2004

  49. [49]

    Communications of the ACM9(5), 366–371 (1966) https://doi.org/10.1145/ 355592.365646

    Böhm, C., Jacopini, G.: Flow Diagrams, Turing Machines and Languages with Only Two Formation Rules. Communications of the ACM9(5), 366–371 (1966) https://doi.org/10.1145/ 355592.365646

    arXiv 1966

  50. [50]

    Rozier, K.Y., Dureja, R., Irfan, A., Johannsen, C., Nukala, K., Shankar, N., Tinelli, C., Vardi, M.Y.: MoXI: An Intermediate Language for Symbolic Model Checking, pp. 26–46. Springer, Cham, Switzerland (2024). https://doi.org/10.1007/978-3-031-66149-5_2

    work page doi:10.1007/978-3-031-66149-5_2 2024

  51. [51]

    Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons Using Branch- ing Time Temporal Logic, pp. 52–71. Springer, Berlin, Heidelberg, Germany (1982). https: //doi.org/10.1007/bfb0025774

    doi:10.1007/bfb0025774 1982

  52. [52]

    Clarke, E.M.: The Birth of Model Checking, pp. 1–26. Springer, Berlin, Heidelberg, Germany (2008). https://doi.org/10.1007/978-3-540-69850-0_1

    work page doi:10.1007/978-3-540-69850-0_1 2008

  53. [53]

    In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp

    Pnueli, A.: The Temporal Logic of Programs. In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp. 46–57. IEEE, Providence, RI, USA (1977). https://doi.org/ 10.1109/sfcs.1977.32

    doi:10.1109/sfcs.1977.32 1977

  54. [54]

    Sometimes

    Emerson, E.A., Halpern, J.Y.: “Sometimes” and “Not Never” Revisited: on Branching versus Linear Time (Preliminary Report). In: Proceedings of the 10th ACM SIGACT-SIGPLAN Sym- posium on Principles of Programming Languages - POPL’83. POPL’83, pp. 127–140. ACM Press, New York, NY, United States (1983). https://doi.org/10.1145/567067.567081

    arXiv 1983

  55. [55]

    Proceedings of the IEEE103(11), 2021–2035 (2015) https://doi.org/10

    Vizel, Y., Weissenbacher, G., Malik, S.: Boolean Satisfiability Solvers and Their Applications in Model Checking. Proceedings of the IEEE103(11), 2021–2035 (2015) https://doi.org/10. 1109/jproc.2015.2455034

    arXiv 2021

  56. [56]

    IEEE Transactions on ComputersC–35(8), 677–691 (1986) https://doi.org/10.1109/tc.1986.1676819

    Bryant: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on ComputersC–35(8), 677–691 (1986) https://doi.org/10.1109/tc.1986.1676819

    arXiv 1986

  57. [57]

    Formal Methods in System Design19(1), 7–34 (2001) https://doi.org/10.1023/a: 1011276507260

    Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design19(1), 7–34 (2001) https://doi.org/10.1023/a: 1011276507260

    doi:10.1023/a: 2001

  58. [58]

    Menezes, R.S., Aldughaim, M., Farias,et al.: ESBMC v7.4: Harnessing the Power of Intervals: (Competition Contribution), pp. 376–380. Springer, Luxembourg City, Luxembourg (2024). https://doi.org/10.1007/978-3-031-57256-2_24

    doi:10.1007/978-3-031-57256-2_24 2024

  59. [59]

    Clarke, E.M., Klieber, W., Nováček, M., Zuliani, P.: Model Checking and the State Explosion 33 Problem, pp. 1–30. Springer, Berlin, Heidelberg, Germany (2012). https://doi.org/10.1007/ 978-3-642-35746-6_1

    2012

  60. [60]

    In: 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering, pp

    Dhaussy, P., Roger, J.-C., Boniol, F.: Reducing State Explosion with Context Modeling for Model-Checking. In: 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering, pp. 130–137. IEEE, Boca Raton, FL, USA (2011). https://doi.org/10.1109/hase. 2011.24

    doi:10.1109/hase 2011

  61. [61]

    Mukherjee, R., Tautschnig, M., Kroening, D.: v2c – A Verilog to C Translator, pp. 580–586. Springer, Berlin, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_38

    work page doi:10.1007/978-3-662-49674-9_38 2016

  62. [62]

    Donaldson, A.F., Haller, L., Kroening, D., Rümmer, P.: Software Verification Using k-Induction, pp. 351–368. Springer, Berlin, Heidelberg (2011). https://doi.org/10.1007/ 978-3-642-23702-7_26

    2011

  63. [63]

    Barrett, C., Tinelli, C.: Satisfiability Modulo Theories, pp. 305–343. Springer, Cham, Switzer- land (2018). https://doi.org/10.1007/978-3-319-10575-8_11

    doi:10.1007/978-3-319-10575-8_11 2018

  64. [64]

    In: 2011 Brazilian Symposium on Computing System Engineering, pp

    Barreto, R., Cordeiro, L., Fischer, B.: Verifying Embedded C Software with Timing Constraints Using an Untimed Bounded Model Checker. In: 2011 Brazilian Symposium on Computing System Engineering, pp. 46–52. IEEE, Los Alamitos, CA, USA (2011). https://doi.org/10. 1109/sbesc.2011.19

    2011

  65. [65]

    Brummayer, R., Biere, A.: Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays, pp. 174–177. Springer, Berlin, Heidelberg, Germany (2009). https://doi.org/10.1007/ 978-3-642-00768-2_16

    2009

  66. [66]

    In: 2016 Formal Methods in Computer-Aided Design (FMCAD), pp

    Ho, Y.-S., Chauhan, P., Roy, P., Mishchenko, A., Brayton, R.: Efficient Uninterpreted Function Abstraction and Refinement for Word-Level Model Checking. In: 2016 Formal Methods in Computer-Aided Design (FMCAD), pp. 65–72. IEEE, Mountain View, CA, USA (2016). https: //doi.org/10.1109/fmcad.2016.7886662

    arXiv 2016

  67. [67]

    Electronic Notes in Theoretical Computer Science75, 95–113 (2003) https://doi.org/10.1016/s1571-0661(04)80781-3

    Tabuchi, N., Sumii, E., Yonezawa, A.: Regular Expression Types for Strings in a Text Processing Language. Electronic Notes in Theoretical Computer Science75, 95–113 (2003) https://doi.org/10.1016/s1571-0661(04)80781-3

    work page doi:10.1016/s1571-0661(04)80781-3 2003

  68. [68]

    arxiv (2020) https://doi.org/10.48550/arxiv.2005.14165

    Brown, T.B., Mann, B., Ryder, N., Subbiah, M., Kaplan,et al.: Language Models are Few-Shot Learners. arxiv (2020) https://doi.org/10.48550/arxiv.2005.14165

    Pith/arXiv arXiv doi:10.48550/arxiv.2005.14165 2020

  69. [69]

    Pearce, H., Ahmad, B., Tan, B., Dolan-Gavitt, B., Karri, R.: Asleep at the Keyboard? Assess- ing the Security of GitHub Copilot’s Code Contributions, vol. 68, pp. 96–105. Association for Computing Machinery (ACM), San Francisco, CA, USA (2025). https://doi.org/10.1145/ 3610721

    2025

  70. [70]

    Zheng, S., Huang, C., Yu, F., Yao, J., Ye, J., Chen, T., Luo, Y., Ding, N., BAI, L., Cui, G., Ye, P.: SCI-Verifier: Scientific Verifier with Thinking (2025) https://doi.org/10.48550/arxiv.2509. 24285

    doi:10.48550/arxiv.2509 2025

  71. [71]

    ACM Computing Surveys51(4), 1–37 (2018) https://doi.org/10.1145/ 3212695

    Allamanis, M., Barr, E.T., Devanbu, P., Sutton, C.: A Survey of Machine Learning for Big Code and Naturalness. ACM Computing Surveys51(4), 1–37 (2018) https://doi.org/10.1145/ 3212695

    2018

  72. [73]

    In: 2023 IEEE/ACM 45th International 34 Conference on Software Engineering (ICSE), pp

    Lemieux, C., Inala, J.P., Lahiri, S.K., Sen, S.: CodaMosa: Escaping Coverage Plateaus in Test Generation with Pre-trained Large Language Models. In: 2023 IEEE/ACM 45th International 34 Conference on Software Engineering (ICSE), pp. 919–931. IEEE, Melbourne, VIC, Australia (2023). https://doi.org/10.1109/icse48619.2023.00085

    arXiv 2023

  73. [74]

    arxiv (2022) https://doi.org/10.48550/arxiv

    Frantar, E., Ashkboos, S., Hoefler, T., Alistarh, D.: GPTQ: Accurate Post-Training Quanti- zation for Generative Pre-trained Transformers. arxiv (2022) https://doi.org/10.48550/arxiv. 2210.17323

    Pith/arXiv arXiv doi:10.48550/arxiv.2210.17323 2022

  74. [75]

    arxiv (2023) https://doi.org/10.48550/arxiv.2305.14314

    Dettmers, T., Pagnoni, A., Holtzman, A., Zettlemoyer, L.: QLoRA: Efficient Finetuning of Quantized LLMs. arxiv (2023) https://doi.org/10.48550/arxiv.2305.14314

    Pith/arXiv arXiv doi:10.48550/arxiv.2305.14314 2023

  75. [76]

    arxiv (2023) https://doi.org/10.48550/arxiv.2301.00774

    Frantar, E., Alistarh, D.: SparseGPT: Massive Language Models Can Be Accurately Pruned in One-Shot. arxiv (2023) https://doi.org/10.48550/arxiv.2301.00774

    Pith/arXiv arXiv doi:10.48550/arxiv.2301.00774 2023

  76. [77]

    arxiv (2015) https://doi.org/10.48550/arxiv.1503.02531

    Hinton, G., Vinyals, O., Dean, J.: Distilling the Knowledge in a Neural Network. arxiv (2015) https://doi.org/10.48550/arxiv.1503.02531

    Pith/arXiv arXiv doi:10.48550/arxiv.1503.02531 2015

  77. [78]

    arxiv (2021) https://doi.org/10.48550/arxiv

    Hu, E.J., Shen, Y., Wallis, P., Allen-Zhu, Z., Li, Y., Wang, S., Wang, L., Chen, W.: LoRA: Low-Rank Adaptation of Large Language Models. arxiv (2021) https://doi.org/10.48550/arxiv. 2106.09685

    Pith/arXiv arXiv doi:10.48550/arxiv.2106.09685 2021

  78. [79]

    In: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis

    Brauße, F., Shmarov, F., Menezes, R., Gadelha, M.R., Korovin, K., Reger, G., Cordeiro, L.C.: ESBMC-CHERI: Towards Verification of C programs for CHERI Platforms with ESBMC. In: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis. ISSTA’22, pp. 773–776. ACM, Seoul, South Korea (2022). https://doi.org/10.1145/ 353376...

    arXiv 2022

  79. [80]

    Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver, pp. 337–340. Springer, Berlin, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    doi:10.1007/978-3-540-78800-3_24 2008

  80. [81]

    In: International Conference on Predictive Models in Software Engineering (2023)

    Tihanyi, N., Bisztray, T., Jain, R., Ferrag, M.A., Cordeiro, L., Mavroeidis, V.: The For- mAI Dataset: Generative AI in Software Security through the Lens of Formal Verification. In: International Conference on Predictive Models in Software Engineering (2023). https: //doi.org/10.1145/3617555.3617874

    arXiv 2023

Showing first 80 references.