Hostname: page-component-7b7567c8c-tnzcf Total loading time: 0 Render date: 2026-11-12T19:36:47.382Z Has data issue: false hasContentIssue false
  • English
  • Français

Introduction to the special issue on computational logic for verification

Published online by Cambridge University Press:  11 May 2018

GERMÁN VIDALOpen the ORCID record for GERMÁN VIDAL[Opens in a new window]
GERMÁN VIDAL*
Affiliation:
MiST, DSIC, Universitat Politècnica de València, Camino de Vera, S/N, 46022 Valencia, Spain (e-mail: gvidal@dsic.upv.es)
Rights & Permissions [Opens in a new window]

Extract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

Logic underlies many fundamental techniques in computer science. It helps us to rigorously formalize these techniques and prove them correct. The last decade has witnessed a growing interest in the use of computational logic methods for program verification. It has attracted researchers from both computational logic and program verification communities, giving rise to a fruitful exchange of ideas and experiences.

Information

Type
Introduction
Information
Theory and Practice of Logic Programming , Volume 18 , Special Issue 2: Computational Logic for Verification , March 2018, pp. 122 - 125
Copyright
Copyright © Cambridge University Press 2018 

References

Bjørner, N., Gurfinkel, A., McMillan, K. L. and Rybalchenko, A. 2015. Horn clause solvers for program verification. In Fields of Logic and Computation II – Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, Beklemishev, L. D., Blass, A., Dershowitz, N., Finkbeiner, B. and Schulte, W., Eds. Lecture Notes in Computer Science, vol. 9300. Springer, Springer International Publishing Switzerland, 24–51.CrossRefGoogle Scholar
Boyland, J., Noble, J. and Retert, W. 2001. Capabilities for sharing: A generalisation of uniqueness and read-only. In Proc. of 15th European Conference on Object-Oriented Programming (ECOOP 2001), Knudsen, J. L., Ed. Lecture Notes in Computer Science, vol. 2072. Springer, Verlag Berlin Heidelberg, 2–27.Google Scholar
De Angelis, E., Fioravanti, F., Pettorossi, A. and Proietti, M. 2014. VeriMAP: A tool for verifying programs through transformations. In Proc. of 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014), E., Ábrahám and Havelund, K., Eds. Lecture Notes in Computer Science, vol. 8413. Springer, 568–574.Google Scholar
de Moura, L. M. and Bjørner, N. 2008. Z3: an efficient SMT solver. In Proc. of 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), Ramakrishnan, C. R. and Rehof, J., Eds. Lecture Notes in Computer Science, vol. 4963. Springer, Verlag Berlin Heidelberg, 337–340.Google Scholar
Esparza, J., Kiefer, S. and Luttenberger, M. 2010. Newtonian program analysis. Journal of the ACM 57, 6, 33:1–33:47.CrossRefGoogle Scholar
Esparza, J., Luttenberger, M. and Schlund, M. 2014. A brief history of Strahler numbers. In Proc. of 8th International Conference Language and Automata Theory and Applications (LATA 2014), A., Dediu, Martín-Vide, C., Sierra-Rodríguez, J. L., and Truthe, B., Eds. Lecture Notes in Computer Science, vol. 8370. Springer, International Publishing Switzerland, 1–13.Google Scholar
Fages, F., Ruet, P. and Soliman, S. 2001. Linear concurrent constraint programming: Operational and phase semantics. Information and Computation 165, 1, 14–41.CrossRefGoogle Scholar
Gallagher, J. P. and Kafle, B. 2014. Analysis and transformation tools for constrained Horn clause verification. In Proc. of 30th International Conference on Logic Programming (Technical Communications), ICLP 2014. Available from http://arxiv.org/abs/1405.3883Google Scholar
Gange, G., Navas, J. A., Schachte, P., Søndergaard, H. and Stuckey, P. J. 2015. Horn clauses as an intermediate representation for program analysis and transformation. Theory and Practice of Logic Programming 15, 4–5, 526–542.CrossRefGoogle Scholar
Jaffar, J. and Maher, M. J. 1994. Constraint logic programming: A survey. Journal of Logic Programming 19/20, 503–581.CrossRefGoogle Scholar
Méndez-Lojo, M., Navas, J. A. and Hermenegildo, M. V. 2008. A flexible, (C)LP-based approach to the analysis of object-oriented programs. In Proc. of 17th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2007). Revised Selected Papers, A., King, Ed. Lecture Notes in Computer Science, vol. 4915. Springer, Verlag Berlin Heidelberg, 154–168.Google Scholar
Pettorossi, A. and Proietti, M. 1994. Transformation of logic programs: Foundations and techniques. Journal of Logic Programming 19/20, 261–320.CrossRefGoogle Scholar
Reps, T. W., Turetsky, E. and Prabhu, P. 2016. Newtonian program analysis via tensor product. In Proc. of 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), R., Bodík and Majumdar, R., Eds. ACM, New York, NY, USA, 663–677.Google Scholar
Saraswat, V. A. 1993. Concurrent Constraint Programming. ACM Doctoral dissertation awards. MIT Press, Cambridge, MA, USA.CrossRefGoogle Scholar
Shapiro, E. Y. 1989. The family of concurrent logic programming languages. ACM Computing Surveys 21, 3, 413–510.CrossRefGoogle Scholar
Tamaki, H. and Sato, T. 1984. Unfold/fold transformation of logic programs. In Proc. of 2nd International Logic Programming Conference (ICLP'84), S., Tärnlund, Ed. Uppsala University, Uppsala, Sweden, 127–138.Google Scholar
Watt, D. 2009. Programming XC on XMOS Devices. XMOS Limited. Antony Row, Chippenham, UK.Google Scholar