T. Agerwala & J. Misra (1978):
Assertion Graphs for Verifying and Synthesizing Programs.
Technical Report 83.
University of Texas, Austin,
doi:10.1.1.13.1126.
R. Bol (1993):
Loop Checking in Partial Deduction.
Journal of Logic Programming 16(1–2),
pp. 25–46,
doi:10.1016/0743-1066(93)90022-9.
P. Cousot & N. Halbwachs (1978):
Automatic Discovery of Linear Restraints Among Variables of a Program.
In: Proceedings of the ACM Symposium on Principles of Programming Languages,
pp. 84–96,
doi:10.1145/512760.512770.
S. Das, D.L. Dill & S. Park (1999):
Experience With Predicate Abstraction.
In: International Conference on Computer Aided Verification,
LNCS 1633.
Springer,
pp. 160–171,
doi:10.1007/3-540-48683-6_16.
N. Dershowitz & J.-P. Jouannaud (1990):
Rewrite Systems.
In: J. van Leeuwen: Handbook of Theoretical Computer Science.
Elsevier,
pp. 244–320,
doi:10.1016/B978-0-444-88074-1.50011-1.
E.W. Dijkstra (1975):
Guarded Commands, Nondeterminacy and Formal Derivation of Programs.
Communications of the ACM 18,
pp. 453–457,
doi:10.1145/360933.360975.
M. Ernst, J. Cockrell, W. Griswold & D. Notkin (2001):
Dynamically Discovering Likely Program Invariants to Support Program Evolution.
IEEE Transactions in Software Engineering 27(2),
pp. 1–25,
doi:10.1109/32.908957.
C. Flanagan & S. Qadeer (2002):
Predicate Abstraction for Software Verification.
In: Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.
ACM Press,
pp. 191–202,
doi:10.1145/503272.503291.
R.W. Floyd (1967):
Assigning Meanings to Programs.
In: Proceedings of the American Mathematical Society Symposia on Applied Mathematics 19,
pp. 19–32,
doi:10.1090/psapm/019/0235771.
C.A. Furia & B. Meyer (2010):
Inferring Loop Invariants Using Postconditions.
In: Fields of Logic and Computation.
Springer,
pp. 277–300,
doi:10.1007/978-3-642-15025-8_15.
S. Graf & H. Saidi (1997):
Construction of Abstract State Graphs With PVS.
In: International Conference on Computer Aided Verification,
LNCS 1254.
Springer,
pp. 72–83,
doi:10.1007/3-540-63166-6_10.
G. W. Hamilton (2006):
Poitín: Distilling Theorems From Conjectures.
Electronic Notes in Theoretical Computer Science 151(1),
pp. 143–160,
doi:10.1016/j.entcs.2005.11.028.
G.W. Hamilton (2007):
Distillation: Extracting the Essence of Programs.
In: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation,
pp. 61–70,
doi:10.1145/1244381.1244391.
G.W. Hamilton (2007):
Distilling Programs for Verification.
Electronic Notes in Theoretical Computer Science 190(4),
pp. 17–32,
doi:10.1016/j.entcs.2007.09.005.
G.W. Hamilton & N.D. Jones (2012):
Distillation With Labelled Transition Systems.
In: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation.
ACM,
pp. 15–24,
doi:10.1145/2103746.2103753.
G. Higman (1952):
Ordering by Divisibility in Abstract Algebras.
Proceedings of the London Mathematical Society 2,
pp. 326–336,
doi:10.1112/plms/s3-2.1.326.
C.A.R. Hoare (1969):
An Axiomatic Basis for Computer Programming.
Communications of the ACM 12,
pp. 576–583,
doi:10.1145/363235.363259.
A. Ireland (2006):
Towards Automatic Assertion Refinement for Separation Logic.
In: Proceedings of the International Conference on Automated Software Engineering,
pp. 209–312,
doi:10.1109/ASE.2006.69.
A. Ireland & J. Stark (1997):
On the Automatic Discovery of Loop Invariants.
In: Fourth Nasa Langley Formal Methods Workshop,
pp. 137–152,
doi:10.1.1.16.9466.
I. Klyuchnikov (2010):
Supercompiler HOSC 1.1: Proof of Termination.
Preprint 21.
Keldysh Institute of Applied Mathematics, Moscow,
doi:10.1.1.182.2914.
J.B. Kruskal (1960):
Well-Quasi Ordering, the Tree Theorem, and Vazsonyi's Conjecture.
Transactions of the American Mathematical Society 95,
pp. 210–225,
doi:10.2307/1993287.
M. Leuschel (1998):
On the Power of Homeomorphic Embedding for Online Termination.
In: Proceedings of the International Static Analysis Symposium, Pisa, Italy,
pp. 230–245,
doi:10.1007/3-540-49727-7_14.
R. Marlet (1994):
Vers une Formalisation de l'Évaluation Partielle.
Université de Nice - Sophia Antipolis.
P. O'Hearn, J. Reynolds & Y. Hongseok (2001):
Local Reasoning About Programs That Alter Data Structures.
In: Proceedings of Computer Science Logic,
Lecture Notes in Computer Science 2142,
pp. 1–19,
doi:10.1007/3-540-44802-0_1.
J.C. Reynolds (2002):
Separation Logic: A Logic for Shared Mutable Data Structures.
In: Proceedings of the Symposium on Logic in Computer Science,
pp. 55–74,
doi:10.1109/LICS.2002.1029817.
H. Saidi & N. Shankar (1999):
Abstract and Model Check While You Prove.
In: International Conference on Computer Aided Verification,
Lecture Notes in Computer Science 1633.
Springer,
pp. 443–454,
doi:10.1007/3-540-48683-6_38.
S. Sankaranarayanan, H. Sipma & Z. Manna (2004):
Non-Linear Loop Invariant Generation Using Gr+.2222emobner Bases.
In: Proceedings of the ACM Symposium on Principles of Programming Languages,
pp. 318–329,
doi:10.1145/964001.964028.
M.H. Sørensen & R. Glück (1994):
An Algorithm of Generalization in Positive Supercompilation.
Lecture Notes in Computer Science 787,
pp. 335–351,
doi:10.1.1.49.1869.
M.H. Sørensen, R. Glück & N.D. Jones (1996):
A Positive Supercompiler.
Journal of Functional Programming 6(6),
pp. 811–838,
doi:10.1017/S0956796800002008.
N. Suzuki & K. Ishihata (1977):
Implementation of an Array Bound Checker.
In: 4th ACM Symposium on Principles of Programming Languages.
ACM Press,
pp. 132–143,
doi:10.1145/512950.512963.
Z. Xu & B. Reps, T. amd Miller (2000):
Safety Checking of Machine Code.
In: ACM SIGPLAN Conference on Programming Language Design and Implementation.
ACM Press,
pp. 70–82,
doi:10.1145/349299.349313.