E. Albert, M. Gómez-Zamalloa, L. Hubert & G. Puebla (2007):
Verification of Java Bytecode Using Analysis and Transformation of Logic Programs.
In: M. Hanus: Practical Aspects of Declarative Languages,
Lecture Notes in Computer Science 4354.
Springer,
pp. 124–139,
doi:10.1007/978-3-540-69611-7_8.
E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2014):
Program Verification via Iterated Specialization.
Science of Computer Programming 95, Part 2,
pp. 149–175,
doi:10.1016/j.scico.2014.05.017.
E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2014):
VeriMAP: A Tool for Verifying Programs through Transformations.
In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS '14,
Lecture Notes in Computer Science 8413.
Springer,
pp. 568–574,
doi:10.1007/978-3-642-54862-8_47.
Available at: http://www.map.uniroma2.it/VeriMAP.
E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2015):
Semantics-based generation of verification conditions by program specialization.
In: Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, Siena, Italy, July 14-16, 2015.
ACM,
pp. 91–102,
doi:10.1145/2790449.2790529.
S. Etalle & M. Gabbrielli (1996):
Transformations of CLP Modules.
Theoretical Computer Science 166,
pp. 101–146,
doi:10.1016/0304-3975(95)00148-4.
J. P. Gallagher & B. Kafle (2014):
Analysis and Transformation Tools for Constrained Horn Clause Verification.
Theory and Practice of Logic Programming 14(4-5),
pp. 90–101.
Supplementary Materials.
A. Gurfinkel, T. Kahsai, A. Komuravelli & J.A. Navas (2015):
The SeaHorn Verification Framework.
In: Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015.
Springer,
pp. 343–361,
doi:10.1007/978-3-319-21690-4_20.
K. S. Henriksen & J. P. Gallagher (2006):
Abstract Interpretation of PIC Programs through Logic Programming.
In: Proceedings of the 6th IEEE International Workshop on Source Code Analysis and Manipulation, SCAM '06,
pp. 103–179,
doi:10.1109/SCAM.2006.1.
M. Leuschel & M. H. Sørensen (1996):
Redundant Argument Filtering of Logic Programs.
In: J. Gallagher: Logic Program Synthesis and Transformation, Proceedings LOPSTR '96, Stockholm, Sweden,
Lecture Notes in Computer Science 1207.
Springer-Verlag,
pp. 83–103,
doi:10.1007/3-540-62718-9_6.
L. M. de Moura & N. Bjørner (2008):
Z3: An Efficient SMT Solver.
In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS '08,
Lecture Notes in Computer Science 4963.
Springer,
pp. 337–340,
doi:10.1007/978-3-540-78800-3_24.
J. C. Peralta, J. P. Gallagher & H. Saglam (1998):
Analysis of Imperative Programs through Analysis of Constraint Logic Programs.
In: G. Levi: Proceedings of the 5th International Symposium on Static Analysis, SAS '98,
Lecture Notes in Computer Science 1503.
Springer,
pp. 246–261,
doi:10.1007/3-540-49727-7_15.
M. Proietti & A. Pettorossi (1995):
Unfolding-Definition-Folding, in this Order, for Avoiding Unnecessary Variables in Logic Programs.
Theoretical Computer Science 142(1),
pp. 89–124,
doi:10.1016/0304-3975(94)00227-A.