@techreport(AGERWALA78,
 author       = {T. Agerwala and J. Misra},
 year         = {1978},
 title        = {Assertion Graphs for Verifying and Synthesizing Programs},
 type         = {Technical Report},
 number       = {83},
 institution  = {University of Texas, Austin},
 doi          = {10.1.1.13.1126},
)
@article(BOL93,
 author       = {R. Bol},
 year         = {1993},
 title        = {{Loop Checking in Partial Deduction}},
 journal      = {Journal of Logic Programming},
 volume       = {16},
 number       = {1--2},
 pages        = {25--46},
 doi          = {10.1016/0743-1066(93)90022-9},
)
@inproceedings(COUSOT78,
 author       = {P. Cousot and N. Halbwachs},
 year         = {1978},
 title        = {Automatic Discovery of Linear Restraints Among Variables of a Program},
 booktitle    = {Proceedings of the ACM Symposium on Principles of Programming Languages},
 pages        = {84--96},
 doi          = {10.1145/512760.512770},
)
@inproceedings(DAS99,
 author       = {S. Das and D.L. Dill and S. Park},
 year         = {1999},
 title        = {Experience With Predicate Abstraction},
 booktitle    = {International Conference on Computer Aided Verification},
 series       = {LNCS},
 volume       = {1633},
 publisher    = {Springer},
 pages        = {160--171},
 doi          = {10.1007/3-540-48683-6\_16},
)
@incollection(DERSHOWITZ90,
 author       = {N. Dershowitz and J.-P. Jouannaud},
 year         = {1990},
 title        = {Rewrite Systems},
 editor       = {J. van Leeuwen},
 booktitle    = {Handbook of Theoretical Computer Science},
 publisher    = {Elsevier},
 pages        = {244--320},
 doi          = {10.1016/B978-0-444-88074-1.50011-1},
)
@article(DIJKSTRA75,
 author       = {E.W. Dijkstra},
 year         = {1975},
 title        = {Guarded Commands, Nondeterminacy and Formal Derivation of Programs},
 journal      = {Communications of the ACM},
 volume       = {18},
 pages        = {453--457},
 doi          = {10.1145/360933.360975},
)
@article(ERNST01,
 author       = {M. Ernst and J. Cockrell and W. Griswold and D. Notkin},
 year         = {2001},
 title        = {Dynamically Discovering Likely Program Invariants to Support Program Evolution},
 journal      = {IEEE Transactions in Software Engineering},
 volume       = {27},
 number       = {2},
 pages        = {1--25},
 doi          = {10.1109/32.908957},
)
@inproceedings(FLANAGAN02,
 author       = {C. Flanagan and S. Qadeer},
 year         = {2002},
 title        = {Predicate Abstraction for Software Verification},
 booktitle    = {Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 publisher    = {ACM Press},
 pages        = {191--202},
 doi          = {10.1145/503272.503291},
)
@inproceedings(FLOYD67,
 author       = {R.W. Floyd},
 year         = {1967},
 title        = {Assigning Meanings to Programs},
 booktitle    = {Proceedings of the American Mathematical Society Symposia on Applied Mathematics},
 volume       = {19},
 pages        = {19--32},
 doi          = {10.1090/psapm/019/0235771},
)
@incollection(FURIA10,
 author       = {C.A. Furia and B. Meyer},
 year         = {2010},
 title        = {Inferring Loop Invariants Using Postconditions},
 booktitle    = {Fields of Logic and Computation},
 publisher    = {Springer},
 pages        = {277--300},
 doi          = {10.1007/978-3-642-15025-8\_15},
)
@inproceedings(GRAF97,
 author       = {S. Graf and H. Saidi},
 year         = {1997},
 title        = {Construction of Abstract State Graphs With PVS},
 booktitle    = {International Conference on Computer Aided Verification},
 series       = {LNCS},
 volume       = {1254},
 publisher    = {Springer},
 pages        = {72--83},
 doi          = {10.1007/3-540-63166-6\_10},
)
@article(HAMILTON06,
 author       = {G. W. Hamilton},
 year         = {2006},
 title        = {{P}oit\'{i}n: {D}istilling {T}heorems {F}rom {C}onjectures},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {151},
 number       = {1},
 pages        = {143--160},
 doi          = {10.1016/j.entcs.2005.11.028},
)
@inproceedings(HAMILTON07A,
 author       = {G.W. Hamilton},
 year         = {2007},
 title        = {{D}istillation: {E}xtracting the {E}ssence of {P}rograms},
 booktitle    = {Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation},
 pages        = {61--70},
 doi          = {10.1145/1244381.1244391},
)
@article(HAMILTON07B,
 author       = {G.W. Hamilton},
 year         = {2007},
 title        = {Distilling Programs for Verification},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {190},
 number       = {4},
 pages        = {17--32},
 doi          = {10.1016/j.entcs.2007.09.005},
)
@inproceedings(HAMILTON12,
 author       = {G.W. Hamilton and N.D. Jones},
 year         = {2012},
 title        = {Distillation With Labelled Transition Systems},
 booktitle    = {Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation},
 publisher    = {ACM},
 pages        = {15--24},
 doi          = {10.1145/2103746.2103753},
)
@article(HIGMAN52,
 author       = {G. Higman},
 year         = {1952},
 title        = {{Ordering by Divisibility in Abstract Algebras}},
 journal      = {{Proceedings of the London Mathematical Society}},
 volume       = {2},
 pages        = {326--336},
 doi          = {10.1112/plms/s3-2.1.326},
)
@article(HOARE69,
 author       = {C.A.R. Hoare},
 year         = {1969},
 title        = {An Axiomatic Basis for Computer Programming},
 journal      = {Communications of the ACM},
 volume       = {12},
 pages        = {576--583},
 doi          = {10.1145/363235.363259},
)
@inproceedings(IRELAND06,
 author       = {A. Ireland},
 year         = {2006},
 title        = {Towards Automatic Assertion Refinement for Separation Logic},
 booktitle    = {Proceedings of the International Conference on Automated Software Engineering},
 pages        = {209--312},
 doi          = {10.1109/ASE.2006.69},
)
@inproceedings(IRELAND97,
 author       = {A. Ireland and J. Stark},
 year         = {1997},
 title        = {On the Automatic Discovery of Loop Invariants},
 booktitle    = {Fourth Nasa Langley Formal Methods Workshop},
 pages        = {137--152},
 doi          = {10.1.1.16.9466},
)
@techreport(KLYUCHNIKOV10A,
 author       = {I. Klyuchnikov},
 year         = {2010},
 title        = {{Supercompiler HOSC 1.1: Proof of Termination}},
 type         = {Preprint},
 number       = {21},
 institution  = {Keldysh Institute of Applied Mathematics, Moscow},
 doi          = {10.1.1.182.2914},
)
@article(KRUSKAL60,
 author       = {J.B. Kruskal},
 year         = {1960},
 title        = {{W}ell-{Q}uasi {O}rdering, the {T}ree {T}heorem, and {V}azsonyi's {C}onjecture},
 journal      = {{Transactions of the American Mathematical Society}},
 volume       = {95},
 pages        = {210--225},
 doi          = {10.2307/1993287},
)
@inproceedings(LEUSCHEL98,
 author       = {M. Leuschel},
 year         = {1998},
 title        = {{O}n the {P}ower of {H}omeomorphic {E}mbedding for {O}nline {T}ermination},
 booktitle    = {Proceedings of the International Static Analysis Symposium, Pisa, Italy},
 pages        = {230--245},
 doi          = {10.1007/3-540-49727-7\_14},
)
@phdthesis(MARLET94,
 author       = {R. Marlet},
 year         = {1994},
 title        = {Vers une Formalisation de l'\'{E}valuation Partielle},
 school       = {Universit\'{e} de Nice - Sophia Antipolis},
)
@inproceedings(OHEARN01,
 author       = {P. O'Hearn and J. Reynolds and Y. Hongseok},
 year         = {2001},
 title        = {Local Reasoning About Programs That Alter Data Structures},
 booktitle    = {Proceedings of Computer Science Logic},
 series       = {Lecture Notes in Computer Science},
 volume       = {2142},
 pages        = {1--19},
 doi          = {10.1007/3-540-44802-0\_1},
)
@inproceedings(REYNOLDS02,
 author       = {J.C. Reynolds},
 year         = {2002},
 title        = {Separation Logic: A Logic for Shared Mutable Data Structures},
 booktitle    = {Proceedings of the Symposium on Logic in Computer Science},
 pages        = {55--74},
 doi          = {10.1109/LICS.2002.1029817},
)
@inproceedings(SAIDI99,
 author       = {H. Saidi and N. Shankar},
 year         = {1999},
 title        = {Abstract and Model Check While You Prove},
 booktitle    = {International Conference on Computer Aided Verification},
 series       = {{L}ecture {N}otes in {C}omputer {S}cience},
 volume       = {1633},
 publisher    = {Springer},
 pages        = {443--454},
 doi          = {10.1007/3-540-48683-6\_38},
)
@inproceedings(SANKARANARAYANAN04,
 author       = {S. Sankaranarayanan and H. Sipma and Z. Manna},
 year         = {2004},
 title        = {Non-Linear Loop Invariant Generation Using Gr{\tmspace+\medmuskip{.2222em}o}bner Bases},
 booktitle    = {{Proceedings of the ACM Symposium on Principles of Programming Languages}},
 pages        = {318--329},
 doi          = {10.1145/964001.964028},
)
@article(SORENSEN94B,
 author       = {S{\o}rensen, M.H. and R. Gl{\"u}ck},
 year         = {1994},
 title        = {{An Algorithm of Generalization in Positive Supercompilation}},
 journal      = {{Lecture Notes in Computer Science}},
 volume       = {787},
 pages        = {335--351},
 doi          = {10.1.1.49.1869},
)
@article(SORENSEN96,
 author       = {S{\o}rensen, M.H. and R. Gl{\"u}ck and N.D. Jones},
 year         = {1996},
 title        = {{A Positive Supercompiler}},
 journal      = {Journal of Functional Programming},
 volume       = {6},
 number       = {6},
 pages        = {811--838},
 doi          = {10.1017/S0956796800002008},
)
@inproceedings(SUZUKI77,
 author       = {N. Suzuki and K. Ishihata},
 year         = {1977},
 title        = {Implementation of an Array Bound Checker},
 booktitle    = {4th ACM Symposium on Principles of Programming Languages},
 publisher    = {ACM Press},
 pages        = {132--143},
 doi          = {10.1145/512950.512963},
)
@inproceedings(XU00,
 author       = {Z. Xu and B. Reps, T. amd Miller},
 year         = {2000},
 title        = {Safety Checking of Machine Code},
 booktitle    = {ACM SIGPLAN Conference on Programming Language Design and Implementation},
 publisher    = {ACM Press},
 pages        = {70--82},
 doi          = {10.1145/349299.349313},
)