Article

Explaining Counterexamples Using Causality

Authors:

Shoham Ben-David,

Richard TreflerAuthors Info & Claims

CAV '09: Proceedings of the 21st International Conference on Computer Aided Verification

Pages 94 - 108

https://doi.org/10.1007/978-3-642-02658-4_11

Published: 23 June 2009 Publication History

Abstract

When a model does not satisfy a given specification, a counterexample is produced by the model checker to demonstrate the failure. A user must then examine the counterexample trace, in order to visually identify the failure that it demonstrates. If the trace is long, or the specification is complex, finding the failure in the trace becomes a non-trivial task. In this paper, we address the problem of analyzing a counterexample trace and highlighting the failure that it demonstrates. Using the notion of <em>causality</em>, introduced by Halpern and Pearl, we formally define a set of causes for the failure of the specification on the given counterexample trace. These causes are marked as red dots and presented to the user as a visual explanation of the failure. We study the complexity of computing the exact set of causes, and provide a polynomial-time algorithm that approximates it. This algorithm is implemented as a feature in the IBM formal verification platform RuleBase PE, where these visual explanations are an integral part of every counterexample trace. Our approach is independent of the tool that produced the counterexample, and can be applied as a light-weight external layer to any model checking tool, or used to explain simulation traces.

References

[1]

Prosyd: Property-Based System Design (2005), http://www.prosyd.org/

[2]

Armoni, R., Bustan, D., Kupferman, O., Vardi, M.Y.: Resets vs. aborts in linear temporal logic. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 65-80. Springer, Heidelberg (2003).

[3]

Ball, T., Naik, M., Rajamani, S.: From symptom to cause: Localizing errors in counterexample traces. In: Proc. of POPL, pp. 97-105 (2003).

[4]

Beer, I., Ben-David, S., Chockler, H., Orni, A., Trefler, R.: Explaining Counterexamples Using Causality. IBM technical report number H-0266, http://domino.watson.ibm.com/library/cyberdig.nsf/Home

[5]

Ben-David, S., Eisner, C., Geist, D., Wolfsthal, Y.: Model checking at IBM. FMSD 22(2), 101-108 (2003).

[6]

Chechik, M., Gurfinkel, A.: A framework for counterexample generation and exploration. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 217-233. Springer, Heidelberg (2005).

[7]

Chockler, H., Grumberg, O., Yadgar, A.: Efficient automatic STE refinement using responsibility. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 233-248. Springer, Heidelberg (2008).

[8]

Chockler, H., Halpern, J.Y., Kupferman, O.:What causes a system to satisfy a specification? ACM TOCL 9(3) (2008).

[9]

Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52-71. Springer, Heidelberg (1981).

[10]

Clarke, E., Grumberg, O., McMillan, K., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proc. 32nd DAC, pp. 427-432 (1995).

[11]

Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999).

[12]

Copty, F., Irron, A., Weissberg, O., Kropp, N., Kamhi, G.: Efficient debugging in a formal verification environment. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 275-292. Springer, Heidelberg (2001).

[13]

Dershowitz, N., Hanna, Z.,Nadel, A.: A scalable algorithm for minimal unsatisfiable core extraction. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 36-41. Springer, Heidelberg (2006).

[14]

Dong, Y., Ramakrishnan, C.R., Smolka, S.A.: Model checking and evidence exploration. In: Proc. of ECBS, pp. 214-223 (2003).

[15]

Eisner, C., Fisman, D.: A Practical Introduction to PSL. Series on Integrated Circuits and Systems (2006).

[16]

Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Campenhout, D.V.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27-39. Springer, Heidelberg (2003).

[17]

Eiter, T., Lukasiewicz, T.: Complexity results for structure-based causality. In: Proc. 7th IJCAI, pp. 35-40 (2001).

[18]

Griesmayer, A., Staber, S., Bloem, R.: Automated fault localization for c programs. ENTCS 174(4), 95-111 (2007).

[19]

Groce, A.: Error explanation with distance metrics. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 108-122. Springer, Heidelberg (2004).

[20]

Groce, A., Kroening, D.: Making the most of BMC counterexamples. In: SGSH (July 2004).

[21]

Hall, N.: Two concepts of causation. Causation and Counterfactuals. MIT Press, Cambridge (2002).

[22]

Halpern, J., Pearl, J.: Causes and explanations: Astructural-model approach--part I: Causes. In: Proc. of 17th UAI, pp. 194-202. Morgan Kaufmann Publishers, San Francisco (2001).

[23]

Hume, D.: A treatise of human nature. John Noon, London (1939).

[24]

Jin, H., Ravi, K., Somenzi, F.: Fate and free will in error traces. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 445-458. Springer, Heidelberg (2002).

[25]

Kupferman, O., Vardi, M., Wolper, P.: An automata-theoretic approach to branching-time model checking. JACM 47(2), 312-360 (2000).

[26]

Maidl, M.: The common fragment of CTL and LTL. In: Proc. of FOCS, pp. 643-652 (2000).

[27]

Queille, J., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337- 351. Springer, Heidelberg (1981).

[28]

RuleBase PE homepage, http://www.haifa.il.ibm.com/projects/verification/ RB Homepage

[29]

Shen, S., Qin, Y., Li, S.: A faster counterexample minization algorithm based on refutation analysis. In: Proc. of DATE, pp. 672-677 (2005).

[30]

Staber, S., Bloem, R.: Fault localization and correction with QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 355-368. Springer, Heidelberg (2007).

[31]

