References

  1. Harold Abelson & Gerald J. Sussman (1996): Structure and Interpretation of Computer Programs, Second Edition. MIT Press.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. 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.
  18. 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.
  19. 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.
  20. Michael Luttenberger (2011): An Extension of Parikh's Theorem beyond Idempotence. CoRR abs/1112.2864. Available at http://arxiv.org/abs/1112.2864.
  21. 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.
  22. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org