Software Model Checking: The VeriSoft Approach

被引：0

作者：

Patrice Godefroid

机构：

[1] Lucent Technologies,Bell Laboratories

来源：

Formal Methods in System Design | 2005年 / 26卷

关键词：

software model checking; systematic testing; program verification;

D O I：

暂无

中图分类号：

学科分类号：

摘要：

Verification by state-space exploration, also often referred to as model checking, is an effective method for analyzing the correctness of concurrent reactive systems (for instance, communication protocols). Unfortunately, traditional model checking is restricted to the verification of properties of models, i.e., abstractions, of concurrent systems.

引用

页码：77 / 101

页数：24

共 16 条

[1]

Bryant R.E.(1992)Symbolic boolean manipulation with ordered binary-decision diagrams ACM Computing Surveys 24 293-318

[2]

Clarke E.M.(1986)Automatic verification of finite-state concurrent systems using temporal logic specifications ACM Transactions on Programming Languages and Systems 8 244-263

[3]

Emerson E.A.(1993)The concurrency workbench: A semantics based tool for the verification of concurrent systems ACM Transactions on Programming Languages and Systems 1 36-72

[4]

Sistla A.P.(1995)State-Space Caching Revisited Formal Methods in System Design 7 1-15

[5]

Cleaveland R.(1993)Using partial orders for the efficient verification of deadlock freedom and safety properties Formal Methods in System Design 2 149-164

[6]

Parrow J.(1985)Tracing protocols AT&T Technical Journal 64 2413-2434

[7]

Steffen B.(1992)Defining conditional independence using collapses Theoretical Computer Science 101 337-359

[8]

Godefroid P.(1977)Proving the correctness of multiprocess programs IEEE Transactions on Software Engineering SE-3 125-143

[9]

Holzmann G.J.(undefined)undefined undefined undefined undefined-undefined

[10]

Pirottin D.(undefined)undefined undefined undefined undefined-undefined

← 1 2 →