Software engineering and formal methods

Mike Hinchey; Michael Jackson; Patrick Cousot; Byron Cook; Jonathan P. Bowen; Tiziana Margaria

doi:10.1145/1378727.1378742

Software engineering and formal methods

Mike Hinchey, Michael Jackson, Patrick Cousot, Byron Cook, Jonathan P. Bowen, Tiziana Margaria

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

The software engineering community has applied formal methods to improve software reliability and dependability to specify, design, analyze, and implement a hardware or software system. The challenges while developing a formal model is met by experience accumulated in each particular product class and captured in a normal design discipline. Formal verification methods also include defining of semantics and specification of a complex systems. Abstract interpretation aids in reducing the complexity inherent in proving properties and correctness of complex software systems, resulting in automating reasoning. Computer-aided formal method engineering targets knowledge understanding and solves problems heterogeneously at a meta level, where whole methods and paradigms are combined.

Original language	English (US)
Pages (from-to)	54-59
Number of pages	6
Journal	Communications of the ACM
Volume	51
Issue number	9
DOIs	https://doi.org/10.1145/1378727.1378742
State	Published - Sep 1 2008

ASJC Scopus subject areas

General Computer Science

Access to Document

10.1145/1378727.1378742

Cite this

@article{77c8ba9e98ab4a6892c349daef46c46f,

title = "Software engineering and formal methods",

abstract = "The software engineering community has applied formal methods to improve software reliability and dependability to specify, design, analyze, and implement a hardware or software system. The challenges while developing a formal model is met by experience accumulated in each particular product class and captured in a normal design discipline. Formal verification methods also include defining of semantics and specification of a complex systems. Abstract interpretation aids in reducing the complexity inherent in proving properties and correctness of complex software systems, resulting in automating reasoning. Computer-aided formal method engineering targets knowledge understanding and solves problems heterogeneously at a meta level, where whole methods and paradigms are combined.",

author = "Mike Hinchey and Michael Jackson and Patrick Cousot and Byron Cook and Bowen, {Jonathan P.} and Tiziana Margaria",

year = "2008",

month = sep,

day = "1",

doi = "10.1145/1378727.1378742",

language = "English (US)",

volume = "51",

pages = "54--59",

journal = "Communications of the ACM",

issn = "0001-0782",

publisher = "Association for Computing Machinery (ACM)",

number = "9",

}

TY - JOUR

T1 - Software engineering and formal methods

AU - Hinchey, Mike

AU - Jackson, Michael

AU - Cousot, Patrick

AU - Cook, Byron

AU - Bowen, Jonathan P.

AU - Margaria, Tiziana

PY - 2008/9/1

Y1 - 2008/9/1

N2 - The software engineering community has applied formal methods to improve software reliability and dependability to specify, design, analyze, and implement a hardware or software system. The challenges while developing a formal model is met by experience accumulated in each particular product class and captured in a normal design discipline. Formal verification methods also include defining of semantics and specification of a complex systems. Abstract interpretation aids in reducing the complexity inherent in proving properties and correctness of complex software systems, resulting in automating reasoning. Computer-aided formal method engineering targets knowledge understanding and solves problems heterogeneously at a meta level, where whole methods and paradigms are combined.

AB - The software engineering community has applied formal methods to improve software reliability and dependability to specify, design, analyze, and implement a hardware or software system. The challenges while developing a formal model is met by experience accumulated in each particular product class and captured in a normal design discipline. Formal verification methods also include defining of semantics and specification of a complex systems. Abstract interpretation aids in reducing the complexity inherent in proving properties and correctness of complex software systems, resulting in automating reasoning. Computer-aided formal method engineering targets knowledge understanding and solves problems heterogeneously at a meta level, where whole methods and paradigms are combined.

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

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

U2 - 10.1145/1378727.1378742

DO - 10.1145/1378727.1378742

M3 - Article

AN - SCOPUS:50849109201

SN - 0001-0782

VL - 51

SP - 54

EP - 59

JO - Communications of the ACM

JF - Communications of the ACM

IS - 9

ER -

Software engineering and formal methods

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this