Automatic verification by abstract interpretation (invited tutorial)

Patrick Cousot

doi:10.1007/3-540-36384-x_4

Automatic verification by abstract interpretation (invited tutorial)

Patrick Cousot

Computer Science

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

Abstract

We discuss the use of abstract interpretation in the context of automatic program verification requiring precise abstractions. We compare entirely manual versus user-guided abstractions ranging from program-specific abstractions including predicate abstraction to the systematic design of abstract domains and iteration strategies.

Original language	English (US)
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Editors	Lenore D. Zuck, Paul C. Attie, Agostino Cortesi, Supratik Mukhopadhyay
Publisher	Springer Verlag
Pages	20-24
Number of pages	5
ISBN (Print)	9783540003489
DOIs	https://doi.org/10.1007/3-540-36384-x_4
State	Published - 2003

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2575
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/3-540-36384-x_4

Cite this

Cousot, P. (2003). Automatic verification by abstract interpretation (invited tutorial). In L. D. Zuck, P. C. Attie, A. Cortesi, & S. Mukhopadhyay (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 20-24). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2575). Springer Verlag. https://doi.org/10.1007/3-540-36384-x_4

Automatic verification by abstract interpretation (invited tutorial). / Cousot, Patrick.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ed. / Lenore D. Zuck; Paul C. Attie; Agostino Cortesi; Supratik Mukhopadhyay. Springer Verlag, 2003. p. 20-24 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2575).

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

Cousot, P 2003, Automatic verification by abstract interpretation (invited tutorial). in LD Zuck, PC Attie, A Cortesi & S Mukhopadhyay (eds), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2575, Springer Verlag, pp. 20-24. https://doi.org/10.1007/3-540-36384-x_4

Cousot P. Automatic verification by abstract interpretation (invited tutorial). In Zuck LD, Attie PC, Cortesi A, Mukhopadhyay S, editors, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag. 2003. p. 20-24. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-36384-x_4

Cousot, Patrick. / Automatic verification by abstract interpretation (invited tutorial). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). editor / Lenore D. Zuck ; Paul C. Attie ; Agostino Cortesi ; Supratik Mukhopadhyay. Springer Verlag, 2003. pp. 20-24 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{a5fb066f6e47443394ba2fd5e0d7264d,

title = "Automatic verification by abstract interpretation (invited tutorial)",

abstract = "We discuss the use of abstract interpretation in the context of automatic program verification requiring precise abstractions. We compare entirely manual versus user-guided abstractions ranging from program-specific abstractions including predicate abstraction to the systematic design of abstract domains and iteration strategies.",

author = "Patrick Cousot",

year = "2003",

doi = "10.1007/3-540-36384-x_4",

language = "English (US)",

isbn = "9783540003489",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "20--24",

editor = "Zuck, {Lenore D.} and Attie, {Paul C.} and Agostino Cortesi and Supratik Mukhopadhyay",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - CHAP

T1 - Automatic verification by abstract interpretation (invited tutorial)

AU - Cousot, Patrick

PY - 2003

Y1 - 2003

N2 - We discuss the use of abstract interpretation in the context of automatic program verification requiring precise abstractions. We compare entirely manual versus user-guided abstractions ranging from program-specific abstractions including predicate abstraction to the systematic design of abstract domains and iteration strategies.

AB - We discuss the use of abstract interpretation in the context of automatic program verification requiring precise abstractions. We compare entirely manual versus user-guided abstractions ranging from program-specific abstractions including predicate abstraction to the systematic design of abstract domains and iteration strategies.

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

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

U2 - 10.1007/3-540-36384-x_4

DO - 10.1007/3-540-36384-x_4

M3 - Chapter

AN - SCOPUS:24344471846

SN - 9783540003489

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

SP - 20

EP - 24

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

A2 - Zuck, Lenore D.

A2 - Attie, Paul C.

A2 - Cortesi, Agostino

A2 - Mukhopadhyay, Supratik

PB - Springer Verlag

ER -

Automatic verification by abstract interpretation (invited tutorial)

Abstract

Publication series

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this