Verification by abstract interpretation, soundness and abstract induction

Patrick Cousot

doi:10.1145/2790449.2790451

Verification by abstract interpretation, soundness and abstract induction

Patrick Cousot

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 [18, 19, 22].

Original language	English (US)
Title of host publication	Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015
Publisher	Association for Computing Machinery, Inc
Pages	1-4
Number of pages	4
ISBN (Electronic)	9781450335164
DOIs	https://doi.org/10.1145/2790449.2790451
State	Published - Jul 14 2015
Event	17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015 - Siena, Italy Duration: Jul 14 2015 → Jul 16 2015

Publication series

Name	Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015

Other

Other	17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015
Country/Territory	Italy
City	Siena
Period	7/14/15 → 7/16/15

ASJC Scopus subject areas

Computer Science Applications
Software
Computational Theory and Mathematics

Access to Document

10.1145/2790449.2790451

Cite this

Cousot, P. (2015). Verification by abstract interpretation, soundness and abstract induction. In Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015 (pp. 1-4). (Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015). Association for Computing Machinery, Inc. https://doi.org/10.1145/2790449.2790451

Verification by abstract interpretation, soundness and abstract induction. / Cousot, Patrick.
Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015. Association for Computing Machinery, Inc, 2015. p. 1-4 (Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Cousot, P 2015, Verification by abstract interpretation, soundness and abstract induction. in Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015. Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015, Association for Computing Machinery, Inc, pp. 1-4, 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015, Siena, Italy, 7/14/15. https://doi.org/10.1145/2790449.2790451

Cousot P. Verification by abstract interpretation, soundness and abstract induction. In Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015. Association for Computing Machinery, Inc. 2015. p. 1-4. (Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015). doi: 10.1145/2790449.2790451

Cousot, Patrick. / Verification by abstract interpretation, soundness and abstract induction. Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015. Association for Computing Machinery, Inc, 2015. pp. 1-4 (Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015).

@inproceedings{fd517b19c491470db05fa6fab737861d,

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 [18, 19, 22].",

author = "Patrick Cousot",

note = "Publisher Copyright: {\textcopyright} Copyright 2015 ACM.; 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015 ; Conference date: 14-07-2015 Through 16-07-2015",

year = "2015",

month = jul,

day = "14",

doi = "10.1145/2790449.2790451",

language = "English (US)",

series = "Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015",

publisher = "Association for Computing Machinery, Inc",

pages = "1--4",

booktitle = "Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015",

}

TY - GEN

T1 - Verification by abstract interpretation, soundness and abstract induction

AU - Cousot, Patrick

PY - 2015/7/14

Y1 - 2015/7/14

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 [18, 19, 22].

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 [18, 19, 22].

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

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

U2 - 10.1145/2790449.2790451

DO - 10.1145/2790449.2790451

M3 - Conference contribution

AN - SCOPUS:84959928897

T3 - Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015

SP - 1

EP - 4

BT - Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015

PB - Association for Computing Machinery, Inc

T2 - 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015

Y2 - 14 July 2015 through 16 July 2015

ER -

Verification by abstract interpretation, soundness and abstract induction

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this