References

  1. Alfred V. Aho, Monica S. Lam, Ravi Sethi & Jeffrey D. Ullman (2007): Compilers. Principles, Techniques, and Tools (Second Edition). Addison Wesley.
  2. Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla & Damiano Zanardini (2007): Cost Analysis of Java Bytecode. In: Rocco De Nicola: ESOP, LNCS 4421. Springer-Verlag, pp. 157–172. Available at http://dx.doi.org/10.1007/978-3-540-71316-6_12.
  3. Elvira Albert, Samir Genaim & Miguel Gómez-Zamalloa (2007): Heap space analysis for java bytecode. In: Greg Morrisett & Mooly Sagiv: ISMM. ACM, pp. 105–116. Available at http://doi.acm.org/10.1145/1296907.1296922.
  4. Elvira Albert, Miguel Gómez-Zamalloa, Laurent Hubert & Germán Puebla (2007): Verification of Java Bytecode Using Analysis and Transformation of Logic Programs. In: Michael Hanus: Proceedings PADL 2007, LNCS 4354. Springer-Verlag, pp. 124–139. Available at http://dx.doi.org/10.1007/978-3-540-69611-7_8.
  5. K. R. Apt & F. Turini (1995): Meta-logics and Logic Programming. MIT Press.
  6. Joe Armstrong (2007): A history of Erlang. In: Barbara G. Ryder & Brent Hailpern: HOPL. ACM, pp. 1–26. Available at http://doi.acm.org/10.1145/1238844.1238850.
  7. Jonathan Bowen (1999): Animating the Semantics of VERILOG using Prolog. Technical Report UNU/IIST Technical Report no. 176. United Nations University, Macau.
  8. Randy Bryant (1992): Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys 24(3), pp. 293–318, doi:10.1145/42282.46161.
  9. Mats Carlsson, Greger Ottosson & Björn Carlson (1997): An Open-Ended Finite Domain Constraint Solver. In: Hugh Glaser Glaser, Pieter H. Hartel & Herbert Kuchen: Proceedings PLILP'97, LNCS 1292. Springer-Verlag, pp. 191–206. Available at https://doi.org/10.1007/BFb0033845.
  10. W. Chen & D. S. Warren (1996): Tabled Evaluation with Delaying for General Logic Programs. Journal of the ACM 43(1), pp. 20–74, doi:10.1016/0304-3975(89)90088-1.
  11. Patrick Cousot & Radhia Cousot (1992): Abstract Interpretation and Application to Logic Programs. The Journal of Logic Programming 13(2 & 3), pp. 103–179, doi:10.1016/0743-1066(92)90030-7.
  12. Berndt Farwer & Michael Leuschel (2004): Model checking object Petri nets in Prolog. In: Proceedings PPDP '04. ACM Press, New York, NY, USA, pp. 20–31, doi:10.1145/1013963.1013970.
  13. Thom Frühwirth (2009): Constraint Handling Rules. Cambridge University Press, doi:10.1017/CBO9780511609886.
  14. Miguel Gómez-Zamalloa, Elvira Albert & Germán Puebla (2007): Improving the Decompilation of Java Bytecode to Prolog by Partial Evaluation. Electr. Notes Theor. Comput. Sci. 190(1), pp. 85–101. Available at http://dx.doi.org/10.1016/j.entcs.2007.02.062.
  15. Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea & Andrey Rybalchenko (2012): Synthesizing software verifiers from proof rules. In: Jan Vitek, Haibo Lin & Frank Tip: 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. Available at http://dl.acm.org/citation.cfm?id=2254064.
  16. Patricia Hill & John Gallagher (1998): Meta-programming in logic programming. In: D. M. Gabbay, C. J. Hogger & J. A. Robinson: Handbook of Logic in Artificial Intelligence and Logic Programming 5. Oxford Science Publications, Oxford University Press, pp. 421–497.
  17. Patricia Hill & John W. Lloyd (1994): The Gödel Programming Language. MIT Press.
  18. Pieter Hintjens (2013): ZeroMQ: Messaging for Many Applications. O'Reilly Media, Inc..
  19. Bishoksan Kafle, John P. Gallagher & Pierre Ganty (2018): Tree dimension in verification of constrained Horn clauses. Theory Pract. Log. Program. 18(2), pp. 224–251, doi:10.1017/S1471068418000030.
  20. Philipp Körner & Jens Bendisposto (2018): Distributed Model Checking Using ProB. In: Aaron Dutle, César A. Muñoz & Anthony Narkawicz: NASA Formal Methods - 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings, Lecture Notes in Computer Science 10811. Springer, pp. 244–260, doi:10.1007/978-3-319-77935-5_18.
  21. Michael Leuschel (2008): Declarative Programming for Verification: Lessons and Outlook. In: Proceedings PPDP'2008. ACM Press, pp. 1–7, doi:10.1145/1389449.1389450.
  22. Michael Leuschel & Jens Bendisposto (2010): Directed Model Checking for B: An Evaluation and New Techniques. In: Jim Davies, Leila Silva & Adenilso da Silva Simão: Formal Methods: Foundations and Applications - 13th Brazilian Symposium on Formal Methods, SBMF 2010, Natal, Brazil, November 8-11, 2010, Revised Selected Papers, Lecture Notes in Computer Science 6527. Springer, pp. 1–16, doi:10.1007/978-3-642-19829-8_1.
  23. Michael Leuschel & Michael Butler (2003): ProB: A Model Checker for B. In: Keijiro Araki, Stefania Gnesi & Dino Mandrioli: FME 2003: Formal Methods, LNCS 2805. Springer-Verlag, pp. 855–874, doi:10.1007/978-3-540-45236-2_46.
  24. Michael Leuschel & Michael J. Butler (2008): ProB: an automated analysis toolset for the B method. STTT 10(2), pp. 185–203. Available at http://dx.doi.org/10.1007/s10009-007-0063-9.
  25. Michael Leuschel & Marc Fontaine (2008): Probing the Depths of CSP-M: A new FDR-compliant Validation Tool. In: Proceedings ICFEM 2008, LNCS. Springer-Verlag, pp. 278–297, doi:10.1007/978-3-540-88194-0_18.
  26. Michael Leuschel & Helko Lehmann (2000): Coverability of Reset Petri Nets and other Well-Structured Transition Systems by Partial Deduction. In: John Lloyd: Proceedings of the International Conference on Computational Logic (CL'2000), LNAI 1861. Springer-Verlag, London, UK, pp. 101–115, doi:10.1007/3-540-44957-4_7.
  27. Michael Leuschel & Thierry Massart (2000): Infinite State Model Checking by Abstract Interpretation and Program Specialisation. In: Annalisa Bossi: Proceedings LOPSTR'99, LNCS 1817, Venice, Italy, pp. 63–82, doi:10.1007/10720327_5.
  28. Michael Leuschel, Thierry Massart & Andrew Currie (2001): How to Make FDR Spin: LTL Model Checking of CSP by Refinement. In: J. N. Oliviera & P. Zave: FME'2001, LNCS 2021. Springer-Verlag, Berlin, Germany, pp. 99–118, doi:10.1007/3-540-45251-6_6.
  29. Victor W. Marek & Miroslaw Truszczynski (1999): Stable Models and an Alternative Logic Programming Paradigm. In: Krzysztof R. Apt, Victor W. Marek, Mirek Truszczynski & David Scott Warren: The Logic Programming Paradigm - A 25-Year Perspective, Artificial Intelligence. Springer, pp. 375–398, doi:10.1007/978-3-642-60085-2_17.
  30. Robin Milner (1978): A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences 17, pp. 348–375, doi:10.1016/0022-0000(78)90014-4.
  31. Lee Naish (March 1982 (Revised July 1983)): An introduction to MU-Prolog. Technical Report 82/2. Department of Computer Science, University of Melbourne, Melbourne, Australia.
  32. Fernando C. N. Pereira & David H. D. Warren (1980): Definite Clause Grammars for Language Analysis - A Survey of the Formalism and a Comparison with Augmented Transition Networks. Artif. Intell. 13(3), pp. 231–278, doi:10.1016/0004-3702(80)90003-X.
  33. Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Terrance Swift & David S. Warren (1997): Efficient Model Checking Using Tabled Resolution. In: O. Grumberg: Proceedings CAV'97, LNCS 1254. Springer-Verlag, pp. 143–154, doi:10.1007/3-540-63166-6_16.
  34. C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Yifei Dong, Xiaoqun Du, Abhik Roychoudhury & V. N. Venkatakrishnan (2000): XMC: A Logic-Programming-Based Verification Toolset. In: Proceedings of CAV 2000, pp. 576–580, doi:10.1007/10722167_48.
  35. Sweden SICS, Kista: SICStus Prolog User's Manual. Available at http://www.sics.se/sicstus.

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