ASPECT: an economical bug-detector
- 10 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
A technique-ASPECT-for catching code-level bugs is presented. ASPECT is intended to be economical for everyday software development. It comprises a formal specification language and a code-checking method. Programmers write simple assertions about the information required to compute a result; an efficient mechanical checker can then find bugs in the annotated code. Careless slips that escape type-checking and standard compiler anomaly tests can be detected, without the cost of formal verification or the uncertainty of testing. The essence of ASPECT is reasoning about dependencies between the aspects of abstract objects.<>Keywords
This publication has 7 references indexed in Scilit:
- The Inscape EnvironmentPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- Debugging Larch shared language specificationsIEEE Transactions on Software Engineering, 1990
- The program dependence graph and its use in optimizationACM Transactions on Programming Languages and Systems, 1987
- Program SlicingIEEE Transactions on Software Engineering, 1984
- An Operational Approach to Requirements Specification for Embedded SystemsIEEE Transactions on Software Engineering, 1982
- Formal specification as a design toolPublished by Association for Computing Machinery (ACM) ,1980
- Data Flow Analysis in Software ReliabilityACM Computing Surveys, 1976