Software engineering and formal methods

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

Research output: Contribution to journalArticle

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 languageEnglish (US)
Pages (from-to)54-59
Number of pages6
JournalCommunications of the ACM
Volume51
Issue number9
DOIs
StatePublished - Sep 1 2008

Fingerprint

Formal methods
Formal Methods
Software Engineering
Software System
Software engineering
Complex Systems
Software Reliability
Software reliability
Abstract Interpretation
Dependability
Formal Verification
Formal Model
Large scale systems
Correctness
Computer systems
Reasoning
Semantics
Paradigm
Hardware
Specification

ASJC Scopus subject areas

  • Hardware and Architecture
  • Computer Graphics and Computer-Aided Design
  • Software
  • Theoretical Computer Science
  • Computational Theory and Mathematics

Cite this

Hinchey, M., Jackson, M., Cousot, P., Cook, B., Bowen, J. P., & Margaria, T. (2008). Software engineering and formal methods. Communications of the ACM, 51(9), 54-59. https://doi.org/10.1145/1378727.1378742

Software engineering and formal methods. / Hinchey, Mike; Jackson, Michael; Cousot, Patrick; Cook, Byron; Bowen, Jonathan P.; Margaria, Tiziana.

In: Communications of the ACM, Vol. 51, No. 9, 01.09.2008, p. 54-59.

Research output: Contribution to journalArticle

Hinchey, M, Jackson, M, Cousot, P, Cook, B, Bowen, JP & Margaria, T 2008, 'Software engineering and formal methods', Communications of the ACM, vol. 51, no. 9, pp. 54-59. https://doi.org/10.1145/1378727.1378742
Hinchey M, Jackson M, Cousot P, Cook B, Bowen JP, Margaria T. Software engineering and formal methods. Communications of the ACM. 2008 Sep 1;51(9):54-59. https://doi.org/10.1145/1378727.1378742
Hinchey, Mike ; Jackson, Michael ; Cousot, Patrick ; Cook, Byron ; Bowen, Jonathan P. ; Margaria, Tiziana. / Software engineering and formal methods. In: Communications of the ACM. 2008 ; Vol. 51, No. 9. pp. 54-59.
@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 = "9",
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

VL - 51

SP - 54

EP - 59

JO - Communications of the ACM

JF - Communications of the ACM

SN - 0001-0782

IS - 9

ER -