Pith. sign in

REVIEW 2 major objections 3 minor 54 references

Model Checking as Program Verification by Abstract Interpretation (Extended Version)

T0 review · 2 major / 3 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read The paper builds a language, MOKA, in which every ACTL or universal $\mu$-calculus formula becomes a program whose collecting semantics returns exactly the counterexamples to that formula.

desk verdict A solid, useful framework with a genuinely incomplete proof in the mu-calculus branch — worth refereeing, but the authors need to repair Corollary B.3. read the letter →

arxiv 2506.05525 v1 pith:WICBQMZD submitted 2025-06-05 cs.LO

Paolo Baldan , Roberto Bruni , Francesco Ranzato , Diletta Rigo This is my paper
classification cs.LO MSC 03B7068Q6068N30
keywords MOKAabstractinterpretationmodelcheckingACTLmodalmu-calculuslocalcompletenesslogicKleenealgebrawithtestscounterexample-guidedrefinement
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

MOKA is a small command language, based on Kleene algebra with tests and a fixpoint operator, whose primitives inspect and extend computation paths. The paper proves that every ACTL formula and every single-variable universal $\mu$-calculus formula can be translated into a MOKA program that filters out exactly the states satisfying the formula; run on a state, the program returns the empty set precisely when the state satisfies the formula, and otherwise it returns the starting state as a counterexample. This recasts model checking as program analysis, so sound over-approximations of program behaviour become sound model checking. The paper then adds a locally complete program logic whose derivable judgements certify that reported alarms are true counterexamples, and whose failed proof obligations indicate how to refine the abstraction.

What carries the argument

The load-bearing device is the frame $\langle\sigma,\Delta\rangle$, a current state paired with the set of states already traversed, organised into stacks; the primitives $p?$, $\neg p?$, $loop?$, $next$, $add$, $reset$, $push$, and $pop$ manipulate these frames. The traversed-state set $\Delta$ and the $loop?$ test are what let finite-state infinite paths be identified with looping traces, which is essential for the encodings of $AF$, $AU$, and least-fixpoint formulae. Stack abstractions are built by lifting a state abstraction through an equivalence adjunction, and LCL judgements combine under-approximation with over-approximation so that derivable conclusions are both reachability facts and locally complete abstract steps.

What would settle it

On the infinite transition system with states $\sigma_0 \to \sigma_1 \to \cdots$ and with no atomic proposition $p$ ever true, run the MOKA encoding of $AF\,p$: every finite prefix is non-repeating, so $loop?$ never fires and the program returns the empty set, yet $\sigma_0$ fails $AF\,p$, directly contradicting Theorem 4.1 if that theorem were stated for infinite systems.

Watch

Extended reading notes

Core claim

On any finite transition system, for every ACTL or single-variable universal $\mu$-calculus formula $\varphi$, the collecting semantics of the MOKA encoding $\lfloor\varphi\rceil$ returns exactly the stacks whose current state does not satisfy $\varphi$. Consequently a state $\sigma$ satisfies $\varphi$ exactly when the encoding run on $\{\langle\sigma,\emptyset\rangle\}$ yields the empty set. Under any sound state abstraction lifted to stacks, the abstract interpreter is sound: abstract bottom means the formula holds on all initial states. With the LCL program logic, derivable judgements are precise: a derivable postcondition is empty if and only if the formula holds on the whole precondition, and any nonempty derivable postcondition consists only of true counterexamples.

Load-bearing premise

The encodings of $AF$, $AU$, and least-fixpoint formulas assume every infinite path eventually revisits a state, which holds only for finite transition systems; on an infinite system with a non-repeating infinite path, the $loop?$ check would miss a real counterexample.

Editorial extensions

If this is right

  • A model checker can run any sound abstract interpreter on MOKA programs: if the abstract result is bottom, the formula holds for all initial states.
  • LCL derivations give exact, alarm-free verdicts: an empty derivable postcondition proves the formula, and a nonempty one yields only genuine counterexamples.
  • A failed LCL proof obligation pinpoints where local completeness fails and suggests how to repair the abstraction, giving a counterexample-guided refinement loop.
  • The encoding works with non-partitioning abstractions such as predicate abstraction, with partition-based abstractions arising as a special case.
  • The same scheme extends to Propositional Dynamic Logic, because its programs are built from the same Kleene-algebra-with-tests primitives.

