Harold Abelson & Gerald J. Sussman (1996):
Structure and Interpretation of Computer Programs, Second Edition.
MIT Press.
Foto N. Afrati, Manolis Gergatsoulis & Francesca Toni (2003):
Linearisability on datalog programs.
Theor. Comput. Sci. 308(1-3),
pp. 199–226,
doi:10.1016/S0304-3975(02)00730-2.
H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison & M. Tommasi (2007):
Tree Automata Techniques and Applications.
Available on: http://www.grappa.univ-lille3.fr/tata.
Release October, 12th 2007.
Patrick Cousot & Radhia Cousot (1977):
Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints.
In: Robert M. Graham, Michael A. Harrison & Ravi Sethi: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977.
ACM,
pp. 238–252,
doi:10.1145/512950.512973.
Available at http://dl.acm.org/citation.cfm?id=512950.
Patrick Cousot & Nicolas Halbwachs (1978):
Automatic Discovery of Linear Restraints Among Variables of a Program.
In: Alfred V. Aho, Stephen N. Zilles & Thomas G. Szymanski: Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978.
ACM Press,
pp. 84–96,
doi:10.1145/512760.512770.
Available at http://dl.acm.org/citation.cfm?id=512760.
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi & Maurizio Proietti (2014):
VeriMAP: A Tool for Verifying Programs through Transformations.
In: Erika Ábrahám & Klaus Havelund: Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings,
Lecture Notes in Computer Science 8413.
Springer,
pp. 568–574,
doi:10.1007/978-3-642-54862-8_47.
Javier Esparza, Stefan Kiefer & Michael Luttenberger (2007):
On Fixed Point Equations over Commutative Semirings.
In: STACS 2007, 24th Annual Symposium on Theoretical Aspects of Computer Science, Proceedings,
LNCS 4393.
Springer,
pp. 296–307,
doi:10.1007/978-3-540-70918-3_26.
Javier Esparza, Michael Luttenberger & Maximilian Schlund (2014):
A Brief History of Strahler Numbers.
In: LATA+.2222em'14, 8th Int. Conf. on Language and Automata Theory and Applications,
LNCS 8370.
Springer,
pp. 1–13,
doi:10.1007/978-3-319-04921-2_1.
J. P. Gallagher & L. Lafave (1996):
Regular Approximation of Computation Paths in Logic and Functional Languages.
In: Partial Evaluation,
LNCS 1110.
Springer,
pp. 115–136,
doi:10.1007/3-540-61580-6_7.
John P. Gallagher, Mai Ajspur & Bishoksan Kafle (2014):
An Optimised Algorithm for Determinisation and Completion of Finite Tree Automata.
Technical Report 145.
Roskilde University, Denmark.
Available from http://arxiv.org/pdf/1511.03595v1.pdf.
Pierre Ganty, Radu Iosif & Filip Konečný (2013):
Underapproximation of Procedure Summaries for Integer Programs.
In: TACAS+.2222em'13: Proc. 19th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems,
LNCS 7795.
Springer,
pp. 247–261,
doi:10.1007/978-3-642-36742-7_18.
Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea & Andrey Rybalchenko (2012):
HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution).
In: Cormac Flanagan & Barbara König: TACAS,
LNCS 7214.
Springer,
pp. 549–551,
doi:10.1007/978-3-642-28756-5_46.
Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea & Andrey Rybalchenko (2012):
Synthesizing software verifiers from proof rules.
In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12, Beijing, China - June 11 - 16, 2012.
ACM,
pp. 405–416,
doi:10.1145/2254064.2254112.
Jozef Gruska (1971):
A Few Remarks on the Index of Context-Free Grammars and Languages.
Information and Control 19(3),
pp. 216–223,
doi:10.1016/S0019-9958(71)90095-7.
Matthias Heizmann, Jochen Hoenicke & Andreas Podelski (2009):
Refinement of Trace Abstraction..
In: Static Analysis, 16th International Symposium, SAS 2009,
LNCS 5673.
Springer,
pp. 69–85,
doi:10.1007/978-3-642-03237-0_7.
Matthias Heizmann, Jochen Hoenicke & Andreas Podelski (2013):
Software Model Checking for People Who Love Automata.
In: Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings,
LNCS 8044.
Springer,
pp. 36–52,
doi:10.1007/978-3-642-39799-8_2.
Krystof Hoder & Nikolaj Bjørner (2012):
Generalized Property Directed Reachability.
In: Alessandro Cimatti & Roberto Sebastiani: Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings,
Lecture Notes in Computer Science 7317.
Springer,
pp. 157–171,
doi:10.1007/978-3-642-31612-8_13.
Bishoksan Kafle & John P. Gallagher (2015):
Constraint Specialisation in Horn Clause Verification.
In: Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM, Mumbai, India, January 15-17, 2015.
ACM,
pp. 85–90,
doi:10.1145/2678015.2682544.
Bishoksan Kafle & John P. Gallagher (2015):
Tree Automata-Based Refinement with Application to Horn Clause Verification.
In: Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings,
LNCS 8931.
Springer,
pp. 209–226,
doi:10.1007/978-3-662-46081-8_12.
Michael Luttenberger (2011):
An Extension of Parikh's Theorem beyond Idempotence.
CoRR abs/1112.2864.
Available at http://arxiv.org/abs/1112.2864.
Alberto Pettorossi & Maurizio Proietti (1999):
Synthesis and Transformation of Logic Programs Using Unfold/Fold Proofs..
J. Log. Program. 41(2-3),
pp. 197–230,
doi:10.1016/S0743-1066(99)00029-1.
Robert F. Stärk (1989):
A Direct Proof for the Completeness of SLD-Resolution.
In: Egon Börger, Hans Kleine Büning & Michael M. Richter: CSL '89, 3rd Workshop on Computer Science Logic, Kaiserslautern, Germany, October 2-6, 1989, Proceedings,
Lecture Notes in Computer Science 440.
Springer,
pp. 382–383,
doi:10.1007/3-540-52753-2_52.