On abstraction in software verification

Patrick Cousot, Radhia Cousot

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

Abstract

We show that the precision of static abstract software checking algorithms can be enhanced by taking explicitly into account the abstractions that are involved in the design of the program model/abstract semantics. This is illustrated on reachability analysis and abstract testing.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 14th International Conference, CAV 2002, Proceedings
PublisherSpringer Verlag
Pages37-56
Number of pages20
Volume2404
ISBN (Print)9783540439974
StatePublished - 2002
Event14th International Conference on Computer Aided Verification, CAV 2002 - Copenhagen, Denmark
Duration: Jul 27 2002Jul 31 2002

Publication series

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

Other

Other14th International Conference on Computer Aided Verification, CAV 2002
CountryDenmark
CityCopenhagen
Period7/27/027/31/02

Fingerprint

Software Verification
Reachability Analysis
Semantics
Testing
Software
Model
Design
Abstraction

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Cousot, P., & Cousot, R. (2002). On abstraction in software verification. In Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings (Vol. 2404, pp. 37-56). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2404). Springer Verlag.

On abstraction in software verification. / Cousot, Patrick; Cousot, Radhia.

Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings. Vol. 2404 Springer Verlag, 2002. p. 37-56 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2404).

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

Cousot, P & Cousot, R 2002, On abstraction in software verification. in Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings. vol. 2404, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2404, Springer Verlag, pp. 37-56, 14th International Conference on Computer Aided Verification, CAV 2002, Copenhagen, Denmark, 7/27/02.
Cousot P, Cousot R. On abstraction in software verification. In Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings. Vol. 2404. Springer Verlag. 2002. p. 37-56. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Cousot, Patrick ; Cousot, Radhia. / On abstraction in software verification. Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings. Vol. 2404 Springer Verlag, 2002. pp. 37-56 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{ada51056383342dfa8b78f0cca240641,
title = "On abstraction in software verification",
abstract = "We show that the precision of static abstract software checking algorithms can be enhanced by taking explicitly into account the abstractions that are involved in the design of the program model/abstract semantics. This is illustrated on reachability analysis and abstract testing.",
author = "Patrick Cousot and Radhia Cousot",
year = "2002",
language = "English (US)",
isbn = "9783540439974",
volume = "2404",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "37--56",
booktitle = "Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings",

}

TY - GEN

T1 - On abstraction in software verification

AU - Cousot, Patrick

AU - Cousot, Radhia

PY - 2002

Y1 - 2002

N2 - We show that the precision of static abstract software checking algorithms can be enhanced by taking explicitly into account the abstractions that are involved in the design of the program model/abstract semantics. This is illustrated on reachability analysis and abstract testing.

AB - We show that the precision of static abstract software checking algorithms can be enhanced by taking explicitly into account the abstractions that are involved in the design of the program model/abstract semantics. This is illustrated on reachability analysis and abstract testing.

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

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

M3 - Conference contribution

SN - 9783540439974

VL - 2404

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

SP - 37

EP - 56

BT - Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings

PB - Springer Verlag

ER -