Reading between the lines

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

  • A dual treatment of existential fragments, producing witnesses instead of counterexamples, should be as direct as the universal encoding and could later be combined to handle mixed logics.
  • The set-based loop detection in frames abstracts away order and multiplicity of visited states; richer logics with regular or counting operators would likely need a finer trace representation.
  • Because MOKA is an algebraic command language, existing abstract-interpretation tools could in principle be reused as model checkers without building dedicated verification engines, though the paper does not implement this.
  • A concrete next step would be to implement the MOKA abstract interpreter over predicate abstraction and compare abstraction repair strategies, such as refining the state domain versus refining the stack equivalence.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 3 minor

Summary. The paper proposes a reduction of model checking of ACTL and of the single-variable universal modal mu-calculus to program verification. It introduces MOKA, a Kleene-algebra-with-fixpoints language over stacks of frames, and encodes each formula phi as a program whose concrete semantics on a set of stacks is exactly the set of counterexample states in that set. It then lifts state abstractions to a stack domain, proves soundness of the resulting abstract interpreter (Prop. 5.4), extends local completeness logic with fixpoint rules (Table 2), and connects failed LCL proof obligations to abstraction refinement. The ACTL encoding and the abstract-interpretation part are developed in detail, with worked examples on traffic-light and control-flow-graph systems.

Significance. The conceptual direction is interesting and the paper is generally careful: the ACTL encoding carries a structural-induction proof, the abstract semantics is sound by construction, and the muLCL extension comes with a soundness lemma. The worked examples make the abstraction/refinement story concrete and show the intended gain over partition-based abstractions. However, the proof of the mu2-calculus half of the central encoding theorem (Theorem 4.1 via Corollary B.3) has genuine gaps. Since this half is a main advertised contribution, the central claim cannot be considered fully established in the present version.

major comments (2)
  1. [Corollary B.3 (least fixpoint)] The proof that lfp(Fn)=lfp(F) for least-fixpoint formulae is not valid as written. The argument says it suffices to compare Fn and F on reductive functions f, but the iterates used to build the least fixpoint need not be reductive. Concretely, for a single-state system with s->s and phi = mu x. 2x, taking Fn as in the corollary gives Fn^2(bottom)(<s,emptyset>::S) = {<s,{s}>::S}, which is not a subset of {<s,emptyset>::S}; hence the 'reductive' restriction is not preserved by iteration. The equality displayed for the sigma in Delta case, and the discarding of the add;floor(phi_x) branch, require exactly the reductivity of the current iterate, which fails for the iterates that define the least fixpoint. The equality lfp(Fn)=lfp(F) is therefore not established, and Theorem 4.1 is not fully proved for least-fixpoint mu2 formulae.
  2. [Corollary B.3 (greatest fixpoint)] The greatest-fixpoint case assumes two unproved facts: (i) the substitution-commutation property floor(psi1[psi2/x]) = floor(psi1)[floor(psi2)/X], used to conclude floor(nu^n x.phi) = mu^n X.floor(phi); and (ii) the identity Jmu X.floor(phi)K_eta = union_{n in N} Jmu^n X.floor(phi)K_eta. Property (i) is not immediate, since the encoding of the 2 modality and of fixpoints changes the stack structure and the meaning of occurrences of X. Property (ii) requires an omega-continuity or finite-height argument on the function lattice; the paper only mentions ACC for abstract domains (Remark 6.2), not for this equality. The nu x branch of the central encoding theorem therefore also needs a repaired proof.
minor comments (3)
  1. [Theorem 4.1 and Section 4] The statement of Theorem 4.1 should include the finiteness hypothesis explicitly. The AF and AU clauses rely on identifying infinite traces with looping traces, which is justified only by the 'finite state systems' remark in Section 4; since Section 2.2 fixes finite Sigma, this is a clarity issue, but the theorem statement as written is easy to misread as holding for arbitrary transition systems.
  2. [Example C.10] The sentence beginning 'We provide an example of a disjuctive abstraction where the lambda a in A. alpha(JbK_Sigma) and A a is bot the BCA' contains a typo ('disjuctive' and 'bot' for 'disjunctive' and 'not').
  3. [Section 4, lower-closure remark] The claim that the semantics of formula-encoding programs is a lower closure is stated before the notion is defined or justified; a pointer to the reference [38] is given, but a short explanation in the text would help the reader understand why this property is relevant for the later abstraction results.

Circularity Check

1 steps flagged · score 4.0 of 10

