Mostly Automated Proof Repair for Verified Libraries
KIRAN GOPINATHAN, National University of Singapore, Singapore
MAYANK KEOLIYA, National University of Singapore, Singapore
ILYA SERGEY, National University of Singapore, Singapore
The cost of maintaining formally speciﬁed and veriﬁed software is widely considered prohibitively high dueto the need to constantly keep code and the proofs of its correctness in sync—the problem known as proof
repair. One of the main challenges in automated proof repair for evolving code is to infer invariants for a newversion of a once veriﬁed program that are strong enough to establish its full functional correctness.
In this work, we present the ﬁrst proof repair methodology for higher-order imperative functions, whose
initial versions were veriﬁed in the Coq proof assistant and whose speciﬁcations remained unchanged. Our
proof repair procedure is based on the combination of dynamic program alignment, enumerative invariant
synthesis, and a novel technique for eﬃciently pruning the space of invariant candidates, dubbed proof-driven
testing, enabled by the constructive nature of Coq’s proof certiﬁcates.
We have implemented our approach in a mostly-automated proof repair tool called Sisyphus. Given an
OCaml function veriﬁed in Coq and its unveriﬁed new version, Sisyphus produces a Coq proof for the newversion, discharging most of the new proof goals automatically and suggesting high-conﬁdence obligations
for the programmer to prove for the cases when automation fails. We have evaluated Sisyphus on 10 OCaml
programs taken from popular libraries, that manipulate arrays and mutable data structures, considering their
veriﬁed original and unveriﬁed evolved versions. Sisyphus has managed to repair proofs for all those functions,suggesting correct invariants and generating a small number of easy-to-prove residual obligations.
CCS Concepts: • Software and its engineering → Software veriﬁcation; Software evolution.
Additional Key Words and Phrases: mechanised proofs, separation logic, proof repair, invariant inference
ACM Reference Format:
Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey. 2023. Mostly Automated Proof Repair for Veriﬁed
Libraries. Proc. ACM Program. Lang. 7, PLDI, Article 107 (June 2023), 25 pages. https://doi.org/10.1145/3591221

1 INTRODUCTION
The last two decades of research in software veriﬁcation have demonstrated that large codebases
can be formally veriﬁed with regard to non-trivial properties by means of constructing machinecheckable correctness proofs. The examples of such veriﬁed software systems range from OS
kernels (Gu et al. 2016; Klein et al. 2009) and compilers (Kumar et al. 2014; Leroy 2006) to distributed
protocols (Hawblitzel et al. 2015; Rahli et al. 2018) and cryptographic libraries (Erbsen et al. 2019).
By and large, the recent practical success of formal veriﬁcation is enabled by (a) the advances inproof engineering and automation techniques (Ringer et al. 2019a), and (b) the vast body of research
dedicated to the design and implementation of mechanised domain-speciﬁc Floyd-Hoare-styleprogram logics (Floyd 1967; Hoare 1969) that allow for syntax-driven deductive symbolic reasoning
about programs as well as for modularity of their speciﬁcations and proof reuse.
Authors’ addresses: Kiran Gopinathan, National University of Singapore, Singapore, kirang@comp.nus.edu.sg; Mayank
Keoliya, National University of Singapore, Singapore, mayank@u.nus.edu; Ilya Sergey, National University of Singapore,
Singapore, ilya@nus.edu.sg.

This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.
© 2023 Copyright held by the owner/author(s).
2475-1421/2023/6-ART107
https://doi.org/10.1145/3591221
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

107107:2

Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey

Problem Statement. While the combined power of deductive machine-assisted reasoning andproof automation can get one as far as to prove a realistic system correct and bug-free, it does notprovide an immediate solution to the well known problem of maintaining the proof in response to
the evolution of veriﬁed code and its speciﬁcation (DeMillo et al. 1977). Such changes may involve:(1) data type deﬁnitions and usages in the veriﬁed program and its proof,(2) formal speciﬁcations and invariants ascribed to the system’s components, and(3) implementation logic of the system’s components.
Any of the changes (1)–(3) will most likely require one to modify correctness proofs in order tokeep them valid—the process known as proof repair (Ringer 2021). Recent work by Ringer et al.
(2021, 2018) has made advances in automating proof repair for the ﬁrst class of changes—in datatypes—by exploiting possible equivalences between old and new type deﬁnitions. The second classof changes—in speciﬁcations—has been acknowledged in several recent eﬀorts (Klein et al. 2009;
Wilcox et al. 2015), and some of them presented methodologies to make proofs more manageable, but
only for speciﬁc case studies (Woos et al. 2016). To the best of our knowledge, the third, probably themost common, class—arbitrary changes in the implementation logic—has been largely unexploredfrom the perspective of proof repair; particularly so in the context of imperative programs.
In this work, we focus on the problem of repairing proofs about imperative programs in response
to local changes in their code, and propose a practical solution to it.
Proof Repair for Libraries. A particular class of programs, whose speciﬁcations and data types
change infrequently, are user-facing libraries. By their nature, to enable forward-compatibility,
library functions are expected to preserve their API and the contracts describing their interaction
with the user code. Because of this, veriﬁed software libraries (Appel and Naumann 2020; Charguéraud et al. 2017; Polikarpova et al. 2018) are a sweet spot for proof repair: it is not uncommon
for library functions to undergo changes in their bodies for the sake of improved performance orreadability, while modiﬁcations in their type deﬁnitions and speciﬁcations are relatively rare.
Given this setup (the spec is ﬁxed) and the recent advances in automated deductive veriﬁcation (Jacobs et al. 2011; Leino 2010; Müller et al. 2016; Sammler et al. 2021), the reader might wonder
if it might be simpler to just prove the new version of a library function correct from scratch rather
than try to adapt its old proof. The reason why this is not so straightforward is because of the mainbane of fully-automated veriﬁcation—invariants for loops and higher-order functions.
As an example, consider a fragment of an imperative program in a higher-order language, suchas OCaml, that manipulates elements of an array arr via an eﬀectful function f in a for-loop overthe set of the array indices, and an updated version of the same program that replaces the for-loop
by a call to a higher-order function Array.iter that iterates over array elements implicitly:(* old version *)for i = 0 to Array.length(arr) - 1 do f arr.(i) done(* new version *)Array.iter f arr

Proving that the new version satisﬁes the same speciﬁcation as the old one would require us toprovide a new invariant for the lemma describing the eﬀect of a call to Array.iter, and ﬁnding
such an invariant is a daunting task for general-purpose automated program veriﬁers. On the other
hand, the programmer who performed this code refactoring with a knowledge about the relation
between array elements, their indices, and the workings of Array.iter, should be able to derive a
new invariant from an old one without too much trouble. Therefore, our hypothesis, supported bythis example, is that an old proof might be helpful for deriving a new one in the situation when
automated veriﬁcation of a program from scratch would most deﬁnitely fail.
The goal of this work is to turn this intuition into a practical proof repair algorithm for libraries.
Approach and Key Challenges. Our goal is to implement the hinted above approach to proof
repair by utilising the “knowledge about old invariants.” We implemented our methodology as aProc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

Mostly Automated Proof Repair for Verified Libraries

107:3

proof repair tool for OCaml programs veriﬁed in the CFML framework (Charguéraud 2011, 2020)—aversion of a sequential higher-order Separation Logic (SL) (O’Hearn et al. 2001; Reynolds 2002)
embedded into the higher-order logic of the Coq proof assistant.
The starting point for each proof repair task is an original OCaml program 𝑝, its SL speciﬁcation𝜙 ≜ {𝑃 } {𝑄 } (i.e., its pre-/postconditions), the CFML proof P of 𝑝’s correctness w.r.t. 𝜙 and anunveriﬁed new program version 𝑝 ′ that is believed to satisfy 𝜙, for which we would like to obtain
the proof P ′ . We identify the following two challenges that need to be addressed to construct P ′ :C1 The new program 𝑝 ′ may be implemented using diﬀerent computations; the relations between
their results and the computations of the old program are not speciﬁed and hence need to beinferred in order to construct plausible invariant candidates.
C2 Given the arbitrary nature of assertions about the shape of data, even assuming that P ′ does
not require new predicates, the search space of invariant candidates is enormous. Given the
non-negligeable time required to validate them using commodity solvers, such as Z3 (de Moura
and Bjørner 2008), and the inability of those solvers to handle many application-speciﬁc theories,
it is not clear what the best strategy is to eﬃciently prune this search space.
We address both challenges using a somewhat unorthodox approach for a problem targeting
deductive veriﬁcation in a foundational proof assistant (i.e., Coq)—via dynamic analysis techniques.
To address C1, we use a trace-based program alignment technique. We run 𝑝 and 𝑝 ′ on thesame randomly generated input, collecting traces of their execution and recording the values ofall program variables at each statement. As both programs still satisfy the same speciﬁcation, 𝑝 ′should still compute the same or similar concrete values when run on the same input. Thus, bycomparing the concrete values that ﬂow through the variables of each program, we heuristicallyinfer the mapping between the intermediate computations of both programs by relating statementsin 𝑝 and 𝑝 ′ that have the most variables with similar concrete values.
The solution to C2 is enabled by exploiting the nature of Coq proofs using a new technique that
we call proof-driven testing. When reasoning about higher-order functions and program constructs(e.g., loops) in program logics, proofs typically make use of second-order lemmas that encode thesemantics of those higher-order constructs and take invariants to constrain the behaviour of theirﬁrst-order arguments (e.g., of a loop body). In turn, when mechanising such proofs within Coq,
proofs of these second-order theorems become second-order programs, that, when instantiatedwith suﬃcient arguments and invariants, compute a proof term that witnesses the execution of thehigher-order construct on these inputs. Furthermore, we observe that by applying these secondorder theorems for loops to particular concrete inputs, we necessarily obtain a concrete trace ofthe program, annotated with additional meta-data capturing how the invariants are instantiatedover the course of the execution with diﬀerent concrete values and states. Proof-driven testingturns these observations into an eﬃcient strategy for validating candidate invariants for a loop. It
applies the loop’s speciﬁcation to concrete inputs and analyses the resulting proof term to extract
an executable function that tests whether a given invariant holds over a particular execution trace.
In conjunction, our solutions to C1 and C2 make it possible to reconstruct a proof for the newprogram, inferring invariants for its loops and higher-order function applications. Our approach
is mostly-automated: the veriﬁcation conditions for the invariants are discharged using domainspeciﬁc automation. A relatively small amount of manual proof eﬀort is required when automation
fails to dispatch the residual proof obligations. Crucially, no manual work is required for stating
invariants for the new program version.
Contributions. In summary, we make the following contributions.
• A methodology for mostly-automated proof repair for higher-order imperative programs written
in OCaml and veriﬁed in Separation Logic embedded into Coq (Sec. 2).
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

107:4

Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey• An algorithm for synthesising basic proof structure and invariant candidates for a refactored
program using dynamic analysis and program alignment (Sec. 3).
• Proof-driven testing—a novel approach to test properties of data and programs for validity by
extracting tests from proofs of higher-order facts that rely on those properties. We provide theintuition and formal description of the proof-driven testing methodology and show how to use it
for eﬃciently pruning the search-space of candidate invariants required for proof repair (Sec. 4).
• Sisyphus—a proof repair tool for OCaml programs veriﬁed in Coq. We evaluated Sisyphus on asuite of 14 evolved programs, of which 10 were drawn from popular OCaml libraries, and foundthat all inferred invariants for new versions were valid and required relatively small amounts ofmanual eﬀort to prove in comparison to the original programs (Sec. 5).
2 THE LABOURS OF SISYPHUS
We present an overview of Sisyphus by means of an illustrative example: repairing the proof ofcorrectness between two versions of a real-world program from a widely-used OCaml library. The
program in question is the function Seq.to_array, which converts a lazy sequence to an array,taken from the popular containers library between versions 3.61 and 3.7,2 wherein it was updated
to improve its performance. We manually veriﬁed the initial version of to_array in Coq via CFML;
Sisyphus was then used to automatically generate a repaired proof for the updated program.
2.1

An Initial Verified Seq.to_array

