Formal verification by abstract interpretation

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

Abstract

We provide a rapid overview of the theoretical foundations and main applications of abstract interpretation and show that it currently provides scaling solutions to achieving assurance in mission- and safety-critical systems through verification by fully automatic, semantically sound and precise static program analysis.

Original languageEnglish (US)
Title of host publicationNASA Formal Methods - 4th International Symposium, NFM 2012, Proceedings
Pages3-7
Number of pages5
Volume7226 LNCS
DOIs
StatePublished - 2012
Event4th NASA Formal Methods Symposium, NFM 2012 - Norfolk, VA, United States
Duration: Apr 3 2012Apr 5 2012

Publication series

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

Other

Other4th NASA Formal Methods Symposium, NFM 2012
CountryUnited States
CityNorfolk, VA
Period4/3/124/5/12

Fingerprint

Safety-critical Systems
Abstract Interpretation
Program Analysis
Formal Verification
Static Analysis
Acoustic waves
Scaling
Sound
Formal verification

Keywords

  • Abstract interpretation
  • Abstraction
  • Aerospace
  • Certification
  • Cyber-physical system
  • Formal Method
  • Mission-critical system
  • Runtime error
  • Safety-critical system
  • Scalability
  • Soundness
  • Static Analysis
  • Validation
  • Verification

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Cousot, P. (2012). Formal verification by abstract interpretation. In NASA Formal Methods - 4th International Symposium, NFM 2012, Proceedings (Vol. 7226 LNCS, pp. 3-7). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7226 LNCS). https://doi.org/10.1007/978-3-642-28891-3_3

Formal verification by abstract interpretation. / Cousot, Patrick.

NASA Formal Methods - 4th International Symposium, NFM 2012, Proceedings. Vol. 7226 LNCS 2012. p. 3-7 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7226 LNCS).

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

Cousot, P 2012, Formal verification by abstract interpretation. in NASA Formal Methods - 4th International Symposium, NFM 2012, Proceedings. vol. 7226 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7226 LNCS, pp. 3-7, 4th NASA Formal Methods Symposium, NFM 2012, Norfolk, VA, United States, 4/3/12. https://doi.org/10.1007/978-3-642-28891-3_3
Cousot P. Formal verification by abstract interpretation. In NASA Formal Methods - 4th International Symposium, NFM 2012, Proceedings. Vol. 7226 LNCS. 2012. p. 3-7. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-28891-3_3
Cousot, Patrick. / Formal verification by abstract interpretation. NASA Formal Methods - 4th International Symposium, NFM 2012, Proceedings. Vol. 7226 LNCS 2012. pp. 3-7 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{f7607d1feec5466eae30c40750dc0988,
title = "Formal verification by abstract interpretation",
abstract = "We provide a rapid overview of the theoretical foundations and main applications of abstract interpretation and show that it currently provides scaling solutions to achieving assurance in mission- and safety-critical systems through verification by fully automatic, semantically sound and precise static program analysis.",
keywords = "Abstract interpretation, Abstraction, Aerospace, Certification, Cyber-physical system, Formal Method, Mission-critical system, Runtime error, Safety-critical system, Scalability, Soundness, Static Analysis, Validation, Verification",
author = "Patrick Cousot",
year = "2012",
doi = "10.1007/978-3-642-28891-3_3",
language = "English (US)",
isbn = "9783642288906",
volume = "7226 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "3--7",
booktitle = "NASA Formal Methods - 4th International Symposium, NFM 2012, Proceedings",

}

TY - GEN

T1 - Formal verification by abstract interpretation

AU - Cousot, Patrick

PY - 2012

Y1 - 2012

N2 - We provide a rapid overview of the theoretical foundations and main applications of abstract interpretation and show that it currently provides scaling solutions to achieving assurance in mission- and safety-critical systems through verification by fully automatic, semantically sound and precise static program analysis.

AB - We provide a rapid overview of the theoretical foundations and main applications of abstract interpretation and show that it currently provides scaling solutions to achieving assurance in mission- and safety-critical systems through verification by fully automatic, semantically sound and precise static program analysis.

KW - Abstract interpretation

KW - Abstraction

KW - Aerospace

KW - Certification

KW - Cyber-physical system

KW - Formal Method

KW - Mission-critical system

KW - Runtime error

KW - Safety-critical system

KW - Scalability

KW - Soundness

KW - Static Analysis

KW - Validation

KW - Verification

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

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

U2 - 10.1007/978-3-642-28891-3_3

DO - 10.1007/978-3-642-28891-3_3

M3 - Conference contribution

SN - 9783642288906

VL - 7226 LNCS

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

SP - 3

EP - 7

BT - NASA Formal Methods - 4th International Symposium, NFM 2012, Proceedings

ER -