Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Debugging Temporal Specifications with Concept Analysis
 
Loading...
Thumbnail Image
conference paper

Debugging Temporal Specifications with Concept Analysis

Ammons, Glenn
•
Mandelin, David
•
Bodík, Rastislav
Show more
2003
2003 ACM SIGPLAN Conference on Programming Language Design and Implementation

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.

  • Details
  • Metrics
Type
conference paper
DOI
10.1145/781131.781152
Author(s)
Ammons, Glenn
•
Mandelin, David
•
Bodík, Rastislav
•
Larus, James R.
Date Issued

2003

Publisher

ACM

Published in
2003 ACM SIGPLAN Conference on Programming Language Design and Implementation
Start page

182

End page

195

Peer reviewed

REVIEWED

Written at

OTHER

EPFL units
VLSC  
Available on Infoscience
December 23, 2013
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/98781
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés