Citation
Glenn Ammons, David Mandelin, Rastislav Bodik, James Larus. "Debugging Temporal Specifications with Concept Analysis". Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June, 2003.

Abstract
Program verification tools (such as model checkers and static analyzers) can find many errors in programs. These tools need formal specifications of correct program behavior, but writing a correct specification is difficult, just as writing a correct program is difficult. Thus, just as we need methods for debugging programs, we need methods for debugging specifications. This paper describes a novel method for debugging formal, temporal specifications. Our method exploits the short program execution traces that program verification tools generate from specification violations and that specification miners extract from programs. Manually examining these traces is a straightforward way to debug a specification, but this method is tedious and error-prone because there may be hundreds or thousands of traces to inspect. Our method uses concept analysis to automatically group the traces into highly similar clusters. By examining clusters instead of individual traces, a person can debug a specification with less work. To test our method, we implemented a tool, Cable, for debugging specifications. We have used Cable to debug specifications produced by Strauss, our specification miner. We found that using Cable to debug these specifications requires, on average, less than one third as many user decisions as debugging by examining all traces requires. In one case, using Cable required only 28 decisions, while debugging by examining all traces required 224.

Electronic downloads

• http://dx.doi.org/10.1145/781131.781152

• HTML

  Glenn Ammons, David Mandelin, Rastislav Bodik, James Larus.
  <a
  href="http://chess.eecs.berkeley.edu/pubs/756.html"
  >Debugging Temporal Specifications with Concept
  Analysis</a>, Proceedings of the ACM SIGPLAN 2003
  conference on Programming language design and
  implementation, June, 2003.

• Plain text

  Glenn Ammons, David Mandelin, Rastislav Bodik, James Larus.
  "Debugging Temporal Specifications with Concept
  Analysis". Proceedings of the ACM SIGPLAN 2003
  conference on Programming language design and
  implementation, June, 2003.

• BibTeX

  @inproceedings{AmmonsMandelinBodikLarus03_DebuggingTemporalSpecificationsWithConceptAnalysis,
      author = {Glenn Ammons and David Mandelin and Rastislav
                Bodik and James Larus},
      title = {Debugging Temporal Specifications with Concept
                Analysis},
      booktitle = {Proceedings of the ACM SIGPLAN 2003 conference on
                Programming language design and implementation},
      month = {June},
      year = {2003},
      abstract = {Program verification tools (such as model checkers
                and static analyzers) can find many errors in
                programs. These tools need formal specifications
                of correct program behavior, but writing a correct
                specification is difficult, just as writing a
                correct program is difficult. Thus, just as we
                need methods for debugging programs, we need
                methods for debugging specifications. This paper
                describes a novel method for debugging formal,
                temporal specifications. Our method exploits the
                short program execution traces that program
                verification tools generate from specification
                violations and that specification miners extract
                from programs. Manually examining these traces is
                a straightforward way to debug a specification,
                but this method is tedious and error-prone because
                there may be hundreds or thousands of traces to
                inspect. Our method uses concept analysis to
                automatically group the traces into highly similar
                clusters. By examining clusters instead of
                individual traces, a person can debug a
                specification with less work. To test our method,
                we implemented a tool, Cable, for debugging
                specifications. We have used Cable to debug
                specifications produced by Strauss, our
                specification miner. We found that using Cable to
                debug these specifications requires, on average,
                less than one third as many user decisions as
                debugging by examining all traces requires. In one
                case, using Cable required only 28 decisions,
                while debugging by examining all traces required
                224.},
      URL = {http://chess.eecs.berkeley.edu/pubs/756.html}
  }
  

Posted by Christopher Brooks on 4 Nov 2010.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.