Fig. 1 presents the original implementation of to_array,
which converts a sequence into an array, where a sequenceof type 'a t is encoded as a thunked list:
type 'a t= unit -> 'a nodeand 'a node = Nil| Cons of 'a * (unit -> 'a node)

let to_array s =match s () with3
| Nil -> [| |]4| Cons (hd, _) ->5
let sz = length s in
6
let a = Array.make sz hd in
7
iteri
8
(fun i vl ->9a.(i) <- vl) s;
10
a
1

2

A sequence is represented by a function that, when evaluated,either returns Nil for the empty sequence, or returns a Conscell with a head element and a tail that can be evaluated ondemand to retrieve the rest of the sequence. This encoding
Fig. 1. Original to_arrayof sequences can even be used to represent lists of inﬁnite
length or encode arbitrary side-eﬀects within the thunks of a sequence. However, for the purposesof this work, we will be restricting our focus to the case in which these sequences are ﬁnite andside-eﬀect free, since to_array has undeﬁned behaviour for other cases.
The implementation of to_array is as follows. If the sequence contains at least one element, thefunction calculates its length and allocates a fresh result array with the capacity to store all of theelements of the sequence. The function then calls the higher-order iterator function iteri, whose
argument function successively assigns elements of the sequence to the corresponding slots of theallocated array, which is eventually returned as the result. Having stepped through the function, it
seems reasonable to believe that to_array is correct, and containers itself comes with an extensive
test suite. But if we truly wish to ensure the correctness of this implementation of to_array, we
should really prove its correctness.
2.1.1 Specification of Seq.to_array. In order to faithfully specify the eﬀect of to_array on theheap, we turn to a formalism tailored for that purpose—Separation Logic (SL) (O’Hearn et al. 2001;
Reynolds 2002)—a Hoare-style program logic for reasoning about heap-manipulating programs.
1 to_array in containers 3.6: https://github.com/c-cube/ocaml-containers/blob/v3.6/src/core/CCSeq.ml#L397
2 to_array in containers 3.7: https://github.com/c-cube/ocaml-containers/blob/v3.7/src/core/CCSeq.ml#L415

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

Mostly Automated Proof Repair for Verified Libraries

107:5

Assertions in Separation Logic capture constraints over disjoint partitions of the program’s heap,
called heaplets. These constraints can be combined using the separating conjunction ∗: the statement
𝐻 ∗ 𝐻 ′ asserts that the heap can be partitioned into two disjoint sub-heaps such that 𝐻 holds on theﬁrst, and 𝐻 ′ on the second. We use the standard notation 𝑎 ↦→ 𝑒 to describe a heaplet represented
by a single memory location with address 𝑎 and contents 𝑒 (pronounced “𝑎 points to 𝑒”); emp is an
SL assertion satisﬁed by an empty heap. Using these assertions, we can thus capture the semantics
of an imperative program using a Hoare triple {𝑃 } 𝑐 {𝑄 }, which asserts the following: starting inany heap state that satisﬁes 𝑃, after executing the program 𝑐, we must obtain a heap state satisfying
𝑄. In this formalism, to_array can be ascribed the following SL speciﬁcation:∀𝑠 ℓ, {𝑠 ↦→ Seq ℓ } ( Seq.to_array 𝑠) ∃𝑎, {𝑎 ↦→ Array ℓ }(1)

The precondition, {𝑠 ↦→ Seq ℓ }, states that the payload of the (universally quantiﬁed) input sequence𝑠 is modelled by a logical list ℓ, where the predicate Seq captures the fact that 𝑠 is a ﬁnite sequence
without side-eﬀects. The postcondition, ∃𝑎, {𝑎 ↦→ Array ℓ }, uses CFML’s convention of using existential quantiﬁers to encode return values and asserts that the function will return some pointer 𝑎that points to an array with contents described by ℓ, where the predicate Array encodes the fact that𝑎 points to an array on the heap.3 In other words, the speciﬁcation (1) asserts that to_array indeed
converts a sequence to an array with the same payload, and now, if proven, provides a meaningful
guarantee about the correctness of this function. Finally, note that while our post-condition does
not constrain the input sequence 𝑠, this does not aﬀect the usability of our speciﬁcation as wehave deﬁned such sequences to be pure and eﬀect-free, so they are immutable and thus allowed by
CFML’s aﬃne logic to be duplicated before passing them to the function.
2.1.2 A mechanised proof for Seq.to_array. We are now ready to verify to_array in Coq. When
proving properties about these kinds of heap-manipulating programs in Coq, the corresponding
proofs follow by stepping through the code using the reasoning rules of the program logic tosymbolically evaluate how its individual statements update the symbolic state.
Fig. 2 shows a correspondence beLemma to_array_spec : ∀ s ℓ ,{𝑠 ↦→ Seq ℓ } (to_array s) ∃𝑎,{𝑎 ↦→ Array ℓ } .
tween to_array and the Coq proof let to_array s =Proof.
(done using the CFML embedding of match s () with
xapp.
->
[| |]
SL) that establishes that the program || Nilcase nxt as [ | hd _].
Cons (hd, _) ->- xvalemptyarr.
indeed satisﬁes the spec (1). As islet sz = length s in
- xapp.
let a =
common with such SL implementaArray.make sz hd inxalloc a.
tions, each rule of the logic comesiteri
xapp (iteri_spec (fun t =>(fun i vl ->a ↦→ Array (with an associated Coq tactic that apa.(i) <- vl) s;t ++ drop (length t)plies the rule, automatically determina(make (length l) hd)))).
ing which heaplets are aﬀected by thexvals. ... Qed.
rule (i.e., its footprint). As an example,
Fig. 2. Proof of to_array in CFML.
consider the rule xapp for verifying
an application of a function 𝑓 with a continuation 𝑐 (ignore the highlighted premise for now):{𝑃 } (𝑓 𝑣) ∃𝑥, {𝑄 ′𝑥 }xapp∀𝑥, {𝑄 ′𝑥 } 𝑐 𝑥 {𝑄 }{𝑃 } (let x = 𝑓 𝑣 in 𝑐 x) {Q}(2)

In a Coq embedding of CFML, this rule is implemented as a tactic xapp, which applies a lemma thatdischarges the conclusion of the rule by emitting veriﬁcation conditions as per its premise.
3We assume an OCaml-style (rather than C-style) memory model, in which locations can store arbitrary values, e.g., arrays.

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

107:6

Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey

Consider the call to Array.make in to_array and the { s ↦→ Seq ℓ }corresponding fragment in the proof in Fig. 2. In the let a = Array.make sz hd inprogram, this expression allocates an array of size sz { s ↦→ Seq ℓ ∗ a ↦→ Array ( repeat sz hd ) }initialised with the value hd in the heap and returns a pointer to the freshly allocated data. In thecorresponding proof step, reasoning about this computation is handled using a tactic xalloc, which
updates the symbolic program state (and is captured correspondingly by the Coq proof context) to
reﬂect the semantics of the operation, as shown in the proof snippet above.
Under the hood, the xalloc tactic itself operates by applying a reasoning rule for function
application, xapp (2), to the speciﬁcation of the library function Array.make:∀sz 𝑣, {sz > 0; emp} ( Array.make sz 𝑣) ∃𝑎, {𝑎 ↦→ Array ( repeat sz 𝑣)}(3)

In particular, the spec (3) asserts that when calling Array.make with a size sz and value 𝑣 wheresz > 0, the return value of the function will be a pointer a to an array, whose contents are describedby the logical expression repeat sz 𝑣; that is, the array has sz copies of 𝑣.
The most interesting part of the proof is reasoning about the use of the higher-order function
iteri, which takes as arguments a possibly-eﬀectful function f and a sequence 𝑠, and iterates
through the sequence, calling f on each element. In order to characterise the state of the heap after
its invocation, the speciﬁcation (4) of iteri requires an invariant 𝐼 that must be maintained by f:∀𝐼 f 𝑠 ℓ, (∀𝑡 𝑣, {𝐼 𝑡 } ( f 𝑣) {𝐼 (𝑡 ++ [𝑣])}) → {𝐼 [] ∗ 𝑠 ↦→ Seq ℓ } (iteri f 𝑠) {𝐼 ℓ ∗ 𝑠 ↦→ Seq ℓ }(4)Here, invariant 𝐼 characterises the heap in terms of the preﬁx 𝑡 of the sequence that has been visitedby iteri. The premise of the speciﬁcation asserts that the function call f 𝑣 preserves the invariant
𝐼 after visiting 𝑣, i.e., 𝐼 now holds over an extended preﬁx. The conclusion of the speciﬁcation (ingrey) states the eﬀect of iteri on the state. Initially, none of the elements of 𝑠 have been seen, so
𝐼 must hold on the empty list [] in the precondition, constraining the corresponding part of theheap. As per the postcondition, after executing iteri f 𝑠, every element in the sequence has now
been visited, and so the speciﬁcation asserts that 𝐼 now holds over all elements in the sequence, ℓ.
The proof in Fig. 2 makes use of the conclusion of the speciﬁcation (4), referred to as iter_spec
in the Coq code, by providing it as the highlighted premise of the rule (2). To do so, it instantiates
iter_spec with a suitable invariant 𝐼 . This invariant argument does not directly follow from thesyntax of the program like other components of the proof, but, rather, must be explicitly provided
by the user. The invariant provided in our proof states that at each iteration of iteri, the allocatedarray a will always start with the sequence of elements 𝑡 that have been visited by the iteration:
fun 𝑡 => a ↦→ Array (𝑡 ++ drop ( length 𝑡) ( repeat ( length ℓ) hd))

(5)

In particular, this invariant asserts that the value a, previously returned by the call to Array.make,will point to an array with the same length as ℓ, where the contents of the array start with 𝑡, thepreﬁx of visited elements, and the remaining elements are all hd. At the precondition of iteri’s
speciﬁcation, we instantiate this invariant with the empty list, where a points to a list whose lengthis equal to that of ℓ and whose elements all have the value hd. Having executed iteri, the invariant
in its postcondition is instantiated with the full sequence ℓ, and so we learn that the ﬁnal contentsof the array a must have the same length as ℓ, with its contents starting with the sequence ℓ andfollowed by an empty suﬃx. Therefore, we can then show that the contents of a are exactly thesequence ℓ, thereby satisfying the post-condition of to_array and concluding the proof.
2.2 A Recipe for Proof Repair
Our proof in Fig. 2 serves as a certiﬁcate of correctness for to_array, but, alas, only for one particularversion of the function: if the implementation of to_array were to later change, then our certiﬁcate
would no longer hold, and we would have to prove correctness of the program again. This deﬁnition
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

Mostly Automated Proof Repair for Verified Libraries
Old Proof

107:7
Sisyphus

Speciﬁcation
Skeleton
Invariants

New Proof
Speciﬁcation(1) Skeleton Generation §3.1

(2)

Alignment §3.2

Obligations

Skeleton
Invariants
Obligations(2) Invariant Synthesis §3.3
New Program(3)

Invariant Testing §4

Old Program

Proof Term Instantiation §4.1

Proof Term Reduction §4.2

Candidate Pruning §4.3

Fig. 4. Sisyphus overview. Boxes with white background represent user-provided components. Light-green
boxes represent outputs generated by the tool with the dashed border around obligations representing a
best-eﬀort attempt at dispatching residual goals using user_solve or otherwise leaving them as admits.
Solid arrows correspond to inputs and outputs, and the dashed arrow encodes that specifications are copied.

of to_array in the containers library was later updated to the implementation in Fig. 3, adopting aradically diﬀerent, but more eﬃcient implementation that avoids repeated evaluation of the input
sequence. In the new implementation, the function ﬁrst traverses the entire sequence in a single
pass (line 3) using the fold iterator to fold over the elements of the sequence, using a pure function
to accumulate a tuple of the length of the sequence and the elements of the sequence in reverse(line 4). Then, having allocated a result array of a suitable length, the program simply iterates over
the reversed list of elements using List.fold_left (line 10), and assigns the elements to its result
array in reverse (lines 11-12), gradually increasing the suﬃx of the array that is shared with the
input. In this way, while both versions traverse the elements twice, the two implementations diﬀer
in the number of times the lazy sequence is “forced”: in the original version the sequence is forced
twice (by length and iteri), while the updated implementation only forces it once (using foldi).
This can have signiﬁcant performance beneﬁts when the elements capture expensive computations.
While this new version signiﬁcantly diﬀers from the orig1 let to_array s =inal implementation of Seq.to_array from Fig. 1, we can2
let sz, rls =3fold (fun (i,ls) x ->notice some striking similarities in their implementations.
4
i+1, x::ls) (0, []) s in
Most signiﬁcantly, both programs follow the same high-level5
match rls withsteps: ﬁrst (1) to calculate the length of the sequence, then6| [] -> [| |]second (2) to allocate a result array with an appropriate size,
7| init :: rest ->and ﬁnally (3) to populate this array with the elements of the
8
let a = Array.make sz init in
9
let idx = sz - 2 insequence. For example, in the old implementation, step (1)let _ = List.fold_left
is completed using a dedicated length function, while in the 10
11(fun i x -> a.(i) <- x;
new program, this is achieved in parallel with accumulating 12
i - 1) idx rest in aa reversed list of the elements of the sequence using fold.
Fig. 3. New version of to_array
Can we use these similarities between the versions of the
program to thus repair the correctness proof from Fig. 2?
The remainder of this section describes our tool Sisyphus that does exactly that.
Overview of Sisyphus. The high level overview of Sisyphus is shown in Fig. 4, which highlights
the three main stages in Sisyphus’s proof repair process:Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

107:8

Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey(1) First, following the syntactic structure of the new program, Sisyphus constructs its proof skeleton,with holes for the parts that cannot be immediately inferred (Sec. 2.2.1).
(2) Next, Sisyphus compares traces of the old and new programs on the same random inputs inorder to recover high-level relations between the individual steps in their implementations.
It uses these relations to discover relevant sections of the old proof, which are then used tosynthesise candidate expressions to ﬁll holes in the new proof skeleton (Sec. 2.2.2).
(3) Finally, Sisyphus uses a fast dynamic test to prune the space of synthesised expressions,instantiating the holes in the proof-skeleton and attempting to dispatch the resulting obligations
using user-provided proof automation, thereby completing the proof script (Sec. 2.2.3).
In this way, Sisyphus implements a mostly-automated proof repair procedure — the tool will
generate a proof-skeleton and invariants for the new proof, but residual obligations are handled
in a best-eﬀort fashion. In particular, pure domain-speciﬁc logical obligations often remain in SL
proofs after symbolically reasoning about the program (e.g., proving that a particular integer isa valid index into a list). Sisyphus allows the user to supply a tactic (which we will refer to as
user_solve), that is invoked during repair to dispatch any such obligations. In order to construct
such a tactic, one will typically use a mixture of Coq’s hint databases and proof search such as
auto/eauto. In the case the tactic fails to dispatch a goal, Sisyphus emits an admit for that particularsubgoal, which the user must then ﬁll in to complete the proof.
2.2.1 Building a proof skeleton. As we have seen 1 Lemma to_array_spec : ∀ s ℓ ,in Sec. 2.1.2, when verifying programs using SL program 2 {𝑠 ↦→ Seq ℓ } (to_array s) ∃𝑎, {𝑎 ↦→ Array ℓ }logics in Coq, the structure of the corresponding proof 34 Proof.
(* .. *) xapp (* .. *).
scripts will often mirror the structure of the program 5(* .. *) case ls as [ | init rest].
- (* .. *) xvalemptyarr. { user_solve. }being veriﬁed. Applying this insight in reverse, Sisyphus 6- (* .. *) xalloc a. (* .. *)starts its repair process by constructing an initial skeleton 78
xapp (list_fold_left_spec
proof script for the new program, traversing the program 9(fun (acc: int) (t: list A) => □)).
{ user_solve. }body and mapping program constructs to the relevant tac- 10(* .. *) xvals. { user_solve. }tics to symbolically execute them. Any obligations that 11
12
Qed.
remain following this process are delegated to a userprovided solver tactic to dispatch (here, user_solve), or Fig. 5. Proof skeleton for new to_array
admitted and left for the user in cases when the solver fails. Using this strategy, Sisyphus can automatically generate a proof skeleton for the new to_array function (Fig. 5). Each program statementin Fig. 3 maps to a particular tactic application in the proof skeleton: function applications to xapp
(lines 4 and 8), array allocation to xalloc (line 7), creating an empty array to xvalemptyarr (line 6),
and branching in the program is mirrored by a case analysis in the proof (line 5).
While this strategy automatically handles a large component of the burden of writing the new
proof script, there may still be certain parts of the new proof which cannot be immediately ﬁlled inand must be left as holes. In our case, such a hole must be left when reasoning about the applicationof List.fold_left in the program, as its speciﬁcation (6) takes an explicit invariant 𝐼 to characterise
how the program state is updated through its execution.
∀𝐼 f 𝑠 acc ′ ℓ, (∀ acc 𝑡 𝑣, {𝐼 acc 𝑡 } (f acc 𝑣) ∃res, {𝐼 res (𝑡 ++ [𝑣])}) →{𝐼 acc ′ [] ∗ 𝑠 ↦→ List ℓ } (List.fold_left f 𝑠) ∃res, {𝐼 res ℓ ∗ 𝑠 ↦→ List ℓ }(6)

The speciﬁcation (6) of fold_left is fairly similar to the speciﬁcation (4) of iteri; the key
diﬀerence being that the invariant used to constrain the behaviour of the user-supplied function
f now takes two parameters: an accumulator value acc, and a list 𝑡. As before, the 𝑡 parameter
represents a logical variable, the preﬁx of the sequence of elements that have been visited so far.
The acc parameter represents a program-level value, which is the result accumulated by the fold.
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

Mostly Automated Proof Repair for Verified Libraries

107:9

The invariant provided to this speciﬁcation must capture the shape of the heap that evolves overthe execution of the fold at each iteration, and it does not easily follow from the program syntax,
so Sisyphus leaves a hole (□) in the proof (Fig. 5) in place of the invariant body to be ﬁlled in later.
2.2.2 Transplanting invariants across proofs. To ﬁll the remaining holes in the proof, Sisyphusbuilds on a simple observation that diﬀerent versions of a program often share similar invariantsin their proofs. More precisely, statements between diﬀerent versions of a program that perform
similar operations (e.g., populating an array), will often share similarities in the assertions used toreason about the state they alter in their corresponding proofs, as in the snippets below:(* old: populate prefix of array *)iteri (fun i vl -> a.(i) <- vl) s(* new: populate suffix of array *)List.fold_left (fun i x -> a.(i) <- x; i-1) idx rest

This intuition leads to a two-step process for instantiating holes in the new proof-skeleton: ﬁrst, (1)to determine which statements in the new program perform similar operations to those from theold program, and then (2) to use relevant invariants from the old proof to guide the generation ofinvariant candidates to ﬁll the holes in the new proof.
Discovering similar computations.
let to_array s =In order to instantiate holes in thelet sz, rls =proof skeleton, we require a map- let to_array s =fold (fun (i,ls) x ->match s () with
i+1, x::ls) (0, []) s inping between the high-level steps| Nil -> [| |]match rls with| Cons (hd, _) ->of old and new programs. In other| [] -> [| |]let sz = length s in
| init :: rest ->words, what we need is a program
let a =
let a =
Array.make sz hd inalignment between the two programs,
Array.make sz init initeri
let idx = sz - 2 inwhich relates individual statements(fun i vl ->let _ =
a.(i) <- vl) s;of both programs that correspond to
List.fold_lefta(fun i x -> a.(i) <- x;
the same high-level steps. These relai - 1) idx rest in ations between the high-level steps in
Fig. 6. Alignment between two versions of to_arraya program capture semantic properties that might be hard to determine
statically, but, as it turns out, can be discovered dynamically using a simple strategy. Consider
the old and new versions of to_array, which adopt the same general strategy to implement theconversion from a sequence to array (Fig. 6): (1) compute the length of the input sequence, (2)allocate an array for the result, and (3) populate the elements of the array. While both programs use
the same steps, the implementations of these individual steps can signiﬁcantly diﬀer in execution.
For example, when populating the result array in step (3), the original implementation ﬁlls thearray from the beginning, while the new implementation does it by assigning elements from theend. However, after executing this step in both programs, the result array will contain exactly theelements of the input sequence—a fact that is easy to capture during executions of both programs:{sz = 3; a ↦→ Array ( [1; 1; 1] ) }iteri (fun i vl -> a.(i) <- vl) sonsz = 3; a ↦→ Array ( [1; 2; 3] ){sz = 3 ∧ idx = 1; a ↦→ Array ( [3; 3; 3] ) }List.fold_left (fun i x -> a.(i) <- x; i - 1) idx restonsz = 3 ∧ idx = 1; a ↦→ Array ( [1; 2; 3] )To exploit this insight for generating new invariants, Sisyphus runs both versions of the programon the same randomly generated inputs and records observations of the runtime program states
at each program point. Observations between the traces are ranked based on their similarity byusing certain metrics to compare the values of program variables in each observation. In particular,
Sisyphus uses two such metrics: comparing exact matches in runtime values, and barring an exact
match, comparing the sizes of collections such as lists, albeit with a lower priority. That is, if many
program variables have the same runtime values, then two observations are considered to be highly
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

107:10

Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey

Table 1. Mapping from Coq invariants to OCaml tests
Number(1)(2)

Logical embedding as Coq predicate(fun acc t => a ↦→Array (repeat (acc + 1) init ++drop (acc + 1) ℓ))(fun acc t => a ↦→Array ([] ++ drop 0(repeat (length t) init)))

Executable embedding as OCaml function(fun acc t -> Array.to_list a =(repeat (acc + 1) init ++drop (acc + 1) ℓ))(fun acc t -> Array.to_list a =([] ++ drop 0(repeat (length t) init)))

Valid?
YesNo

similar. A statement in one program is considered as similar to a statement in the other program
when the observations at points surrounding the respective statements are similar.
In this way, Sisyphus builds up an alignment between the statements of both programs. For
example, in Fig. 6 the call to iteri on the left is discovered to be similar to the call to fold_left
on the right as both produce arrays with the same payload, even though they do so in diﬀerent
directions, hence both statements are marked as aligned.
Generating invariant candidates. When instantiating a hole in the new proof skeleton, Sisyphus
ﬁrst uses the calculated alignment to ﬁnd the relevant statements of the old program that plausibly
correspond to the same high-level step as the current statement of the new program that needs an
explicit invariant in its proof. Looking at the proof steps from the old proof that correspond to thesestatements, Sisyphus then collects any expressions that occur in symbolic states preceding thesesteps and produces a family of sketches that are likely to capture the similarities in the invariants
between the old and new proofs by replacing sub-expressions within those invariants with holes(_). For example, when looking to synthesise an invariant for the call to fold_left in the proof of
the new program, Sisyphus discovers an aligned statement—a call to iteri—and the invariant (5)used to verify it in the corresponding proof (Fig. 2). It then extracts from the old invariant a numberof sketches, one of them being (_ ++ drop _ _), which captures the preﬁx/suﬃx argument fromthe proof of the old program and contributes the following (simpliﬁed) invariant template:fun (acc: int) (t: list A) => a ↦→ Array (_ ++ drop _ _)(7)

Finally, Sisyphus uses this template (amongst others), along with any logical functions and constantsin state assertions in the proof of the old and new program, to bootstrap an enumerative synthesis
procedure for generating concrete invariant candidates for the current hole in the proof in Fig. 5.
2.2.3 Validating invariant candidates. The last step in Sisyphus’ repair process is to validate thegenerated invariants and identify suitable candidates to instantiate the holes in the proof skeleton.
As the generation strategy can produce large numbers of candidates, validating each candidate bytrying to prove its correctness would quickly become intractable. As such, Sisyphus implements its
candidate validation step in two phases, ﬁrst running a fast dynamic test to quickly prune generated
candidates, and then using the user-provided solver to actually prove the invariant. The key insight
powering Sisyphus is that while such dynamic tests for invariants may be challenging to generatefrom scratch, we can actually automatically construct these tests from information hidden within
the proofs of the higher-order functions, using a novel technique we dub proof-driven testing.
Consider the invariant candidates for the call to fold_left in the new program generated fromthe template (7) and listed in Tab. 1.4 The ﬁrst candidate accurately describes the invariant that
holds for one iteration of fold_left’s argument function, while the second invariant is incorrect.
4We assume that the invariants are used in an environment where a and ℓ are bound, e.g., the proof in Fig. 5.

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

Mostly Automated Proof Repair for Verified Libraries

107:11

Following the intuition presented in the earlier sections, thelet ℓ= [ 1; 2; 3 ] inlet a = [| 3; 3; 3; |] inﬁrst invariant asserts that during the execution of fold_left,
let f i x = a.(i) <- x; i-1 inthe contents of the array a will share an increasing suﬃx withthe contents ℓ of the original sequence. The second invari- let len = 3 - 2 in
let inv = (* .. *) in
ant asserts that the contents of a will always be described by(* a = [ 3; 3; 3 ] *)repeat (length t) init—that is, all elements in the array willassert (inv len []);
let acc = f len 2 inalways have the same value. Our goal is to test these invariants(* a = [ 3; 2; 3 ] *)to quickly distinguish between the invalid invariant (2) and theassert (inv acc [2]);correct invariant (1). To do so, we would like to convert the
let acc = f acc 1 inlogical state properties asserted by the invariant and expressed(* a = [ 1; 2; 3 ] *)as propositions in Coq’s logic (second column of Tab. 1), into
assert (inv acc [2;1])
executable OCaml tests (third column) that check the program
values of the program via a direct syntactic translation. Com- Fig. 7. A concrete invariant test
bining this with a suitable instantiation for the free variables in the expressions (i.e., a and ℓ), we
can construct an executable program to test the invariants.
Suppose we had access to the testing program prelet rec fold_left (* I *) f acc ls =sented in Fig. 7. This program encodes a particular con(* assert (I acc []); *)crete execution trace of List.fold_left within the newlet rec loop (* t *) acc ls =implementation of to_array called on a sequence withmatch ls with| [] -> acc
the elements [1, 2, 3], annotated with appropriate asser| hd :: tl ->tions (inv). Speciﬁcally, after each step in the trace, thelet acc' = f acc hd inprogram includes an assertion that an invariant function(* assert (I acc' (t ++ [hd])); *)inv holds with the current value of accumulator variable
loop (* (t ++ [hd]) *) acc' tl in
acc and the preﬁx of the elements that have been visited
loop (* [] *) acc ls
so far. If we use our ﬁrst invariant candidate as the defFig. 8. Implementation of fold_left
inition of the inv function, then this testing function will
execute without raising an exception, as each time inv is called, the contents of the array a will
indeed match the state expected by the invariant. Conversely, if we execute this program with thedeﬁnition of inv assigned to the second invariant candidate, then the program will fail to executeto completion, as at the second call to the inv function, the contents of the array will be [3; 2; 3]
while the invariant will expect all elements to be the same.
The challenge with constructing such a test program is that it manipulates logical variables andperforms invariant checks that do not occur in the implementation of fold_left (as given in Fig. 8).
Note however that these properties could actually be obtained if we considered the execution traceof a suitably annotated version of fold_left (cf. the comments in Fig. 8) that was parameterised byadditional logical parameters (i.e., t) and contained explicit invariant checks.
The key insight of Sisyphus is that we do have access to these annotations: they are in fact contained within the proof of correctness for fold_left with regard to the speciﬁcation (6), which itself
has to manipulate and maintain these variables and checks in order to establish that the invariant
holds over the course of the entire program. Sisyphus evaluates proof terms of speciﬁcations forhigher-order functions (as well as correctness proofs for rules of a program logic) on concrete
inputs, extracting test speciﬁcations from the resulting reduced proof terms as presented in Fig. 7,
a process we dub proof-driven testing. Using these generated tests, Sisyphus can quickly prune thegenerated candidates and suggest valid invariants necessary to complete the repaired proof.
2.2.4 Putting it all together. Recall that our starting point was an old program, its SL speciﬁcation,
and a Coq proof of its correctness (Sec. 2.1). Taking those artifacts and running them throughthe sequence of steps described in Sec. 2.2.1–Sec. 2.2.3, Sisyphus produced a nearly complete
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

107:12

Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey

repaired proof with explicitly-stated high-conﬁdence invariants for calls to higher-order functions
and loops. To fully complete the proof, the user has to mechanically establish the validity of thesuggested invariants. These residual proof obligations typically boil down to proving new facts
about (a) entailment of SL assertions and (b) mathematical properties of involved data types (e.g., a
new lemma relating list reversal and concatenation)—all outside of the scope of the original proof,
and, therefore, beyond the reach of Sisyphus’s proof repair capabilities.
In the following sections we provide detailed descriptions of the outlined algorithms for reconstructing proof skeletons, computing program alignment, and synthesising invariant candidates(Sec. 3), formally deﬁne proof-driven testing via Coq proofs (Sec. 4), and elaborate on the utility
aspects of Sisyphus, including the proof burden for the residual veriﬁcation conditions (Sec. 5).
3 PROOF RECONSTRUCTION AND SYNTHESIS OF INVARIANT CANDIDATES
3.1 Generating Proof SkeletonsFig. 9 provides a subset of OCaml terms (ranged over𝑣variable namesby 𝑐) and CFML proof tactics (𝑇 ), which we will be us𝑐::= 𝑣 | fun v ⇒ c | assert c
ing for our presentation in the remainder of the paper.
| 𝑐 𝑐 | let v = c in c
For the sake of uniform treatment, we require loops in| if c then c else c
OCaml programs to be encoded as applications of higher| match 𝑣 with 𝐶𝑖 𝑣𝑖 → 𝑐𝑖order combinators that take a function, representing the
𝑇 ::= xval. | xif. {T }loop’s body, as their argument. This reduces the prob| xletval v. | xmatch. {T }lem of inferring loop invariants to inferring invariants| xapp. | xapp v (fun v ⇒ □).
for higher-order function applications. In practice, thisconvention poses little problem: most idiomatic OCaml Fig. 9. OCaml programs and Coq tactics
programs that loop are either already implemented using higher-order combinators or can be easily
rewritten to do so. A tactic xapp that implements the CFML logic rules for function applications
has two forms—the latter tackles application of higher-order functions and requires an explicit
invariant, which is initially represented by a “blank” fun 𝑣 ⇒ □ to be elaborated later.
Fig. 10 shows the rules of proof skeleton reconstruction. It is implemented as a syntax-basedtranslation {x from OCaml programs to Coq sequences of Coq tactics. It also takes the actual
veriﬁcation goal (i.e., pre-/postcondition of the residual program to be traversed) and emits a list ofresidual obligations 𝜑 that should be discharged separately. For example, the obligation emitted in
the conclusion of xval, which is typically applied at the end of the proof (cf. Fig. 2), is the heap
entailment 𝑃 ⊢ 𝑄 𝑣, which is derived immediately from the residual goal {𝑃 } {𝑄 }. Both rules xapp
and xapp-hof deal with function applications, using the function dictionary E to retrive function
speciﬁcations and adding their side conditions to the list of residual obligations. In addition to that,xif{𝑣 = true; P } {Q} ct {x Tt ; 𝜑 t{𝑣 = false; P } {Q} cf {x Tf ; 𝜑 fxapp{𝑃 } {𝑄 }; if 𝑣 then 𝑐𝑡 else 𝑐 𝑓{x xif. {𝑇𝑡 } {𝑇𝑓 }; (𝜑𝑡 , 𝜑 𝑓 )xmatch{𝑣 = 𝐶𝑖 𝑣𝑖 ; P } {Q} ci {x Ti ; 𝜑𝑖{𝑃 } {𝑄 }; match 𝑣 with 𝐶𝑖 𝑣𝑖 ⇒ 𝑐𝑖
{x xmatch. {𝑇𝑖 }; 𝜑𝑖xval{𝑃 } {𝑄 }; 𝑣 {x xval.; 𝑃 ⊢ 𝑄 𝑣

xapp-hof

E [ 𝑓 ] = ∀ 𝑥,𝜓 → {𝑃 } 𝑓 𝑥 ∃𝑥 {𝑄 ′ 𝑥 }{ (𝑄 ′ 𝑥 ) [𝑣/𝑥 ] } {𝑄 }; 𝑐 x {x 𝑇 ; 𝜑

E [ 𝑓 ] = (𝑠 : ∀𝐹, 𝑥, 𝐼,𝜓 → {𝑃 } 𝑓 𝐹 𝑥 ∃𝑥 {𝑄 ′ 𝑥 } ) 𝑑 is ﬁrst-order{ (𝑄 ′ 𝑥 ) [𝑣/𝑥, (fun w ⇒ d )/F, (fun q ⇒ □)/I] } {Q}; c x {x T ; 𝜑{𝑃 } {𝑄 }; let x = 𝑓 𝑣 in 𝑐 x {x xapp. T ;(𝜓 [𝑣/𝑥 ], 𝜑 ){𝑃 } {𝑄 }; let x = 𝑓 (fun w ⇒ d ) 𝑣 in 𝑐 x {xxapp s (fun q ⇒ □). T ; (𝜓 [𝑣/𝑥, (fun w ⇒ d )/𝐹, (fun q ⇒ □)/𝐼 ], 𝜑 )Fig. 10. Transformation from OCaml to CFML proof scripts (sequences of tactics)
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

Mostly Automated Proof Repair for Verified Libraries

107:13

ALGORITHM 3.1: Dynamic Program Alignment
Procedure DPA(𝑝, 𝑝 ′ )Input: Old program 𝑝, and a new program 𝑝 ′Output: Map 𝛼 from program points in 𝑝 ′ to 𝑝
𝑅, 𝑅 ′ ← ProgramPoints(p), ProgramPoints(𝑝 ′ )for input in GenRandInputs(𝑝 ) dotr, tr ′ ← Trace(p, input), Trace(𝑝 ′ , input)
for ⟨𝜌, 𝜌 ′ ⟩ in 𝑅 × 𝑅 ′ dops ← ProgramStateAt(tr, 𝜌 )ps′ ← ProgramStateAt(tr ′ , 𝜌 ′ )scores[𝜌 ′ ] [𝜌 ] ← Score(ps, ps′ )for 𝜌 ′ in 𝑅 ′ do𝛼 [𝜌 ′ ] ← HighestScore(scores[𝜌 ′ ] )return 𝛼

Procedure Score(ps, ps′ )Input: Old and new program state ps, ps′
Output: Integer score
𝐻, 𝐻 ′ ← Heap(ps), Heap(ps′ )𝑆, 𝑆 ′ ← Stack(ps), Stack(ps′ )vals ← Normalize(𝐻 ∪ 𝑆 )vals′ ← Normalize(𝐻 ′ ∪ 𝑆 ′ )score ← 0
for val in vals do
if val ∈ vals′ thenscore ← score + Size(val)return score

xapp-hof generates a “blank” invariant fun q ⇒ □, whose hole □ is going to be ﬁlled up later withcandidates. Our next step is to mine the building blocks for constructing such candidates from theold program’s proofs using the program alignment technique.
3.2 Computing Program Alignment
Program alignment is the mapping from program points in the new program to those in the old one
with similar program states—a crucial component in determining possible invariant candidates toﬁll holes in the reconstructed proof script. Note that alignment is a many-to-one correspondence:
many new program points can map to one old program point (but not vice versa). Algorithm 3.1
shows the main step of computing the alignment. To measure similarity of two program states, it
uses a simple Score function that only takes into the account the sizes of the aggregate values (e.g.,arrays and lists) present in both program states. Prior to computing the score, the Normalize function
transforms aggregate data types with known canonical projections to a uniﬁed representation.
For instance, both arrays and sequences are represented as lists; the user can supply their own
projections. This enables Sisyphus to compare program states bearing the same logical values
represented in diﬀerent OCaml datatypes (e.g., seq and array in to_array).
To compute the alignment 𝛼, Sisyphus generates a series of random inputs and executes bothversions of the program on them to obtain execution traces tr and tr ′ correspondingly. It records the
program state at each program point, computes the similarity to program points in the alternative
version via the Score function, and ﬁnally associates each program point in the new program withthe most similar program point in the old program.
3.3 Synthesising Invariant Candidates
Algorithm 3.2 provides an overview of the algorithm for template-based invariant synthesis. In our
approach, invariants are encoded as Coq functions that take one or more parameters and construct
a logical proposition that constrains the symbolic SL state (e.g., the invariant (5)).
Recall that, as detailed in Sec. 3.1, we generate a “blank” invariant for every application of ahigher-order function. Initially, this “blank” invariant consists of a single hole. To aid our synthesis,
in its ﬁrst step (Algorithm 3.2, left), the algorithm constructs an invariant template 𝐼 □ for a program
point 𝜌 ′ in the new program. It does so by collecting all heaplets in the program’s symbolic state,obtained by symbolic execution, immediately before 𝜌 ′ . Each heaplet has the shape 𝑣 ↦→ Π 𝑒𝑖 , where
𝑣 is a logical or program-level variable, and Π is an OCaml data type constructor (e.g., Array or ref),Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

107:14

Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey

ALGORITHM 3.2: Synthesis of invariant candidates
Procedure MakeTemplate(𝜌 ′ , vs)
Input: New program point 𝜌 ′ , invariant parameters vs
Output: Invariant template 𝐼 □𝐼 □ ← emp
for 𝑣 ↦→ Π 𝑒𝑖 in Heaplets(𝜌 ′ ) do𝐼 □ ← 𝐼 □ ∗ (𝑣 ↦→ Π _ )for 𝑣 in vs do
𝐼 □ ← 𝐼 □ ∧ (𝑣 = _ )return 𝐼 □Procedure SynthesizeCandidates(𝐼 □ , 𝛼, P, 𝑝 ′ , 𝜌 ′ )Input: Invariant template 𝐼 □ , DPA 𝛼, old proof P,
new program 𝑝 ′ , new program point 𝜌 ′Output: List of invariant candidates matching 𝐼 □𝐼 old ← GetInvariant(𝛼 (𝜌 ′ ) )sketches ← GetExpressionSketches(𝐼 old )atoms ← CollectConsts( P ) ∪ CollectFuns( P )logvars ← LogicalVars(speciﬁcation of P )return EnumSynthesis(sketches, atoms ∪ logvars, 𝐼 □ )possibly applied to arguments 𝑒𝑖 that are being replaced by a hole _. The template heaplets are thenconjoined using the SL ∗ connective. Additionally, for every parameter to the invariant (obtained
from the type of the corresponding lemma that requires it), we generate equality propositions of
the form 𝑣 = _ . For example, the template that was elaborated into the form (7) is
fun acc t => (a ↦→ Array _) ∧ (acc = _) ∧ (t = _)(8)

After inferring the template 𝐼 □ of the desired invariant, we construct concrete candidates by ﬁllingit (Algorithm 3.2, right). To do so, the algorithm ﬁrst retrieves the corresponding invariant fromthe aligned location in the old program and uses it to construct a set of sketches (i.e., expressions
with holes). It then collects constants and function symbols from the old proof, as well as logicalvariables from the ascribed speciﬁcations and uses those to ﬁll the holes in the sketches, themselves
used to instantiate holes in the template, thus completing the enumerative synthesis of candidates.
4 PROOF-DRIVEN INVARIANT TESTING
In this section, we describe the technique at the heart of Sisyphus, proof-driven testing, a means totest the validity of invariant candidates. We achieve that goal by automatically generating tests tocheck computable properties of program values and states, from proofs of higher-order lemmas.
To build an intuition for this process, let us start our reasoning by considering a simple computableproperty 𝑃 on natural numbers, deﬁned as 𝑃 𝑛 ≜ 1 + 𝑛 = 𝑛 + 1. A standard way to prove that 𝑃
holds on all natural numbers is by induction, i.e., by providing proofs of the facts 𝐻 0 : 𝑃 0 (i.e., theinduction base) and 𝐻𝑖 : ∀𝑖, 𝑃 𝑖 → 𝑃 (𝑖 + 1) (i.e., the induction transition).
𝐻 0 and 𝐻𝑖 are proof terms: following their types, we can compose them into the expression
𝐻𝑖 2 (𝐻𝑖 1 (𝐻𝑖 0 𝐻 0 ))) : 𝑃 3(9)whose type will be 𝑃 3, therefore making it a proof term for the fact that the property 𝑃 holds on
the number 3. The proof of 𝑃 3 is, therefore, constructed by applying 𝐻𝑖 , an inductive step, to twoarguments: a concrete value 2, and a sub-term constructed to have the type 𝑃 2. This sub-term
proving 𝑃 2 recursively is also constructed by applying 𝐻𝑖 again, but this time to 1 and (𝐻𝑖 0 𝐻 0 ).
The remarkable observation supported by this example is that this proof, i.e., that 𝑃 holds on thevalue 3, contains within it the information that 𝑃 must necessarily also hold on the values 2, 1,
and 0—from the fact that within its construction, it contains sub-terms proving 𝑃 𝑖 for 𝑖 ∈ {0, 1, 2}.
What does this have to do with testing invariants? Imagine that we don’t know if 𝑃 holds for
all numbers. A natural (pun intended) thing to do in this case would be to ﬁrst test that 𝑃 holds
on some numbers, e.g., 0, 1, 2, etc., up to some large number (e.g., 3). On the other hand, assumingthat 𝑃 can be proven by induction, we know that there must be witnesses (i.e., proof terms) 𝐻 0 and
𝐻𝑖 for statements 𝑃 0 and ∀𝑖, 𝑃 𝑖 → 𝑃 (𝑖 + 1), correspondingly, such that for any concrete 𝑛, 𝑃 𝑛
can be derived by repeated application of 𝐻𝑖 to smaller numbers and 𝐻 0 , as demonstrated by (9).
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

Mostly Automated Proof Repair for Verified Libraries

red-constr

red-app′𝑡𝑖 ⇓r 𝑡𝑖′′(fun 𝑥 : 𝑇 , 𝑡 ) 𝑡 ⇓r 𝑡 [𝑡 /𝑥 ]red-fun𝐶 𝑡𝑖 ⇓r 𝐶 𝑡𝑖′

107:15

red-match(match 𝐶𝑘 𝑡 𝑗 with 𝐶𝑖 𝑥 𝑗 → 𝑡𝑖′ ) ⇓r 𝑡𝑘′ [𝑡 𝑗 /𝑥 𝑗 ]red-fix𝑡 0′ = 𝐶 𝑡 ′𝑡 ⇓r 𝑡 ′′(fun 𝑥 : 𝑇 ⇒ 𝑡 ) ⇓r (fun 𝑥 : 𝑇 ⇒ 𝑡 )𝐹 = (fix 𝑓 𝑥𝑖 : 𝑇𝑖 ⇒ 𝑡 )𝐹 𝑡𝑖′ ⇓r 𝑡 [𝐹 /𝑓 , 𝑡𝑖′ /𝑥𝑖 ]Fig. 12. Selected reduction rules for CIC𝜔

By combining these two observations, we can have our main revelation: For any concrete 𝑛, theproof term 𝑡𝑛 for the proposition 𝑃 𝑛 contains sub-terms of types 𝑃 𝑖 for 𝑖 < 𝑛 within itself; bytraversing 𝑡𝑛 , we can identify each of those types 𝑃 𝑖 and convert it into a dynamically checkableassertion over a boolean expression 𝑃 (𝑖), which must not fail if 𝑃 holds universally.
As it turns out, the same observation, i.e., that a proof-term for a higher-order lemma abouta property can be used for extracting tests for this property, is not speciﬁc to statements about
natural numbers! Exactly the same principle applies to testing properties of program executions, e.g.,when 𝑃 is a guessed invariant over program states parameterised by program and logical variables.
In this case, concrete values of theose variables can be supplied by subterms of the corresponding
lemma proofs that are partially evaluated on concrete inputs.
4.1 Instantiating Proof Terms with Concrete Inputs
variable names
For the rest of this section we restrict our language to a 𝑣
subset of CIC𝜔 , the calculus of Coq, its syntax adopted 𝑡 ::= 𝑣 | 𝑡 𝑡 ′ | ∀𝑥 : 𝑡, 𝑡 ′ | fun 𝑥 : 𝑡 ⇒ 𝑡 ′from Timany and Jacobs (2015) and given in Fig. 11.
| 𝐶 𝑡 | match 𝑡 with 𝐶𝑖 𝑣𝑖 ⇒ 𝑡𝑖
The ﬁrst step in our process is to instantiate higher| fix 𝑓 𝑣𝑖 : 𝑡𝑖 : 𝑡 ⇒ 𝑡 ′order lemmas with concrete arguments and reduce theirFig. 11. Syntax of selected CIC𝜔 terms
proof terms to a head-normal form using rules from
Fig. 12. Once an expression is in head-normal form, the types of its non-reducible subterms willcontain the property of interest applied to concrete values, allowing for further test extraction.
As an example, consider instantiating and reducing the induction principle nat_ind for natural
numbers. The induction principle is implemented as a higher-order lemma whose type is∀(𝑃 : nat → Prop), 𝑃 0 → (∀𝑖, 𝑃 𝑖 → 𝑃 (𝑖 + 1)) → ∀(𝑥 : nat), 𝑃 𝑥(10)and whose proof term is a recursive function that pattern-matches over two constructors of nat:
fun 𝑃 𝐻 0 𝐻𝑖 ⇒ fix 𝐹 (𝑛 : nat) : 𝑃 𝑛 ⇒ match 𝑛 with | 0 ⇒ 𝐻 0 | 𝑆 𝑛 ′ ⇒ 𝐻𝑖 𝑛 ′ (𝐹 𝑛 ′ )(11)According to its (dependent) type (10), nat_ind takes four parameters, of which the ﬁrst three are
either properties or their proofs (which is indicated by their types), while the fourth one has typenat. In the scenario of our interest, we apply lemmas to concrete (i.e., non-proposition) arguments,
as those correspond to values that can be used for testing the validity of propositions (in this case,passed as arguments to 𝑃). Therefore, to formally replicate the example (9), we should instantiate
nat_ind with three symbolic values 𝑃, 𝐻 0 , and 𝐻𝑖 indicating proof terms or properties whose values
are irrelevant for test generation (but whose types are important), and the fourth concrete value 3.
By repeatedly applying the rules red-app, red-fix, and red-match to this expression, we reduce itto the following partially-evaluated form:
nat_ind 𝑃 𝐻 0 𝐻𝑖 3 ⇓∗r 𝐻𝑖 2 (𝐻𝑖 1 (𝐻𝑖 0 𝐻 0 ))(12)

The reduced form on the right reveals the familiar sub-terms whose types contain applications of 𝑃
to concrete values. We proceed by using this result to extract a testable speciﬁcation for 𝑃.
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

107:16

Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey

vanilla-app

Γ; 𝑡 ′ {v 𝑐 ′Γ; 𝑡 {v 𝑐Γ; 𝑡 𝑡 ′ {v 𝑐 𝑐 ′𝑥𝑖 , Γ; 𝑡𝑖′ {v 𝑐𝑖Γ; match 𝑡 with 𝐶𝑖 𝑥𝑖 : 𝑇𝑖 → 𝑡𝑖′ {vmatch 𝑐 with 𝐶𝑖 𝑥𝑖 → 𝑐𝑖

vanilla-fun

Γ; 𝑡𝑖 {v 𝑐𝑖vanilla-erase𝑡 :𝜏𝑥, Γ; 𝑡 {v 𝑐(fun 𝑥 : 𝑇 ⇒ 𝑡 ) {v (fun 𝑥 ⇒ 𝑐 )𝜏 : Prop𝑡 {v ( )vanilla-fix
𝑓 , 𝑥𝑖 , Γ; 𝑡 {v 𝑐′

𝜏 : Prop

Γ; 𝑡 {e (fun 𝑥 1 . . . 𝑥𝑛 ⇒ ( ) )Γ ⊢𝑡 :𝜏Γ ⊢ 𝜏 {t 𝑝Γ; 𝑡𝑖′ {v 𝑐𝑖′

Γ; (fix 𝑓 𝑥𝑖 : 𝑇𝑖 ⇒ 𝑡 ) 𝑡𝑖′ {vlet rec 𝑓 𝑥𝑖 = 𝑐 in 𝑓 𝑐𝑖′

extract-test

extract-propΓ ⊢𝑡 :𝜏𝜏 = 𝑡 1 . . . 𝑡𝑛 → 𝜏 ′𝐶 𝑡𝑖 : 𝜏Γ; 𝐶 𝑡𝑖 {v 𝐶 𝑐𝑖vanilla-match𝑡 {v 𝑐vanilla-ind𝜏 : Prop
Γ; 𝑡 {e 𝑐Γ; 𝑡 {e assert 𝑝; 𝑐extract-gen
Γ; 𝑣 𝑡𝑖 {f 𝑐Γ; 𝑣 𝑡𝑖 {e 𝑐Fig. 13. Vanilla extraction rules from CIC𝜔 to OCaml (top) and new rules for test extraction (bottom).
Highlighted premises are domain-specific and are instantiated for a particular set of properties.

4.2 Extracting Tests from Reduced Proof Terms
The top part of Fig. 13 presents a simpliﬁed form of the extraction relation ({v ) from Coq toOCaml (Letouzey 2008). The key rule that is relevant for our purposes is vanilla-erase, whichhandles the removal of logical parameters for the sake of producing eﬃcient executable OCaml
code: when a Coq expression 𝑡 has type in Prop, which means that it is a proof term, then Coq’s
vanilla extraction simply returns the unit value () without even inspecting 𝑡’s structure. As wewish to visit the sub-terms of logical properties to generate tests, this rule must be suitably adapted.
Our extraction mechanism (Fig. 13, bottom), updates {v with the additional three rules : extracttest, extract-prop, and extract-gen (which will be explained in Sec. 4.3). The rule extract-prop
extends the extraction making it traverse terms with type in Prop. The key addition is the rule
extract-test, which implements our earlier intuition that sub-terms witnessing a property can
encode dynamically checkable assertions for which the property must hold. In particular, whenever
we visit a sub-term inhabiting a type 𝜏 that can be converted into an executable test p (via a reﬂection
step {t ), the extraction emits an assertion that p must hold within the extracted computation. The
heavy lifting in this translation is done by the {t reﬂection rule, which is domain-speciﬁc and isinstantiated by the user for a particular set of decidable properties.
nat-refl-eq
To wrap up, let us get back to our running example. We shall instan- Γ; 𝑡 { 𝑐Γ; 𝑡 ′ {v 𝑐 ′vtiate {t with the bespoke reﬂection function (on the right) tailored for
Γ; (𝑡 = 𝑡 ′ ) {t 𝑐 = 𝑐 ′our property 𝑃 𝑛 ≜ 1 + 𝑛 = 𝑛 + 1, and use the extraction rules to convert
the normalised proof term (12) into the test-speciﬁcation (13).
𝐻𝑖 2 (𝐻𝑖 1 (𝐻𝑖 0 𝐻 0 )) {t∗assert (1 + 3 = 3 + 1); assert (1 + 2 = 2 + 1); assert (1 + 1 = 1 + 1); assert (1 + 0 = 0 + 1)

(13)

Notice that the four asserts in the OCaml program above correspond to the subterms (𝐻𝑖 2 . . .),(𝐻𝑖 1 . . .), (𝐻𝑖 0 𝐻 0 ), and 𝐻 0 , as each one inhabits the type of a concrete instantiation of 𝑃.
4.3 Testing Properties in Separation Logic
Leaving the world of properties over nat, let us now tackle our original goal, using proof-driven
testing to test separation logic properties, such as invariants. In particular, we consider an embeddingof CFML in Coq, and present how our extraction rules (cf. Fig. 14) can be extended for this domain.
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

Mostly Automated Proof Repair for Verified Libraries

refl-emp
Γ; emp {t truerefl-sep
Γ; 𝑡 {t 𝑐107:17

refl-pts

Γ; 𝑡 ′ {t 𝑐 ′Γ; 𝑡 {t 𝑐Γ; 𝑡 ∗ 𝑡 ′ {t 𝑐 && 𝑐 ′R (𝑓 ) = 𝐹

Γ; 𝑣 ↦→ 𝑓 𝑡 {t 𝐹 𝑣 = 𝑐

extract-xapp
Γ; 𝐻𝑐 {e 𝑐Γ; 𝑃 {t 𝑝Γ; xapp 𝑃 𝑄 ′ 𝑄 𝑓 𝑣 𝑏 𝐻 𝑓 𝐻𝑐 {f assert 𝑝; let 𝑥 = 𝑓 𝑣 in 𝑐 𝑥

Fig. 14. A reflection for SL properties (top); An extraction rule for xapp (bottom)

Consider a prototypical CFML rule xapp for function applications, ﬁrst seen in Sec. 2.1.2. Whenembedded as a lemma (xapp) within Coq, xapp takes the following type:∀(𝑃 : hprop) 𝑄 ′ 𝑄 𝑓 𝑣 𝑏,({𝑃 } (𝑓 𝑣) ∃𝑥, {𝑄 ′ 𝑥 }) → (∀𝑥, {𝑄 ′ 𝑥 } 𝑏 𝑥 {𝑄 }) →{𝑃 } ( let 𝑥 = 𝑓 𝑣 in 𝑏 𝑥) {𝑄 }(14)That is, the xapp lemma takes eight arguments, where the ﬁrst three are properties over the symbolic
heap (with type hprop), the next three take values, and the last two take SL proofs. Notice that,from the type of xapp, for the heap properties we pass as input (i.e., 𝑃, 𝑄 ′ , and 𝑄) no witness ispassed to the lemma. Rather, the lemma expects proofs of Hoare triples such as {𝑃 } . . . ∃𝑥, {𝑄 ′ 𝑥 }.
We do not show the proof term of xapp here, but it does not construct proof terms inhabiting 𝑃, 𝑄,
etc., either; instead, it composes the witnesses for the lemma’s argument Hoare triples. As such,
if we were to apply our extraction rules from cf. Fig. 14 to a concrete instantiation of xapp, theresulting program would not include any explicit assertions about properties over the heap.
Our goal is thus to extend our test extraction to test SL properties that hold over the heap. We ﬁrst
instantiate the reﬂection relation {t with the rules refl-emp, refl-sep, and refl-pts (cf. Fig. 14,top) to handle terms in hprop, CFML’s encoding of heap properties. The key rule in this encoding
is refl-pts that uses a mapping R to extract heap predicates (e.g., Array) to corresponding OCaml
functions that manipulate their logical contents (e.g., of_list). Applying these rules, we can now
reﬂect logical assertions over the heap into executable OCaml tests similar to the program in Fig. 7.
To assert these SL properties within our test, we ALGORITHM 4.1: Invariant testing
must tune our extraction procedure such that the test
Procedure TestInvariant(𝑝 ′ , 𝑓 , 𝑡 𝑓 , 𝐼 )programs appropriately maintain the heap, testing
Input: Program 𝑝 ′ , HOF 𝑓 , proof term for 𝑓
the predicates derived from the passed heap asser𝑡 𝑓 : args → 𝐼 → Spec, invariant 𝐼
Output: Passes if no assertion is violated
tions at the right program points. For this purpose,st, args ← RunUpto(𝑝 ′ , 𝑓 , GenInput(𝑝 ) )we now turn to the extract-gen rule (cf. Fig. 13), and𝑡 ← Instantiate(𝑡 𝑓 , 𝑎𝑟𝑔𝑠, 𝐼 )instantiate it for CFML, extending F to map CFML’s
Reduce(𝑡 ⇓r 𝑡 ′ )reasoning rules to transformations that capture their
Extract(𝑡 ′ {e 𝛿 )semantics. For example, extract-xapp (cf. Fig. 14,
RunFromState(st, 𝛿 ( ) )bottom) presents the corresponding instantiation forxapp. The essential part of the rule is the bespoke invocation of the {t procedure that converts theprecondition 𝑃 to the assertion assert p installed right before the call to f. The rule extract-xapp
does not convert the other two argument properties of xapp, 𝑄 ′ and 𝑄, which both take value
arguments, into assertions. This extension is straightforward but would require to generalise {tto handle parameterised properties; in the interest of time we did not carry out this exercise. The
encodings for the remaining rules of CFML follow the same strategy and are not presented here,
but can be found in our implementation.
Putting it all together, Algorithm 4.1 describes how Sisyphus uses proof-driven testing to prune
candidate invariants when instantiating holes in the generated proof skeleton for a given program.
When testing an invariant candidate 𝐼 for a higher-order function 𝑓 , whose application occurs in thecode of the new program 𝑝 ′ , TestInvariant ﬁrst executes the enclosing program 𝑝 ′ on a randomly
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

107:18

Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey

generated input and observes both the program state st at the call site and the concrete arguments
to 𝑓 . The concrete arguments and the invariant are passed to 𝑡 𝑓 to construct an instantiated reduced
proof term 𝑡, which is extracted into a OCaml test program 𝛿, which is executed in the context st.
If 𝛿 raises an exception during its execution, then 𝐼 is invalidated and can be pruned away.
5 IMPLEMENTATION AND EVALUATION
We have implemented Sisyphus in 19k lines of OCaml.
Component
LOC
The table on the right summarises the distribution of
Proof-skeleton generator (§3.1)
2700
implementation eﬀort, in terms of the approximate lines
Program alignment (§3.2)
1400
of code of each component of the development.5 In order
1600
Enumerative synthesis (§3.3)
to implement proof-driven testing, we include a lightly
Modiﬁed Coq reduction (§4.1)
7600
modiﬁed version of Coq’s reduction algorithm to allow
2000
Proof-driven test extraction (§4.2)
reduction within proof terms. Note that our CFML in- Reﬂection & extraction for CFML (§4.3) 1600
Miscellanea (e.g., logging, stats, etc)
1900
stantiation of proof-driven testing only requires around1600 speciﬁc LOC, which is likely a good estimate of
Total
18800
the additional eﬀort that one might expect in order toextend Sisyphus to handle proof repair in other Coq embeddings of Separation Logic. In order todispatch any obligations generated during the repair process, we implemented a domain-speciﬁcsolver as a small collection of Ltac-based tactics (∼700 LOC). An initial implementation of the tool
used Z3 (de Moura and Bjørner 2008) for this purpose; however, we found that it was not eﬀectiveat reasoning about the generated obligations, taking several minutes on even simple goals.
We conducted an empirical evaluation of Sisyphus to answer the following research questions:• RQ1: Is Sisyphus eﬀective at repairing proofs for real world programs: can it ﬁnd correct
invariants and how much manual eﬀort is required to complete the proof?
• RQ2: How eﬃcient is Sisyphus: does it generate invariants in a reasonable amount of time?
• RQ3: What are the classes of changes in programs that Sisyphus handles poorly or not at all?
Benchmarks. In order to answer these questions, we constructed a benchmark suite of 14 evolved
OCaml programs as summarised in Tab. 2. Of these programs, a majority, 10, were drawn fromreal-world code-bases, found by mining the version control of popular OCaml libraries (e.g., Jane
Street’s base, containers, etc.—cf. the accompanying artefact for their exact provenance), with theremaining ones constructed by us.
Programs were selected to exhibit the use of a diverse range of refactorings. In particular, weclassify the changes of programs in our benchmarks into four classes: (1) IterOrd, for changes in
iteration order (cf. the change in to_array), (2) DataStr, for changes in intermediate data structures,(3) Mutable/Pure for the transformation of programs using loops with mutation to pure variants,and (4) Pure/Mutable for the converse. The benchmarks we consider manipulate a range of common
OCaml data-structures: arrays, lazy sequences, mutable singly-linked-lists (SLL), stacks, queues
and trees. The main roadblock in tackling larger classes of data structures for the case studies wasin the lack of available veriﬁed implementations of these data structures. For example, though the
CFML development provides a simpliﬁed version of the OCaml Map data structure, implemented
using a balanced binary tree, it does not verify most of its associated functions.
Methodology. Our methodology to evaluate Sisyphus on these benchmark programs was asfollows: For each library function in our benchmark suite, we ﬁrst extracted the function andits dependencies into a standalone ﬁle, replacing the use of for- and while-loops with suitablehigher-order loop combinators (cf. Sec. 3.1). Then, in order to construct the initial proofs for each
5 The accompanying artefacts, Sisyphus implementation and benchmarks, are available online (Gopinathan et al. 2023).

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

Mostly Automated Proof Repair for Verified Libraries

107:19

Table 2. Categorisation of benchmark programs by the type of program changes and language features anddata structures they use (left); Comparison of additional eﬀort required to dispatch the obligations in proof
scripts produced by Sisyphus (right). † indicates when the new version of the program was constructed by
the authors, and ‡ indicates when both versions of the programs were constructed by the authors.

ExampleData Structure

Refactoring

seq_to_array
make_rev_list†
tree_to_array†
array_exists
array_ﬁnd_mapi
array_is_sorted
array_ﬁndi
array_of_rev_list
array_foldi
array_partition
stack_ﬁlter‡
stack_reverse‡
sll_partition‡
sll_of_array‡

Array, Seq
Ref
Array, Tree
Array
Array, Ref
Array
Array
Array
Array
Array
Stack
Stack
SLL
Array, SLL

IterOrd, DataStr
Mutable/Pure
IterOrd, DataStr
Mutable/Pure
Pure/Mutable
Pure/Mutable
Pure/Mutable
DataStrPure/Mutable
DataStr
DataStr
DataStr
Mutable/Pure, IterOrd
IterOrdTime (old)
Spec

Proof

Total

1hrs
5m
4hrs
10m
30m
1hr
30m
5m
10m
30m
1hr
1.5hrs1hr
1.5hrs

1hr
5m
1hr
20m
1hr
3hrs
1hr
1hr
5m
2hrs
30m
30m
1hr
30m

2hrs
10m
5hrs
30m
1.5hrs4hrs
1.5hrs1hr
15m
2.5hrs
1.5hrs
2hrs
2hrs
2hrs

Time (new)# Admits /# Obligations

17m
18m
12m
12m
2m
9m
3m
5m
11m
30s
-

3/5
0/2
2/4
2/4
2/5
2/5
3/7
2/3
0/1
3/3
3/3
1/1
0/2
0/1

program, one of the authors manually veriﬁed the implementations of each of the benchmark
programs and recorded the time taken. Sisyphus was then invoked to construct proofs for the newversions of each benchmark program. Finally, any residual obligations that were left as admits by
the tool were proven manually by another author and timed. Both authors were equally familiar
with Coq/CFML before writing any proofs, and the purpose of this experiment was to evaluate themanual eﬀort in proving the remaining obligations in relation to the initial proof eﬀort.
RQ1: Eﬀectiveness and Utility. Our experiments demonstrate that Sisyphus is eﬀective at repairing
the proofs of real world programs. Sisyphus was able to automatically construct new proofs for all
programs in our benchmarks: all synthesised invariants were valid, and we were able to manually
prove any remaining proof obligations. The fourth to the sixth columns of Tab. 2 describe thecomparison of the manual eﬀort, in terms of the time taken, to prove and specify the original
programs in comparison to using Sisyphus and manually dispatching remaining obligations. The
last column of the table (# Admits / # Obligations) describes the number of veriﬁcation conditions
that Sisyphus was unable to dispatch automatically and were left as admits for the user to prove.
We were able to construct Coq proofs for all such remaining sub-goals manually.
As can be seen from the table, all obligations took fewer than 20 minutes to dispatch, while
specifying and proving the original programs took considerably longer, demonstrating the utility of Sisyphus for maintaining veriﬁed code-bases. We found that most of the challenge incompleting proofs was in reasoning about properties of the involved functions that were notconsidered in the original development but relied on by the generated invariants. For example,
in our case study for array_partition, the generated invariant made use of an expression of theform filter 𝑝 ( filter 𝑝 ℓ). Since ﬁltering is idempotent, such repetition is redundant, but no suchproperty had been proven before, so dispatching the obligation required us to prove it manually.
RQ2: Eﬃciency. Our experiments were conducted on a commodity laptop (3.5 GHz Apple M2
MacBook Air with 8GB RAM). We have found Sisyphus to be eﬃcient at repairing proofs, taking
fewer than 2 minutes to execute on most examples in our benchmarks.
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

107:20

Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey

Table 3. Statistics of Sisyphus when repairing proofs of verified OCaml programs. The first 3 columns list the
total number of invariant candidates that were generated and their breakdown by heap and pure parts, tobe tested independently. The last 5 columns describe the time taken by Sisyphus, with the breakdown per
individual component: generation of candidates, extraction of tests, running the tests, and the remaining
tasks, which include computing program alignment and interaction with the Coq runtime.
Candidates

Exampleseq_to_array
make_rev_list
tree_to_array
array_exists
array_ﬁnd_mapi
array_is_sorted
array_ﬁndi
array_of_rev_list
array_foldi
array_partition
stack_ﬁlter
stack_reverse
sll_partition
sll_of_array

Time (s)Total (s)

Heap

Pure

Total

Generation

Extraction

Testing

Remaining

3.4 × 107
5.0 × 1061364
4.9 × 103
1.5 × 10624
1.6 × 10671
22630
2.4 × 104

1.8 × 10430
8.2 × 103
25
34
70
34
-

6.2 × 1011
30
4.0 × 1010
25
442
4.5 × 103
1.7 × 105
1.5 × 10624
1.6 × 10671
22630
2.4 × 104

28.57
≤ 10ms6.75≤ 10ms≤ 10ms≤ 10ms≤ 10ms1.72≤ 10ms3.51≤ 10ms≤ 10ms≤ 10ms
0.02

1.95
3.36
1.95
3.30
2.13
2.04
2.13
2.82
488.89
69.73
81.88
88.42
426.6255.98

20.36≤ 10ms2.98≤ 10ms≤ 10ms≤ 10ms≤ 10ms0.96≤ 10ms2.62≤ 10ms≤ 10ms≤ 10ms
0.01

5.28
11.95
13.32
13.23
13.95
15.38
19.07
15.62
15.00
17.53
21.53
16.94
16.43
13.33

58
15
25
17
17
18
22
21
504
95
104
105
443
69

In the two cases where Sisyphus takes longer than 2 minutes, array_foldi and sll_partition,
most of the time is spent on performing the extraction of tests itself, rather than generating andpruning candidates. Our implementation of proof-driven testing has not been particularly optimised,
simply reusing Coq’s infrastructure to implement extraction, so further improvements could beobtained by adopting a more specialised implementation. The second to fourth columns of Tab. 3
list the number of generated invariant candidates; Sisyphus uses a lazy generation strategy, so weonly record the number of candidates until Sisyphus ﬁnds a suitable invariant or gives up. Notethat for many of the benchmarks, Sisyphus is able to use program alignment to considerably reduce
the space of candidates, often leaving fewer than 100 candidates. Furthermore, whenever possible
Sisyphus conducts testing of pure and heap-related parts of invariant candidates independently,
rather than by taking their product, thus contributing to the eﬃciency of the search.
RQ3: Failure Modes. An important assumption of Sisyphus’s repair process is that componentsof the old proof, such as the lemmas and functions that it uses, will be suﬃcient to prove thenew program correct. As we have seen, this is not always the case. In the case of array_partition,
Sisyphus was unable to fully automatically repair the proof, as the new proof required a lemma
about repeated ﬁlters that had not been present in the old proof. In cases where the new program
requires use of a function not present in the old proof, Sisyphus’s search space will not even containan invariant that can pass proof-driven testing, and the repair process will fail entirely.
For example, consider an optimised version of to_array on the let batches = (* .. *) inright that uses a batching strategy: instead of collecting the elements let res =of the sequence into a list, it accumulates a list of batches of elements
Array.make (* .. *) inand then separately inserts each batch into the result array as on List.iter (fun batch ->let dst = (* .. *) inthe right. Sisyphus will fail to repair this program as the invariants
Array.copy batch res dst)
for its loops will require an operation to reason about ﬂattening lists
batchesof lists; however, the old proof for to_array does not make use of
any functions that can capture this operation.
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

Mostly Automated Proof Repair for Verified Libraries

107:21

6 RELATED WORK
Proof refactoring and repair. Most of the existing tools for automated proof refactoring allow
for direct manipulations of standalone proofs while preserving their validity. Levity is a tool for
the Isabelle/HOL proof assistant that simpliﬁes the motion of lemmas between diﬀerent packages
while ensuring that the automation procedures relying on those lemmas do not break (Bourke
et al. 2012). Tactitian (Adams 2015) is a tool for refactoring proof scripts in HOL Light. RefactorAgda (Wibergh 2019) and Chick (Robert 2018) are refactoring tools for programs in dependentlytyped languages that can serve as proof terms to some theorems. None of these tools address the
problem of adapting a proof about a program in response to changes in that program.
The work by Ringer (2021) focuses on proof repair in two particular scenarios: (𝑖) synthesisby-example of patches to proofs of theorems whose statements were changed to use new datatypes (Ringer et al. 2018) and (𝑖𝑖) equivalence-preserving changes in data types used by a veriﬁed
functional program and its speciﬁcation (Ringer et al. 2021, 2019b). Neither of these approaches
address arbitrary local changes in the code of a veriﬁed program; nor do they consider foundationalveriﬁcation of imperative programs, via embedded program logics or otherwise.
Techniques from non-dependently typed provers. Our work draws some parallels with earlier
research in non-dependently typed proof assistants by Matichuk (2012) on automatic extraction offunction annotations for programs in Isabelle/HOL. Matichuk describes a technique that operates on
proofs about stateful programs in monadic Hoare logic to extract intermediate state assertions intoa standalone set of function annotations, that can then be re-used to verify other inter-dependent
properties. While this approach has similarities to our proof-driven-testing algorithm, there aresome constraints arising from the non-constructive setting that limit the generality of this technique.
In particular, Matichuk’s approach requires proofs to use a particular monadic Hoare logic that has
been adjusted to collect intermediate assertions, while proof-driven testing allows extracting tests
from a larger class of theorems in pre-existing logics and is able to obtain this information for free by
introspecting the proof terms “as is”. Furthermore, the machinery in the 2012 paper only considers
ﬁrst-order imperative programs, while our proof-driven testing mechanism enables inferring
invariants for higher-order programs with combinators. That said, assuming that Matichuk’s
approach could be extended to proofs about higher-order combinators such that it stored annotations
describing how those proofs instantiate the invariants (as in our Fig. 8), we speculate that suchannotations could be used to generate tests similar to the one in Fig. 7.
KeYTestGen (Ahrendt et al. 2016) and StaDy (Petiot et al. 2014) take advantage of annotations
required by correctness proofs to generate tests with a high degree of coverage. On a conceptual
level, in contrast with KeYTestGen and StaDy, our approach is inherently higher-order, as it extract
tests for invariants (i.e., properties of programs) from proofs of lemmas that use those invariants,
while the mentioned tools target testing of programs themselves.
Invariant inference. Inference of loop invariants for imperative programs using static (Flanagan
and Leino 2001; Henzinger et al. 2004; Qin et al. 2013) and dynamic (Ernst et al. 1999, 2000) analysis,
as well as machine learning techniques (Si et al. 2018) is a well-studied research topic.
Magill et al. (2006) were amongst the ﬁrst to describe a heuristic procedure for automaticallyinferring SL invariants via static analysis relying on predicate abstraction (Das et al. 1999; Graf andSaïdi 1997) for programs manipulating linked lists. In contrast with Magill et al.’s work, our approachis based on dynamic analysis techniques and does not require a predeﬁned set of predicates, neither
heap- nor pure ones, as those are drawn from the old proofs.
The data-driven tools Locust (Brockschmidt et al. 2017) and SLING (Le et al. 2019) use dynamic
analysis to derive SL formulas describing the shape of a state manipulated by a C program as well as

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

107:22

Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey

the program’s loop invariants. Both of these tools target proofs of memory safety and do not consider
full functional correctness w.r.t. arbitrary speciﬁcations, limiting the language of pure assertions tothe ﬁrst-order logic with arithmetic comparisons. For the validation of inferred invariants, Locust
relies on the automated non-foundational veriﬁcation tool GRASShopper (Piskac et al. 2014), while
the authors of SLING report poor experience with SMT solvers and had to resort to manual (i.e.,
non machine-assisted) invariant checking (cf. Sec. 5.3 of Le et al. (2019)).
Of the state-of-the-art deductive veriﬁcation tools, only Why3 (Filliâtre and Paskevich 2013)
allows for a limited form of invariant inference using numeric abstract domains and does notsupport arbitrary eﬀectful functions or statements about shape properties of data (e.g., constraining
contents of an array). We are not aware of any approach comparable to Sisyphus in its ability
to automatically infer complex invariants which constrain both heap and data for higher-orderimperative programs, and then use these invariants to reconstruct proofs for modiﬁed programs.
Automated foundational proofs in Separation Logic. Foundational approaches to program veriﬁcation encode the meta-theory and the rules of a domain-speciﬁc logic (e.g., a version of SL)
in terms of the logic of the host veriﬁer (e.g., Coq). In this work, we considered libraries written
in a higher-order imperative language and veriﬁed in a foundational encoding of SL into Coq,
which enabled proof reconstruction and eﬃcient pruning of invariant candidates as described inSec. 3 and 4. Our contributions are complementary to the eﬀorts in automated foundational SLbased veriﬁcation of sequential (Gonthier et al. 2011; Sammler et al. 2021) and concurrent (Mulder
et al. 2022) heap-manipulating programs, as all those tools require explicit invariants.
Even though our current implementation of Sisyphus only supports a particular Coq-embedded
SL, namely, CFML (Charguéraud 2020), we believe that our approach would be applicable to manyother foundational SL implementations: HTT (Nanevski et al. 2010), Bedrock (Chlipala 2011),
VST (Appel 2011), CHL (Chen et al. 2015), FCSL (Sergey et al. 2015), and the large family of logics
based on the Iris framework (Iris Project 2022). As explained in Sec. 4.3, to support a custom SL
embedding, one would have to elaborate test extraction by implementing reﬂection procedures forembedding-speciﬁc encodings of SL assertions and rules.
7 CONCLUSION
In this work we have presented Sisyphus, a tool for the mostly-automated repair of veriﬁed
libraries. Our repair procedure is implemented through two dynamic analyses: a dynamic programalignment for recovering relations between old and new programs, and proof-driven testing for
quickly pruning candidate invariants, with the latter being a novel construction introduced inthis work. Our experimental results show that the combination of these techniques is eﬀective atconstraining the search space of repairs, and allows Sisyphus to produce repaired proofs in only a
few minutes for most cases; while the generated proofs are sometimes incomplete, the remaining
proof obligations are typically of a reasonable diﬃculty and pose signiﬁcantly less challenge thanwriting the initial proof. Our current implementation only supports the CFML embedding of SL;
however, our techniques have been designed where possible to be parametric over the logic, so we
expect can be generalised to other logics and programming languages. We leave these opportunities
as exciting future work in making maintainable veriﬁed software less of a Sisyphean task.
ACKNOWLEDGMENTS
We thank Andreea Costea, Leonidas Lampropoulous, Yunjeong Lee, Peter Müller, and George Pîrlea
for their feedback on drafts of this paper. We also thank the anonymous PLDI’23 PC and AEC
reviewers as well as our shepherd Adam Chlipala for their constructive and insightful comments.
This work was partially supported by a Singapore Ministry of Education (MoE) Tier 3 grant“Automated Program Repair” MOE-MOET32021-0001 and Tier 1 grant T1 251RES2108.
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

Mostly Automated Proof Repair for Verified Libraries

107:23DATA AVAILABILITY
The software artefact accompanying this paper is available online (Gopinathan et al. 2023). The
artefact contains the source code and build scripts for Sisyphus, a corpus of OCaml programs thatcan be used to reproduce the experimental results described in Sec. 5, a self-contained Docker ﬁleto automate setting up the development environment, and a README ﬁle in markdown that provides
detailed step-by-step instructions for running Sisyphus and the experiments.
REFERENCES
Mark Adams. 2015. Refactoring Proofs with Tactician. In SEFM (LNCS, Vol. 9509). Springer, 53–67. https://doi.org/10.1007/9783-662-49224-6_6
Wolfgang Ahrendt, Christoph Gladisch, and Mihai Herda. 2016. Proof-based Test Case Generation. In Deductive Software
Veriﬁcation - The KeY Book - From Theory to Practice. LNCS, Vol. 10001. Springer, 415–451. https://doi.org/10.1007/978-3319-49812-6_12
Andrew W. Appel. 2011. Veriﬁed Software Toolchain - (Invited Talk). In ESOP (LNCS, Vol. 6602). Springer, 1–17. https://doi.org/10.1007/978-3-642-19718-5_1
Andrew W. Appel and David A. Naumann. 2020. Veriﬁed sequential Malloc/Free. In ISMM. ACM, 48–59. https://doi.org/10.
1145/3381898.3397211
Timothy Bourke, Matthias Daum, Gerwin Klein, and Rafal Kolanski. 2012. Challenges and Experiences in Managing
Large-Scale Proofs. In 11th International Conference Intelligent Computer Mathematics (CICM) (LNCS, Vol. 7362). Springer,
32–48. https://doi.org/10.1007/978-3-642-31374-5_3
Marc Brockschmidt, Yuxin Chen, Pushmeet Kohli, Siddharth Krishna, and Daniel Tarlow. 2017. Learning Shape Analysis. In
SAS (LNCS, Vol. 10422). Springer, 66–87. https://doi.org/10.1007/978-3-319-66706-5_4
Arthur Charguéraud. 2011. Characteristic Formulae for the Veriﬁcation of Imperative Programs. In ICFP. ACM, 418–430.
https://doi.org/10.1145/2034773.2034828
Arthur Charguéraud. 2020. Separation Logic for Sequential Programs (Functional Pearl). Proc. ACM Program. Lang. 4, ICFP
(2020), 116:1–116:34. https://doi.org/10.1145/3408998
Arthur Charguéraud, Jean-Christophe Filliâtre, François Pottier, and Mário Pereira. 2017. VOCAL – A Veriﬁed OCaml
Library. In ML Family Workshop.
Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2015. Using Crash
Hoare logic for certifying the FSCQ ﬁle system. In SOSP. ACM, 18–37. https://doi.org/10.1145/2815400.2815402
Adam Chlipala. 2011. Mostly-automated veriﬁcation of low-level programs in computational separation logic. In PLDI.
ACM, 234–245. https://doi.org/10.1145/1993498.1993526
Satyaki Das, David L. Dill, and Seungjoon Park. 1999. Experience with Predicate Abstraction. In CAV (LNCS, Vol. 1633),
Nicolas Halbwachs and Doron A. Peled (Eds.). Springer, 160–171. https://doi.org/10.1007/3-540-48683-6_16
Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An Eﬃcient SMT Solver. In TACAS (LNCS, Vol. 4963). Springer,
337–340. https://doi.org/10.1007/978-3-540-78800-3_24
Richard A. DeMillo, Richard J. Lipton, and Alan J. Perlis. 1977. Social Processes and Proofs of Theorems and Programs. In
POPL. ACM, 206–214. https://doi.org/10.1145/512950.512970
Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2019. Simple High-Level Code for
Cryptographic Arithmetic - With Proofs, Without Compromises. In IEEE Symposium on Security and Privacy. IEEE.
https://doi.org/10.1109/SP.2019.00005
Michael D. Ernst, Jake Cockrell, William G. Griswold, and David Notkin. 1999. Dynamically Discovering Likely Program
Invariants to Support Program Evolution. In ICSE. ACM, 213–224. https://doi.org/10.1145/302405.302467
Michael D. Ernst, Adam Czeisler, William G. Griswold, and David Notkin. 2000. Quickly detecting relevant program
invariants. In ICSE. ACM, 449–458. https://doi.org/10.1145/337180.337240
Jean-Christophe Filliâtre and Andrei Paskevich. 2013. Why3 - Where Programs Meet Provers. In ESOP (LNCS, Vol. 7792).
Springer, 125–128. https://doi.org/10.1007/978-3-642-37036-6_8
Cormac Flanagan and K. Rustan M. Leino. 2001. Houdini, an Annotation Assistant for ESC/Java. In FME (LNCS, Vol. 2021).
Springer, 500–517. https://doi.org/10.1007/3-540-45251-6_29
Robert W. Floyd. 1967. Assigning Meanings to Programs. Proceedings of Symposium on Applied Mathematics 19 (1967),
19–32.
Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, and Derek Dreyer. 2011. How to make ad hoc proof automation lessad hoc. In ICFP. ACM, 163–175. https://doi.org/10.1145/2034773.2034798
Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey. 2023. Reproduction Artefact for Article “Mostly Automated Proof Repair
for Veriﬁed Libraries". https://doi.org/10.5281/zenodo.7703886
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

107:24

Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey

Susanne Graf and Hassen Saïdi. 1997. Construction of Abstract State Graphs with PVS. In CAV (LNCS, Vol. 1254). Springer,
72–83. https://doi.org/10.1007/3-540-63166-6_10
Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016.
CertiKOS: An Extensible Architecture for Building Certiﬁed Concurrent OS Kernels. In OSDI. USENIX Association,
653–669.
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath T. V. Setty, andBrian Zill. 2015. IronFleet: proving practical distributed systems correct. In SOSP. ACM, 1–17. https://doi.org/10.1145/
2815400.2815428
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L. McMillan. 2004. Abstractions from proofs. In POPL.
ACM, 232–244. https://doi.org/10.1145/964001.964021
C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12, 10 (1969), 576–580. https://doi.org/10.1145/363235.363259
The Iris Project. 2022. Iris: a Higher-Order Concurrent Separation Logic Framework, implemented and veriﬁed in the Coq
proof assistant. https://iris-project.org/ Online; last accessed 6 November 2022.
Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. 2011. VeriFast: A
Powerful, Sound, Predictable, Fast Veriﬁer for C and Java. In NASA Formal Methods (LNCS, Vol. 6617). Springer, 41–55.
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai
Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: formal
veriﬁcation of an OS kernel. In SOSP. ACM, 207–220. https://doi.org/10.1145/1629575.1629596
Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: a veriﬁed implementation of ML. In
POPL. ACM, 179–192. https://doi.org/10.1145/2535838.2535841
Ton Chanh Le, Guolong Zheng, and ThanhVu Nguyen. 2019. SLING: Using Dynamic Analysis to Infer Program Invariants
in Separation Logic. In PLDI. ACM, 788–801. https://doi.org/10.1145/3314221.3314634
K. Rustan M. Leino. 2010. Dafny: An Automatic Program Veriﬁer for Functional Correctness. In LPAR (LNCS, Vol. 6355).
Springer, 348–370. https://doi.org/10.1007/978-3-642-17511-4_20
Xavier Leroy. 2006. Formal certiﬁcation of a compiler back-end or: programming a compiler with a proof assistant. In POPL.
ACM, 42–54. https://doi.org/10.1145/1111037.1111042
Pierre Letouzey. 2008. Extraction in Coq: An Overview. In 4th Conference on Computability in Europe (CiE) (LNCS, Vol. 5028).
Springer, 359–369. https://doi.org/10.1007/978-3-540-69407-6_39
Stephen Magill, Aleksandar Nanevski, Edmund Clarke, and Peter Lee. 2006. Inferring Invariants in Separation Logic for
Imperative List-Processing Programs. The third workshop on Semantics, Program Analysis and Computing Environments
for Memory Management (SPACE) 1, 1, 5–7.
Daniel Matichuk. 2012. Automatic Function Annotations for Hoare Logic. In Proceedings Seventh Conference on Systems
Software Veriﬁcation (SSV) (EPTCS, Vol. 102). 46–56. https://doi.org/10.4204/EPTCS.102.6
Ike Mulder, Robbert Krebbers, and Herman Geuvers. 2022. Diaframe: automated veriﬁcation of ﬁne-grained concurrent
programs in Iris. In PLDI. ACM, 809–824. https://doi.org/10.1145/3519939.3523432
Peter Müller, Malte Schwerhoﬀ, and Alexander J. Summers. 2016. Viper: A Veriﬁcation Infrastructure for Permission-Based
Reasoning. In VMCAI (LNCS, Vol. 9583). Springer, 41–62. https://doi.org/10.1007/978-3-662-49122-5_2
Aleksandar Nanevski, Viktor Vafeiadis, and Josh Berdine. 2010. Structuring the veriﬁcation of heap-manipulating programs.
In POPL. 261–274. https://doi.org/10.1145/1706299.1706331
Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local Reasoning about Programs that Alter Data Structures.
In CSL (LNCS, Vol. 2142). Springer, 1–19. https://doi.org/10.1007/3-540-44802-0_1
Guillaume Petiot, Bernard Botella, Jacques Julliand, Nikolai Kosmatov, and Julien Signoles. 2014. Instrumentation of
Annotated C Programs for Test Generation. In 14th IEEE International Working Conference on Source Code Analysis andManipulation (SCAM). IEEE Computer Society, 105–114. https://doi.org/10.1109/SCAM.2014.19
Ruzica Piskac, Thomas Wies, and Damien Zuﬀerey. 2014. GRASShopper - Complete Heap Veriﬁcation with Mixed
Speciﬁcations. In TACAS (LNCS, Vol. 8413). Springer, 124–139. https://doi.org/10.1007/978-3-642-54862-8_9
Nadia Polikarpova, Julian Tschannen, and Carlo A. Furia. 2018. A fully veriﬁed container library. Formal Aspects Comput.
30, 5 (2018), 495–523. https://doi.org/10.1007/s00165-017-0435-1
Shengchao Qin, Guanhua He, Chenguang Luo, Wei-Ngan Chin, and Xin Chen. 2013. Loop invariant synthesis in a combined
abstract domain. J. Symb. Comput. 50 (2013), 386–408. https://doi.org/10.1016/j.jsc.2012.08.007
Vincent Rahli, Ivana Vukotic, Marcus Völp, and Paulo Jorge Esteves Veríssimo. 2018. Velisarios: Byzantine Fault-Tolerant
Protocols Powered by Coq. In ESOP (LNCS, Vol. 10801), Amal Ahmed (Ed.). Springer, 619–650. https://doi.org/10.1007/9783-319-89884-1_22
John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS. IEEE Computer Society,55–74. https://doi.org/10.1109/LICS.2002.1029817
Talia Ringer. 2021. Proof Repair. Ph. D. Dissertation. University of Washington, USA.

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.

Mostly Automated Proof Repair for Verified Libraries

107:25

Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock. 2019a. QED at Large: A Survey of Engineeringof Formally Veriﬁed Software. Found. Trends Program. Lang. 5, 2-3 (2019), 102–281. https://doi.org/10.1561/2500000045
Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, and Dan Grossman. 2021. Proof repair across type equivalences.
In PLDI. ACM, 112–127. https://doi.org/10.1145/3453483.3454033
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. 2018. Adapting proof automation to adapt proofs. In CPP.
ACM, 115–129. https://doi.org/10.1145/3167094
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. 2019b. Ornaments for Proof Reuse in Coq. In ITP (LIPIcs,
Vol. 141). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 26:1–26:19. https://doi.org/10.4230/LIPIcs.ITP.2019.26
Valentin Robert. 2018. Front-end tooling for building and maintaining dependently-typed functional programs. Ph. D.
Dissertation. University of California, San Diego, USA.
Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg. 2021. ReﬁnedC:
automating the foundational veriﬁcation of C code with reﬁned ownership types. In PLDI. ACM, 158–174. https://doi.org/10.1145/3453483.3454036
Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015. Mechanized veriﬁcation of ﬁne-grained concurrent programs.
In PLDI. ACM, 77–87. https://doi.org/10.1145/2737924.2737964
Xujie Si, Hanjun Dai, Mukund Raghothaman, Mayur Naik, and Le Song. 2018. Learning Loop Invariants for Program
Veriﬁcation. In NeurIPS. 7762–7773.
Amin Timany and Bart Jacobs. 2015. First Steps Towards Cumulative Inductive Types in CIC. In ICTAC (LNCS). Springer,
608–617. https://doi.org/10.1007/978-3-319-25150-9_36
Karin Wibergh. 2019. Automatic refactoring for Agda. Master’s thesis. Chalmers University of Technology and University ofGothenburg.
James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas E. Anderson.
2015. Verdi: a framework for implementing and formally verifying distributed systems. In PLDI. ACM, 357–368. https://doi.org/10.1145/2737924.2737958
Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas E. Anderson. 2016. Planning forchange in a formal veriﬁcation of the raft consensus protocol. ACM, 154–165. https://doi.org/10.1145/2854065.2854081

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 107. Publication date: June 2023.