µ2-calculus fixpoint branch has a circular 'reductive functions' step; ACTL and abstract-interpretation parts are self-contained.

  1. other [Appendix B, Corollary B.3 (µ2-calculus least-fixpoint case)]
    "We conclude simply by observing that, in our setting we can restrict to functions f∈ C^C which are reductive, i.e., such that f(X)⊆ X for X∈ C, and on such functions Fn(f) = F(f)."

    This step is the sole bridge between the tableau-correct intermediate encoding Tµx.φx W and the paper's actual encoding ⌊µx.φx⌉: it equates lfp(Fn) and lfp(F). The equality is inferred from agreement of Fn and F on reductive functions, but the least-fixpoint iterates are not shown reductive and need not be: for φx=p and a state σ⊢¬p, Fn(⊥)({⟨σ,∅⟩::S})={⟨σ,{σ}⟩::S}, which is not a subset of the input. Reductivity f(X)⊆X is exactly the filter/counterexample behaviour that Theorem 4.1 must prove for formula encodings. Thus the proof assumes the target property on the very functions being compared; the derivation of lfp(Fn)=lfp(F) reduces to its own conclusion rather than to the semantics of MOKA.

full rationale

The ACTL branch (Theorem B.1) is a genuine structural-induction proof from the independently defined semantics of the MOKA primitives and the standard finite-trace/loop characterization; no fitted parameter or target-dependent definition is involved. The abstract-interpretation lifting (Section 5) and the µLCL soundness proof (Lemma D.1) are also derived from the stated lattice and Galois-connection machinery. The paper does rely on the authors' earlier LCL and abstract-interpretation-repair work [6,7,8], but those are published external results, and the new fixpoint rules are proved here; that self-citation is not load-bearing in a circular way. The main defect is localized to Corollary B.3 for the µ2-calculus: the 'reductive functions' restriction is not invariant under the fixpoint iteration, so the equality lfp(Fn)=lfp(F) is not established; this is a circular/unsupported proof step. Additionally, the νx branch asserts without proof that ⌊ψ1[ψ2/x]⌉ = ⌊ψ1⌉[⌊ψ2⌉/X]; this is an omitted proof, not a circularity, but it further weakens the µ2 branch. Because the ACTL result and the overall framework remain self-contained, the circularity is partial rather than total.

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

The framework rests on standard abstract interpretation axioms plus two domain restrictions: finite state spaces and single-variable mu-calculus. No fitted parameters or empirical constants are introduced.

assumptions (5)
  • domain assumption Finite transition system (Sigma finite)
    Needed for the loop? check to identify infinite traces with cycles in AF, AU, and least fixpoint encodings (Section 4).
  • domain assumption Total transition relation
    Standard in model checking; every state has a successor (Definition 2.2).
  • domain assumption Single-variable mu-calculus with no mutual fixpoint dependencies
    The paper restricts to this fragment (Section 2.2) and the tableau proof of Theorem B.2 relies on it.
  • standard math Galois connection and standard abstract interpretation
    Used throughout for sound approximations (Section 2.1).
  • domain assumption Soundness of LCL rules for KAT programs from prior work
    The paper extends LCL with fixpoint rules; the base rules are imported from prior work (Table 1, Section 6).
invented entities (2)
  • MOKA language
    purpose: To encode temporal formulae as programs that return counterexamples
    Internal construction; correctness is proven within the paper.
  • Traced frames (sigma,Delta) and stacks
    purpose: To track visited states for loop detection and handle nested formulae
    Semantic device; no external empirical handle.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Model Checking as Program Verification by Abstract Interpretation (Extended Version)." pith.science (2026). https://pith.science/paper/WICBQMZD

@misc{pith2026250605525,
  author       = {Pith},
  title        = {Pith review of: Model Checking as Program Verification by Abstract Interpretation (Extended Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/WICBQMZD}},
  note         = {Machine review of arXiv:2506.05525}
}
read the original abstract

Abstract interpretation offers a powerful toolset for static analysis, tackling precision, complexity and state-explosion issues. In the literature, state partitioning abstractions based on (bi)simulation and property-preserving state relations have been successfully applied to abstract model checking. Here, we pursue a different track in which model checking is seen as an instance of program verification. To this purpose, we introduce a suitable language-called MOKA (for MOdel checking as abstract interpretation of Kleene Algebras)-which is used to encode temporal formulae as programs. In particular, we show that (universal fragments of) temporal logics, such as ACTL or, more generally, universal mu-calculus can be transformed into MOKA programs. Such programs return all and only the initial states which violate the formula. By applying abstract interpretation to MOKA programs, we pave the way for reusing more general abstractions than partitions as well as for tuning the precision of the abstraction to remove or avoid false alarms. We show how to perform model checking via a program logic that combines under-approximation and abstract interpretation analysis to avoid false alarms. The notion of locally complete abstraction is used to dynamically improve the analysis precision via counterexample-guided domain refinement.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

