Verification by abstract interpretation, Soundness and abstract induction

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Automatic program verification tools have to cope with programming language and machine semantics, undecidability, and mathematical induction, and so are all complex and imperfect. The ins and outs of automatic program verification will be discussed in light of the theory and practice of abstract interpretation [1–3].

Original languageEnglish (US)
Title of host publicationLogic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Revised Selected Papers
PublisherSpringer Verlag
Volume9527
ISBN (Print)9783319274355
StatePublished - 2015
Event25th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2015 - Siena, Italy
Duration: Jul 13 2015Jul 15 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9527
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other25th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2015
CountryItaly
CitySiena
Period7/13/157/15/15

Fingerprint

Automatic Verification
Program Verification
Abstract Interpretation
Soundness
Proof by induction
Mathematical Induction
Undecidability
Imperfect
Computer programming languages
Programming Languages
Semantics

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Cousot, P. (2015). Verification by abstract interpretation, Soundness and abstract induction. In Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Revised Selected Papers (Vol. 9527). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9527). Springer Verlag.

Verification by abstract interpretation, Soundness and abstract induction. / Cousot, Patrick.

Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Revised Selected Papers. Vol. 9527 Springer Verlag, 2015. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9527).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Cousot, P 2015, Verification by abstract interpretation, Soundness and abstract induction. in Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Revised Selected Papers. vol. 9527, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9527, Springer Verlag, 25th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2015, Siena, Italy, 7/13/15.
Cousot P. Verification by abstract interpretation, Soundness and abstract induction. In Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Revised Selected Papers. Vol. 9527. Springer Verlag. 2015. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Cousot, Patrick. / Verification by abstract interpretation, Soundness and abstract induction. Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Revised Selected Papers. Vol. 9527 Springer Verlag, 2015. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{664d42f672d149a296c81c5d62166729,
title = "Verification by abstract interpretation, Soundness and abstract induction",
abstract = "Automatic program verification tools have to cope with programming language and machine semantics, undecidability, and mathematical induction, and so are all complex and imperfect. The ins and outs of automatic program verification will be discussed in light of the theory and practice of abstract interpretation [1–3].",
author = "Patrick Cousot",
year = "2015",
language = "English (US)",
isbn = "9783319274355",
volume = "9527",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
booktitle = "Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Revised Selected Papers",

}

TY - GEN

T1 - Verification by abstract interpretation, Soundness and abstract induction

AU - Cousot, Patrick

PY - 2015

Y1 - 2015

N2 - Automatic program verification tools have to cope with programming language and machine semantics, undecidability, and mathematical induction, and so are all complex and imperfect. The ins and outs of automatic program verification will be discussed in light of the theory and practice of abstract interpretation [1–3].

AB - Automatic program verification tools have to cope with programming language and machine semantics, undecidability, and mathematical induction, and so are all complex and imperfect. The ins and outs of automatic program verification will be discussed in light of the theory and practice of abstract interpretation [1–3].

UR - http://www.scopus.com/inward/record.url?scp=84952837139&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84952837139&partnerID=8YFLogxK

M3 - Conference contribution

SN - 9783319274355

VL - 9527

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

BT - Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Revised Selected Papers

PB - Springer Verlag

ER -