2002 · 607 citations · 12 references
Software MaintenanceEngineeringVerificationSoftware EngineeringSource Code AnalysisSoftware AnalysisFormal VerificationData MiningDiduce SystemStatic CheckingProgram InvariantsSoftware MiningRuntime VerificationStatic AnalysisKnowledge DiscoveryComputer ScienceDebuggerStatic Program AnalysisSoftware DesignComplex Program ErrorsProgram AnalysisSoftware TestingFormal MethodsSystem SoftwareSoftware Bugs
This paper introduces DIDUCE, a tool that helps programmers detect complex program errors and pinpoint their root causes. DIDUCE instruments a program during execution, dynamically formulates and relaxes invariant hypotheses based on observed behavior to detect violations. In experiments on four sizable Java programs, DIDUCE quickly identified root causes of bugs—including a timing‑dependent flaw in JSSE—demonstrating that dynamic invariant checking is an effective debugging method.
This paper introduces DIDUCE, a practical and effective tool that aids programmers in detecting complex program errors and identifying their root causes. By instrumenting a program and observing its behavior as it runs, DIDUCE dynamically formulates hypotheses of invariants obeyed by the program. DIDUCE hypothesizes the strictest invariants at the beginning, and gradually relaxes the hypothesis as violations are detected to allow for new behavior. The violations reported help users to catch software bugs as soon as they occur. They also give programmers new visibility into the behavior of the programs such as identifying rare corner cases in the program logic or even locating hidden errors that corrupt the program's results.We implemented the DIDUCE system for Java programs and applied it to four programs of significant size and complexity. DIDUCE succeeded in identifying the root causes of programming errors in each of the programs quickly and automatically. In particular, DIDUCE is effective in isolating a timing-dependent bug in a released JSSE (Java Secure Socket Extension) library, which would have taken an experienced programmer days to find. Our experience suggests that detecting and checking program invariants dynamically is a simple and effective methodology for debugging many different kinds of program errors across a wide variety of application domains.
12
Stefan Savage, Michael T. Burrows, Greg Nelson et al. · ACM Transactions on Computer Systems · 1997 · 1.6K citations · Full text
An investigation of the Therac-25 accidents
Nancy G. Leveson, Clark Savage Turner · Computer · 1993 · 1.2K citations
Dawson Engler, David Yu Chen, Seth Hallem et al. · 2001 · 740 citations