54 extracted references · 54 canonical work pages

  1. [1]

    Abstraction, up-to techniques and games for systems of fixpoint equations

    Paolo Baldan, Barbara K\"onig, and Tommaso Padoan. Abstraction, up-to techniques and games for systems of fixpoint equations. In Proceedings of CONCUR 2020 , volume 171 of LIPIcs , pages 25:1--25:20, 2020

    work page 2020

  2. [2]

    Abstraction for falsification

    Thomas Ball, Orna Kupferman, and Greta Yorsh. Abstraction for falsification. In Proceedings of CAV 2005 , volume 3576 of LNCS , pages 67--81. Springer, 2005

    work page 2005

  3. [3]

    Rajamani

    Thomas Ball, Andreas Podelski, and Sriram K. Rajamani. Boolean and C artesian abstraction for model checking C programs. In Proceedings of TACAS 2001 , volume 2031 of LNCS , pages 268--283. Springer, 2001

    work page 2001

  4. [4]

    Gallagher

    Gourinath Banda and John P. Gallagher. Constraint-based abstract semantics for temporal logic: A direct approach to design and implementation. In Proceedings of LPAR 2016 , volume 6355 of LNCS , pages 27--45. Springer, 2010

    work page 2016

  5. [5]

    On-the-fly model checking of RCTL formulas

    Ilan Beer, Shoham Ben - David, and Avner Landver. On-the-fly model checking of RCTL formulas. In CAV , volume 1427 of LNCS , pages 184--194. Springer, 1998

    work page 1998

  6. [6]

    A logic for locally complete abstract interpretations

    Roberto Bruni, Roberto Giacobazzi, Roberta Gori, and Francesco Ranzato. A logic for locally complete abstract interpretations. In Proceedings of LICS 2021 , pages 1--13. IEEE , 2021

    work page 2021

  7. [7]

    Abstract interpretation repair

    Roberto Bruni, Roberto Giacobazzi, Roberta Gori, and Francesco Ranzato. Abstract interpretation repair. In Proceedings of PLDI 2022 , pages 426--441. ACM , 2022

    work page 2022

  8. [8]

    A correctness and incorrectness program logic

    Roberto Bruni, Roberto Giacobazzi, Roberta Gori, and Francesco Ranzato. A correctness and incorrectness program logic. Journal of the ACM , 70(2):15:1--15:45, 2023

    work page 2023

