The ASTREE analyzer

被引：0

作者：

Cousot, P ^{[1
]}

Cousot, R

Feret, J

Mauborgne, L

Miné, A

Monniaux, D

Rival, X

机构：

[1] CNRS, Paris, France

[2] Ecole Normale Super, F-75231 Paris, France

[3] Ecole Polytech, Palaiseau, France

来源：

PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS | 2005年 / 3444卷

关键词：

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

ASTREE is an abstract interpretation-based static program analyzer aiming at proving automatically the absence of run time errors in programs written in the C programming language. It has been applied with success to large embedded control-command safety critical real-time software generated automatically from synchronous specifications, producing a correctness proof for complex software without any false alarm in a few hours of computation.

引用

页码：21 / 30

页数：10

共 17 条

[1] AAMODT T, 1999, 1 WORKSH MED PROC DS, P3
[2] ALT M, 1996, LNCS, V1145, P52
[3] [Anonymous], 2004, THESIS ECOLE POLYTEC
[4] Blanchet B, 2002, LECT NOTES COMPUT SC, V2566, P85
[5] Blanchet Bruno, 2003, P ACM SIGPLAN 2003 C, P196, DOI [DOI 10.1145/780822.781153, 10.1145/781131.781153, DOI 10.1145/781131.781153]
[6] A tool for checking ANSI-C programs
Clarke, E
Kroening, D
Lerda, F
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2004, 2988 : 168 - 176
[7] Cousot P., 1992, Journal of Logic and Computation, V2, P511, DOI 10.1093/logcom/2.4.511
[8] Cousot P, 1977, POPL, P238, DOI DOI 10.1145/512950.512973
[9] Cousot Patrick, 1979, POPL, P269, DOI DOI 10.1145/567752.567778
[10] Feret J, 2004, LECT NOTES COMPUT SC, V2986, P33

← 1 2 →