Sülflow, A., Fey, G., Bloem, R., Drechsler, R.: Using unsatisfiable cores to debug multiple design errors. In: Proc. of Symp. on VLSI, pp. 77-82 (2008).

[32]

Wang, C., Yang, Z., Ivancic, F., Gupta, A.: Whodunit? causal analysis for counterexamples. In: Graf, S., Zhang,W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 82-95. Springer, Heidelberg (2006).

Cited By

Hendriks MVerriet JBasten T(2024)Visualization, transformation, and analysis of execution traces with the eclipse TRACE4CPS trace toolInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-024-00736-326:1(101-126)Online publication date: 1-Feb-2024
https://dl.acm.org/doi/10.1007/s10009-024-00736-3
Finkbeiner BFrenkel HMetzger NSiber J(2024)Synthesis of Temporal CausalityComputer Aided Verification10.1007/978-3-031-65633-0_5(87-111)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65633-0_5
Lloyd-Roberts BJames PEdwards MRobinson SWerner T(2023)Improving Railway Safety: Human-in-the-loop Invariant FindingExtended Abstracts of the 2023 CHI Conference on Human Factors in Computing Systems10.1145/3544549.3573853(1-8)Online publication date: 19-Apr-2023
https://dl.acm.org/doi/10.1145/3544549.3573853
Show More Cited By

Index Terms

Explaining Counterexamples Using Causality
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking

Index terms have been assigned to the content through auto-classification.

Recommendations

Explaining counterexamples using causality

When a model does not satisfy a given specification, a counterexample is produced by the model checker to demonstrate the failure. A user must then examine the counterexample trace, in order to visually identify the failure that it demonstrates. If the ...
Explaining abstract counterexamples

When a program violates its specification a model checker produces a counterexample that shows an example of undesirable behavior. It is up to the user to understand the error, locate it, and fix the problem. Previous work introduced a technique for ...
Explaining abstract counterexamples
SIGSOFT '04/FSE-12: Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering

When a program violates its specification a model checker produces a counterexample that shows an example of undesirable behavior. It is up to the user to understand the error, locate it, and fix the problem. Previous work introduced a technique for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CAV '09: Proceedings of the 21st International Conference on Computer Aided Verification

June 2009

720 pages

ISBN:9783642026577

Editors:
Ahmed Bouajjani
LIAFA, University Paris Diderot (Paris 7), Case 7014, Paris Cedex 13, France 75205
,
Oded Maler
Verimag, Centre Equation, Gières, France 38610

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 23 June 2009

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

24
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 02 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Hendriks MVerriet JBasten T(2024)Visualization, transformation, and analysis of execution traces with the eclipse TRACE4CPS trace toolInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-024-00736-326:1(101-126)Online publication date: 1-Feb-2024
https://dl.acm.org/doi/10.1007/s10009-024-00736-3
Finkbeiner BFrenkel HMetzger NSiber J(2024)Synthesis of Temporal CausalityComputer Aided Verification10.1007/978-3-031-65633-0_5(87-111)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65633-0_5
Lloyd-Roberts BJames PEdwards MRobinson SWerner T(2023)Improving Railway Safety: Human-in-the-loop Invariant FindingExtended Abstracts of the 2023 CHI Conference on Human Factors in Computing Systems10.1145/3544549.3573853(1-8)Online publication date: 19-Apr-2023
https://dl.acm.org/doi/10.1145/3544549.3573853
Horak TCoenen NMetzger NHahn CFlemisch TMéndez JDimov DFinkbeiner BDachselt R(2022)Visual Analysis of Hyperproperties for Understanding Model Checking ResultsIEEE Transactions on Visualization and Computer Graphics10.1109/TVCG.2021.311486628:1(357-367)Online publication date: 1-Jan-2022
https://dl.acm.org/doi/10.1109/TVCG.2021.3114866
Coenen NDachselt RFinkbeiner BFrenkel HHahn CHorak TMetzger NSiber J(2022)Explaining Hyperproperty ViolationsComputer Aided Verification10.1007/978-3-031-13185-1_20(407-429)Online publication date: 7-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-13185-1_20
Vick CKang ETripakis S(2021)Counterexample ClassificationSoftware Engineering and Formal Methods10.1007/978-3-030-92124-8_18(312-331)Online publication date: 6-Dec-2021
https://dl.acm.org/doi/10.1007/978-3-030-92124-8_18
Baier CFunke FJantsch SPiribauer JZiemek R(2021)Probabilistic Causes in Markov ChainsAutomated Technology for Verification and Analysis10.1007/978-3-030-88885-5_14(205-221)Online publication date: 18-Oct-2021
https://dl.acm.org/doi/10.1007/978-3-030-88885-5_14
Herd BMiles S(2019)Detecting Causal Relationships in Simulation Models Using Intervention-based Counterfactual AnalysisACM Transactions on Intelligent Systems and Technology10.1145/332212310:5(1-25)Online publication date: 18-Sep-2019
https://dl.acm.org/doi/10.1145/3322123
Schuppan V(2016)Enhancing unsatisfiable cores for LTL with information on temporal relevanceTheoretical Computer Science10.1016/j.tcs.2016.01.014655:PB(155-192)Online publication date: 6-Dec-2016
https://dl.acm.org/doi/10.1016/j.tcs.2016.01.014
Malburg JFinder AFey G(2016)Debugging hardware designs using dynamic dependency graphsMicroprocessors & Microsystems10.1016/j.micpro.2016.10.00447:PB(347-359)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1016/j.micpro.2016.10.004
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents