pith. sign in

arxiv: 1907.03999 · v1 · pith:22JIFS3Enew · submitted 2019-07-09 · 💻 cs.LO · cs.PL· cs.SC

Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification

Emanuele De Angelis (DEC , University "G. d'Annunzio" of Chieti-Pescara , Italy) , Fabio Fioravanti (DEC , Alberto Pettorossi (DICII , University of Roma Tor Vergata , Maurizio Proietti (CNR-IASI , Rome This is my paper

Pith reviewed 2026-05-25 00:14 UTC · model grok-4.3

classification 💻 cs.LO cs.PLcs.SC
keywords constrained horn clausesprogram verificationsorting algorithmsinductive data structuresdifference predicatespartial correctnessfunctional programshorn clause transformation
0
0 comments X

The pith

A transformation technique reduces constrained Horn clauses from sorting programs to integer and boolean constraints whose satisfiability proves the target properties.

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

The paper shows that a transformation applied to constrained Horn clauses generated from functional sorting programs can remove inductive data structures such as lists. Once reduced to constraints over integers and booleans only, satisfiability of the resulting clauses can be decided by existing solvers to establish properties including output orderedness, input-output multiset equality, and sum preservation. The study applies the method to both linearly recursive algorithms such as insertion sort and selection sort and to non-linear ones such as quicksort and mergesort. Difference predicates are introduced to encode the auxiliary lemmas needed during verification. If the transformation preserves satisfiability status, the approach yields an effective verification path that avoids direct solver reasoning about complex data structures.

Core claim

The transformation technique, when successful, derives a set of constrained Horn clauses whose constraints range only over the integers and booleans; satisfiability of these clauses establishes the partial correctness properties (orderedness of the output list and multiset equality between input and output) as well as arithmetic properties such as equality of the sum of elements before and after sorting, for the programs implementing insertion sort, selection sort, quicksort, and mergesort.

What carries the argument

The transformation technique that eliminates inductive data structures from constrained Horn clauses, together with the introduction of difference predicates whose definitions serve as the required verification lemmas.

If this is right

  • Partial correctness of linearly recursive sorts such as insertion sort and selection sort reduces to satisfiability of integer-boolean constrained Horn clauses.
  • The same reduction applies to non-linear recursive sorts such as quicksort and mergesort.
  • Arithmetic properties such as preservation of the sum of list elements are likewise established by satisfiability of the transformed clauses.
  • Difference predicates supply the lemmata that allow the satisfiability check to succeed where it would otherwise fail.

Where Pith is reading between the lines

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

  • The separation of data-structure elimination from numeric constraint solving may apply to verification of other list-manipulating functional programs whose recursion follows similar patterns.
  • Integrating the transformation as a preprocessing step inside CHC solvers could enlarge the class of programs whose properties become automatically checkable.
  • Because the method targets both orderedness and multiset equality, it offers a uniform route to proving that sorting implementations are correct permutations.

Load-bearing premise

The transformation that eliminates inductive data structures succeeds for the considered sorting programs without changing the satisfiability status of the original constrained Horn clauses.

What would settle it

A concrete counter-example in which, for one of the studied sorting programs, the transformed clauses are satisfiable yet the program fails to produce an ordered output list or to preserve the multiset of input elements.

read the original abstract

The proof of a program property can be reduced to the proof of satisfiability of a set of constrained Horn clauses (CHCs) which can be automatically generated from the program and the property. In this paper we have conducted a case study in Horn clause verification by considering several sorting programs with the aim of exploring the effectiveness of a transformation technique which allows us to eliminate inductive data structures such as lists or trees. If this technique is successful, we derive a set of CHCs with constraints over the integers and booleans only, and the satisfiability check can often be performed in an effective way by using state-of-the-art CHC solvers, such as Eldarica or Z3. In this case study we have also illustrated the usefulness of a companion technique based on the introduction of the so-called difference predicates, whose definitions correspond to lemmata required during the verification. We have considered functional programs which implement the following kinds of sorting algorithms acting on lists of integers: (i) linearly recursive sorting algorithms, such as insertion sort and selection sort, and (ii) non-linearly recursive sorting algorithms, such as quicksort and mergesort, and we have considered the following properties: (i) the partial correctness properties, that is, the orderedness of the output lists, and the equality of the input and output lists when viewed as multisets, and (ii) some arithmetic properties, such as the equality of the sum of the elements before and after sorting.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper conducts a case study applying an existing transformation technique to eliminate inductive data structures (lists) from CHCs generated from functional sorting programs (insertion sort, selection sort, quicksort, mergesort) and their properties (orderedness, multiset equality, sum preservation). If successful, the resulting CHCs involve only integer and boolean constraints solvable by solvers such as Eldarica or Z3; difference predicates are introduced as needed to encode required lemmas.

Significance. The work provides concrete evidence that the transformation plus difference predicates can handle both linearly and non-linearly recursive sorting algorithms for partial correctness and arithmetic properties. Credit is due for the explicit conditional framing of the claim and the focus on practical solver effectiveness rather than new theory.

minor comments (2)
  1. [Abstract] Abstract: the phrase 'several sorting programs' is followed by a list; explicitly naming insertion sort, selection sort, quicksort and mergesort in the abstract would improve immediate clarity.
  2. The manuscript reports successful application but supplies no table or section enumerating which properties succeeded or failed for each algorithm; adding such a summary table would strengthen the case-study presentation without altering the central claim.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our case study and the recommendation for minor revision. No specific major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper is a case study applying an existing transformation technique (from prior literature) to remove inductive data structures from CHCs generated for specific sorting programs and properties. The central claim is conditional on the transformation succeeding for the considered examples, after which satisfiability is checked by external solvers (Eldarica, Z3). No equations, parameters, or derivations reduce results to inputs by construction; no self-citation is load-bearing for a uniqueness theorem or ansatz; the work does not rename known results or smuggle in fitted inputs as predictions. The derivation chain is self-contained against external benchmarks and solvers.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claim rests on the soundness of the CHC encoding of program semantics and the correctness of the data-structure elimination transformation; both are treated as given from prior work. No free parameters are introduced. Difference predicates are an auxiliary device rather than an invented physical entity.

axioms (2)
  • domain assumption Satisfiability of the generated CHCs is equivalent to the program satisfying the stated property
    Invoked in the opening sentence of the abstract when reducing proof of program property to CHC satisfiability.
  • domain assumption The transformation preserves satisfiability when it eliminates inductive data structures
    Stated as the condition under which the integer/boolean CHCs can be solved effectively.
invented entities (1)
  • difference predicates no independent evidence
    purpose: To encode lemmata required during verification of the transformed CHCs
    Introduced as a companion technique whose definitions correspond to required lemmata.

pith-pipeline@v0.9.0 · 5862 in / 1390 out tokens · 20819 ms · 2026-05-25T00:14:21.993274+00:00 · methodology

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

27 extracted references · 27 canonical work pages

  1. [1]

    Bjørner, A

    N. Bjørner, A. Gurfinkel, K. L. McMillan & A. Rybalchenko ( 2015): Horn Clause Solvers for Program V erification. In L. D. Beklemishev, A. Blass, N. Dershowitz, B. Finkbeine r & W . Schulte, editors: Fields of Logic and Computation II - Essays Dedicated to Y uri Gurevichon the Occasion of His 75th Birthday, Lecture Notes inComputer Science 9300, Springer, p...

    work page doi:10.1007/978-3-319-23534-9_2 2015

  2. [2]

    Bundy (2001): The Automation of Proof by Mathematical Induction

    A. Bundy (2001): The Automation of Proof by Mathematical Induction . In A. Robinson & A. V oronkov, editors: Handbook of Automated Reasoning , I, North Holland, pp. 845–911, doi: 10.1016/ B978-044450813-3/50015-1

    work page 2001

  3. [3]

    De Angelis, F

    E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2014): Program V erification via Iterated Special- ization. Science of Computer Programming 95, Part 2, pp. 149–175, doi: 10.1016/j.scico.2014.05.017. Selected and extended papers from Partial Evaluation and Pr ogram Manipulation 2013

    work page doi:10.1016/j.scico.2014.05.017 2014

  4. [4]

    De Angelis, F

    E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2014): V eriMAP: A Tool for V erifying Programs through Transformations . In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , TACAS ’14 , Lecture Notes in Com- 62 Proving Properties of Sorting Programs: A Case Study in Horn Cl...

    work page doi:10.1007/978-3-642-54862-8_47 2014

  5. [5]

    De Angelis, F

    E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2015): Proving correctness of imperative programs by linearizing constrained Horn clauses . Theory and Practice of Logic Programming 15(4–5), pp. 635–650, doi:10.1017/S1471068415000289

    work page doi:10.1017/s1471068415000289 2015

  6. [6]

    De Angelis, F

    E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2017): Semantics-based generation of verifica- tion conditions via program specialization . Science of Computer Programming 147, pp. 78–108, doi: 10. 1016/j.scico.2016.11.002. Available at http://www.sciencedirect.com/science/article/ pii/S016764231630199X. Selected and Extended papers from the Int...

    work page 2017

  7. [7]

    De Angelis, F

    E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2018): Predicate Pairing for program verification. TPLP 18(2), pp. 126–166, doi: 10.1017/S1471068417000497

    work page doi:10.1017/s1471068417000497 2018

  8. [8]

    De Angelis, F

    E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2018): Solving Horn Clauses on Inductive Data Types Without Induction. TPLP 18(3-4), pp. 452–469, doi: 10.1017/S1471068418000157

    work page doi:10.1017/s1471068418000157 2018

  9. [9]

    De Angelis, F

    E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2019): Lemma Generation for Horn Clause Satis- fiability: A Preliminary Study . In A. Lisitsa & A. Nemytykh, editors: Proceedings of VPT 2019 Workshop on Program V erification and Program Transformation, Genova , Italy, April 4th, 2019 , To appear in EPTCS. Available at http://refal.botik.ru/vpt/vpt...

    work page 2019

  10. [10]

    Etalle & M

    S. Etalle & M. Gabbrielli (1996): Transformations of CLP Modules. Theoretical Computer Science 166, pp. 101–146, doi:10.1016/0304-3975(95)00148-4

    work page doi:10.1016/0304-3975(95)00148-4 1996

  11. [11]

    Fedyukovich, S

    G. Fedyukovich, S. Prabhu, K. Madhukar & A. Gupta (2018) : Solving Constrained Horn Clauses Using Syntax and Data . In N. Bjørner & A. Gurfinkel, editors: 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018 , IEEE, pp. 1–9, doi: 10.23919/FMCAD. 2018.8603011

    work page doi:10.23919/fmcad 2018

  12. [12]

    Grebenshchikov, N

    S. Grebenshchikov, N. P . Lopes, C. Popeea & A. Rybalchen ko (2012): Synthesizing software verifiers from proof rules . In: Proceedings of the ACM SIGPLAN Conference on Programming La nguage Design and Implementation, PLDI ’12 , pp. 405–416, doi: 10.1145/2345156.2254112

    work page doi:10.1145/2345156.2254112 2012

  13. [13]

    Hojjat, F

    H. Hojjat, F. Konecn´ y, F. Garnier, R. Iosif, V . Kuncak & P . R¨ ummer (2012):A V erification T oolkit for Nu- merical Transition Systems . In D. Giannakopoulou & D. M´ ery, editors: FM ’12: Formal Methods, 18th International Symposium, Paris, France, August 27–31, 201 2. Proceedings, Lecture Notes in Computer Sci- ence 7436, Springer, pp. 247–251, doi: ...

    work page doi:10.1007/978-3-642-32759-9_21 2012

  14. [14]

    Hojjat & P

    H. Hojjat & P . R¨ ummer (2018): The ELDARICA Horn Solver . In N. Bjørner & A. Gurfinkel, editors: 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin , TX, USA, October 30 - November 2, 2018, IEEE, pp. 1–7, doi: 10.23919/FMCAD.2018.8603013

    work page doi:10.23919/fmcad.2018.8603013 2018

  15. [15]

    B. Kafle, J. P . Gallagher & J. F. Morales (2016): RAHFT: A T ool for V erifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata . In: Computer Aided V erification, 28th International Conferenc e, CA V 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, Lecture Notes in Computer Science 9779, Springer, pp. 261–268, doi: 10....

    work page doi:10.1007/978-3-319-41528-4_14 2016

  16. [16]

    Komuravelli, A

    A. Komuravelli, A. Gurfinkel & S. Chaki (2014): SMT-Based Model Checking for Recursive Programs . In A. Biere & R. Bloem, editors: Computer Aided V erification - 26th International Conferenc e, CA V 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, A ustria, July 18-22, 2014. Proceedings , Lecture Notes in Computer Science 8559, Springer, ...

    work page doi:10.1007/978-3-319-08867-9_2 2014

  17. [17]

    Leroy, D

    X. Leroy, D. Doligez, A. Frisch, J. Garrigue, D. R´ emy & J . V ouillon (2017): The OCaml system, Release 4.06. Documentation and user’s manual, Institut National de Rec herche en Informatique et en Automatique, France

    work page 2017

  18. [18]

    Mordvinov & G

    D. Mordvinov & G. Fedyukovich (2017): Synchronizing Constrained Horn Clauses. In T. Eiter & D. Sands, editors: LP AR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Rea- E. De Angelis et al. 63 soning, Maun, Botswana, May 7-12, 2017 , EPiC Series in Computing 46, EasyChair, pp. 338–355, doi: 10. 29007/gr5c. Available...

    work page 2017

  19. [19]

    L. M. de Moura & N. Bjørner (2008): Z3: An Efficient SMT Solver . In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS ’08 , Lecture Notes in Computer Science 4963, Springer, pp. 337–340, doi: 10.1007/978-3-540-78800-3_24

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

  20. [20]

    Reynolds & V

    A. Reynolds & V . Kuncak (2015): Induction for SMT Solvers . In Deepak D’Souza, Akash Lal & Kim Guld- strand Larsen, editors: V erification, Model Checking, and Abstract Interpretation - Proceedings of the 16th International Conference, VMCAI 2015, Mumbai, India,, Lecture Notes in Computer Science 8931, Springer, pp. 80–98, doi: 10.1007/978-3-662-46081-8_5

    work page doi:10.1007/978-3-662-46081-8_5 2015

  21. [21]

    Tamaki & T

    H. Tamaki & T. Sato (1984): Unfold/F old Transformation of Logic Programs . In S.- ˚A. T¨ arnlund, editor: Proceedings of the Second International Conference on Logi c Programming, ICLP ’84 , Uppsala University, Uppsala, Sweden, pp. 127–138

    work page 1984

  22. [22]

    H. Unno, S. Torii & H. Sakamoto (2017): Automating Induction for Solving Horn Clauses . In Rupak Ma- jumdar & Viktor Kuncak, editors: Proc. Computer Aided V erification - 29th Intern. Conf. CA V 20 17, Hei- delberg, Germany, Part II, Lecture Notes in Computer Science 10427, Springer, pp. 571 –591, doi:10.1007/ 978-3-319-63390-9_30 . 64 Proving Properties o...

    work page 2017

  23. [23]

    ⟨InsertionSort, IS Orderedness⟩

    ⟨InsertionSort, IS Perm⟩ 2. ⟨InsertionSort, IS Orderedness⟩

    work page

  24. [24]

    ⟨InsertionSort, IS Sum⟩

    ⟨InsertionSort, IS Length⟩ 4. ⟨InsertionSort, IS Sum⟩

    work page

  25. [25]

    ⟨SelectionSort, SS Orderedness⟩

    ⟨SelectionSort, SS Perm⟩ 6. ⟨SelectionSort, SS Orderedness⟩

    work page

  26. [26]

    ⟨QuickSort, QS Perm⟩

    ⟨SelectionSort, SS Length⟩ 8. ⟨QuickSort, QS Perm⟩

    work page

  27. [27]

    ⟨MergeSort, MS Sum⟩ 6.1 Program InsertionSort and property IS Perm

    ⟨QuickSort, QS Sum⟩ 10. ⟨MergeSort, MS Sum⟩ 6.1 Program InsertionSort and property IS Perm. 6.1.1 Constrained Horn clauses obtained by translating InsertionSort and IS Perm. :- pred ins(int,list(int),list(int)). :- pred insertionSort(list(int),list(int)). :- pred count(int,list(int),int). false :- C1=\=C2, insertionSort(L,S), count(X,L,C1), cou nt(X,S,C2)...

    work page