Show all 54 references
  1. [9]

    Simulation-based minimization

    Doron Bustan and Orna Grumberg. Simulation-based minimization. ACM Transactions on Computational Logic , 4(2):181--206, 2003

    2003

  2. [10]

    Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith

    Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In Proceedings of CAV 2000 , volume 1855 of LNCS , pages 154--169. Springer, 2000

    2000

  3. [11]

    Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith

    Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM , 50(5):752--794, 2003

    2003

  4. [12]

    Clarke, Orna Grumberg, Daniel Kroening, Doron A

    Edmund M. Clarke, Orna Grumberg, Daniel Kroening, Doron A. Peled, and Helmut Veith. Model checking, 2nd Edition . MIT Press, 2018

    2018

  5. [13]

    Clarke, Orna Grumberg, and David E

    Edmund M. Clarke, Orna Grumberg, and David E. Long. Model checking and abstraction. ACM Transactions on Programming, Languages and Systems , 16(5):1512--1542, 1994

    1994

  6. [14]

    Clarke, William Klieber, Milos Nov \' a cek, and Paolo Zuliani

    Edmund M. Clarke, William Klieber, Milos Nov \' a cek, and Paolo Zuliani. Model checking and the state explosion problem. In Tools for Practical Software Verification, LASER, International Summer School 2011 , volume 7682 of LNCS , pages 1--30. Springer, 2011

    2011

  7. [15]

    Principles of Abstract Interpretation

    Patrick Cousot. Principles of Abstract Interpretation . MIT Press, 2021

    2021

  8. [16]

    Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints

    Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of POPL 1977 , pages 238--252. ACM , 1977

    1977

  9. [17]

    Systematic design of program analysis frameworks

    Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In Proceedings of POPL 1979 , pages 269--282. ACM Press, 1979

    1979

  10. [18]

    Refining model checking by abstract interpretation

    Patrick Cousot and Radhia Cousot. Refining model checking by abstract interpretation. Automated Software Engineering , 6(1):69--95, 1999

    1999

  11. [19]

    Temporal abstract interpretation

    Patrick Cousot and Radhia Cousot. Temporal abstract interpretation. In Proceedings of POPL 2000 , pages 12--25. ACM , 2000

    2000

  12. [20]

    Fixpoint-guided abstraction refinements

    Patrick Cousot, Pierre Ganty, and Jean - Fran c ois Raskin. Fixpoint-guided abstraction refinements. In Proceedings of SAS 2007 , volume 4634 of LNCS , pages 333--348. Springer, 2007

    2007

  13. [21]

    Abstract interpretation of reactive systems

    Dennis Dams, Rob Gerth, and Orna Grumberg. Abstract interpretation of reactive systems. ACM Transactions on Programming, Languages and Systems , 19(2):253--291, 1997

    1997

  14. [22]

    Abstraction and abstraction refinement

    Dennis Dams and Orna Grumberg. Abstraction and abstraction refinement. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking , pages 385--419. Springer, 2018

    2018

  15. [23]

    Davey and Hilary A

    Brian A. Davey and Hilary A. Priestley. Introduction to Lattices and Order . Cambridge University Press, 2002

    2002

  16. [24]

    Incompleteness, counterexamples, and refinements in abstract model-checking

    Roberto Giacobazzi and Elisa Quintarelli. Incompleteness, counterexamples, and refinements in abstract model-checking. In Proceedings of SAS 2001 , volume 2126 of LNCS , pages 356--373. Springer, 2001

    2001

  17. [25]

    Incompleteness of states w.r.t

    Roberto Giacobazzi and Francesco Ranzato. Incompleteness of states w.r.t. traces in model checking. Information and Computation , 204(3):376--407, 2006

    2006

  18. [26]

    Making abstract interpretations complete

    Roberto Giacobazzi, Francesco Ranzato, and Francesca Scozzari. Making abstract interpretations complete. Journal of the ACM , 47(2):361--416, 2000

    2000

  19. [27]

    Construction of abstract state graphs with PVS

    Susanne Graf and Hassen Sa \" di. Construction of abstract state graphs with PVS . In Proceedings of CAV 1997 , volume 1254 of LNCS , pages 72--83. Springer, 1997

    1997

  20. [28]

    When not losing is better than winning: Abstraction and refinement for the full mu-calculus

    Orna Grumberg, Martin Lange, Martin Leucker, and Sharon Shoham. When not losing is better than winning: Abstraction and refinement for the full mu-calculus. Information and Computation , 205(8):1130--1148, 2007

    2007

  21. [29]

    Abstraction refinement for bounded model checking

    Anubhav Gupta and Ofer Strichman. Abstraction refinement for bounded model checking. In Proceedings of CAV 2005 , volume 3576 of LNCS , pages 112--124. Springer, 2005

    2005

  22. [30]

    Dynamic Logic

    David Harel, Jerzy Tiuryn, and Dexter Kozen. Dynamic Logic . MIT Press, Cambridge, MA, USA, 2000

    2000

  23. [31]

    Software model checking

    Ranjit Jhala and Rupak Majumdar. Software model checking. ACM Computing Surveys , 41(4):21:1--21:54, 2009

    2009

  24. [32]

    Predicate abstraction for program verification

    Ranjit Jhala, Andreas Podelski, and Andrey Rybalchenko. Predicate abstraction for program verification. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking , pages 447--491. Springer, 2018

    2018

  25. [33]

    Kleene algebra with tests

    Dexter Kozen. Kleene algebra with tests. ACM Transactions on Programming, Languages and Systems , 19(3):427--443, 1997

    1997

  26. [34]

    A modal process logic

    Kim Guldstrand Larsen and Bent Thomsen. A modal process logic. In Proceedings of LICS 1988 , pages 203--210. IEEE Computer Society, 1988

    1988

  27. [35]

    Towards K leene algebra with recursion

    Hans Lei . Towards K leene algebra with recursion. In Proceedings of CSL 1991 , volume 626 of LNCS , pages 242--256. Springer, 1991

    1991

  28. [36]

    Property preserving abstractions for the verification of concurrent systems

    Claire Loiseaux, Susanne Graf, Joseph Sifakis, Ahmed Bouajjani, and Saddek Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design , 6(1):11--44, 1995

    1995

  29. [37]

    Semantics for abstract interpretation-based static analyzes of temporal properties

    Damien Mass \' e . Semantics for abstract interpretation-based static analyzes of temporal properties. In Proceedings of SAS 2002 , volume 2477 of LNCS , pages 428--443. Springer, 2002

    2002

  30. [38]

    Tutorial on static inference of numeric invariants by abstract interpretation

    Antoine Min \' e . Tutorial on static inference of numeric invariants by abstract interpretation. Foundations and Trends in Programming Languages , 4(3-4):120--372, 2017

    2017

  31. [39]

    Model checking Is static analysis of modal logic

    Flemming Nielson and Hanne Riis Nielson. Model checking Is static analysis of modal logic. In Proceedings of FoSSaCS 2010 , volume 6014 of LNCS , pages 191--205. Springer, 2010

    2010

  32. [40]

    A succinct solver for ALFP

    Flemming Nielson, Helmut Seidl, and Hanne Riis Nielson. A succinct solver for ALFP . Nordic Journal of Computing , 9(4):335--372, 2002

    2002

  33. [41]

    Flow logic: A multi-paradigmatic approach to static analysis

    Hanne Riis Nielson and Flemming Nielson. Flow logic: A multi-paradigmatic approach to static analysis. In The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones [on occasion of his 60th birthday] , volume 2566 of LNCS , pages 223--2...

    2002

  34. [42]

    Peter W. O'Hearn. Incorrectness logic. In Proceedings of POPL 2020 , volume 4, pages 10:1--10:32. ACM , 2020

    2020

  35. [43]

    On the completeness of model checking

    Francesco Ranzato. On the completeness of model checking. In Proceedings of ESOP 2001 , volume 2028 of LNCS , pages 137--154. Springer, 2001

    2001

  36. [44]

    Making abstract model checking strongly preserving

    Francesco Ranzato and Francesco Tapparo. Making abstract model checking strongly preserving. In Proceedings of SAS 2002 , volume 2477 of LNCS , pages 411--427. Springer, 2002

    2002

  37. [45]

    Generalized strong preservation by abstract interpretation

    Francesco Ranzato and Francesco Tapparo. Generalized strong preservation by abstract interpretation. Journal of Logic and Computation , 17(1):157--197, 2007

    2007

  38. [46]

    Binary relations for abstraction and refinement

    David Schmidt. Binary relations for abstraction and refinement. Technical report, Kansas State University, 2001

    2001

  39. [47]

    David A. Schmidt. Data flow analysis is model checking of abstract interpretations. In Proceedings of POPL 1998 , pages 38--48. ACM , 1998

    1998

  40. [48]

    Schmidt and Bernhard Steffen

    David A. Schmidt and Bernhard Steffen. Program analysis as model checking of abstract interpretations. In Proceedings of SAS 1998 , volume 1503 of LNCS , pages 351--380. Springer, 1998

    1998

  41. [49]

    Monotonic abstraction-refinement for CTL

    Sharon Shoham and Orna Grumberg. Monotonic abstraction-refinement for CTL . In Proceedings of TACAS 2004 , volume 2988 of LNCS , pages 546--560. Springer, 2004

    2004

  42. [50]

    Data flow analysis as model checking

    Bernhard Steffen. Data flow analysis as model checking. In Proceedings of TACS 1991 , volume 526 of LNCS , pages 346--365. Springer, 1991

    1991

  43. [51]

    Generating data flow analysis algorithms from modal specifications

    Bernhard Steffen. Generating data flow analysis algorithms from modal specifications. Sci. Comput. Program. , 21(2):115--139, 1993

    1993

  44. [52]

    Local model checking in the modal mu-calculus

    Colin Stirling and David Walker. Local model checking in the modal mu-calculus. In Proceedings of TAPSOFT'89 , volume 351 of LNCS , pages 369--383. Springer, 1989

    1989

  45. [53]

    Temporal logic can be more expressive

    Pierre Wolper. Temporal logic can be more expressive. Information and Control , 56(1/2):72--99, 1983

    1983

  46. [54]

    Model checking as static analysis: Revisited

    Fuyuan Zhang, Flemming Nielson, and Hanne Riis Nielson. Model checking as static analysis: Revisited. In Proceedings of IFM 2012 , volume 7321 of LNCS , pages 99--112. Springer, 2012

    2012

Pith tools

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