Formal Software Analysis Emerging Trends in Software Model Checking
- 1 May 2007
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 1165, 120-136
- https://doi.org/10.1109/fose.2007.6
Abstract
The study of methodologies and techniques to produce correct software has been active for four decades. During this period, researchers have developed and investigated a wide variety of approaches, but techniques based on mathematical modeling of program behavior have been a particular focus since they offer the promise of both finding errors and assuring important program properties. The past fifteen years have seen a marked and accelerating shift towards algorithmic formal reasoning about program behavior - we refer to these as formal software analysis. In this paper, we define formal software analyses as having several important properties that distinguish them from other forms of software analysis. We describe three foundational formal software analyses, but focus on the adaptation of model checking to reason about software. We review emerging trends in software model checking and identify future directions that promise to significantly improve its cost-effectiveness.Keywords
This publication has 36 references indexed in Scilit:
- Compositional dynamic test generationPublished by Association for Computing Machinery (ACM) ,2007
- SYNERGYPublished by Association for Computing Machinery (ACM) ,2006
- Testing, abstraction, theorem proving: better together!Published by Association for Computing Machinery (ACM) ,2006
- DARTPublished by Association for Computing Machinery (ACM) ,2005
- Heuristics for model checking Java programsInternational Journal on Software Tools for Technology Transfer, 2004
- A type and effect system for atomicityPublished by Association for Computing Machinery (ACM) ,2003
- Verifying safety properties of concurrent Java programs using 3-valued logicPublished by Association for Computing Machinery (ACM) ,2001
- Partial-Order Methods for the Verification of Concurrent SystemsPublished by Springer Nature ,1996
- A formal analysis of the fault-detecting ability of testing methodsIEEE Transactions on Software Engineering, 1993
- Assigning meanings to programsPublished by American Mathematical Society (AMS) ,1967