Software engineering and formal methods

被引：27

作者：

Hinchey, Mike ^{[1
]}

Jackson, Michael

Cousot, Patrick ^{[2
]}

Cook, Byron ^{[3
]}

Bowen, Jonathan P.

Margaria, Tiziana ^{[4
]}

机构：

[1] Univ Limerick, Limerick, Ireland

[2] Ecole Normale Super, Paris, France

[3] Univ Cambridge, Microsofts Lab, Cambridge CB2 1TN, England

[4] Univ Potsdam, Inst Informat, Potsdam, Germany

来源：

COMMUNICATIONS OF THE ACM | 2008年 / 51卷 / 09期

关键词：

D O I：

10.1145/1378727.1378742

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：54 / 59

页数：6

共 15 条

[1]

[Anonymous], 2002, UCBCSD021175

[2] 7 MORE MYTHS OF FORMAL METHODS [J].

BOWEN, JP ;

HINCHEY, MG .

IEEE SOFTWARE, 1995, 12 (04) :34-41

[3]

BOWEN JP, 1999, FORMAL APPROACHES CO

[4]

COOK B, P 2006 ACM SIGPLAN C, P415

[5] Proving Thread Termination [J].

Cook, Byron ;

Podelski, Andreas ;

Rybalchenko, Andrey .

PLDI'07: PROCEEDINGS OF THE 2007 ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, 2007, :320-330

[6]

COUSOT P, 2007, P 1 IEEE IFIP INT S, P3

[7]

Delmas D, 2007, LECT NOTES COMPUT SC, V4634, P437

[8]

FERDINAND C, 2006, LECT NOTES COMPUTER, V4147, P1

[9]

GOTSMAN A, P 2007 ACM SIGPLAN C, P226

[10]

Gray J., 2001, P HIGH DEP COMP CONS

← 1 2 →