Advertisement

Tests, Proofs and Refinements

  • Sriram K. Rajamani
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5311)

Abstract

Counter-example driven refinement using predicate abstraction has been successfully used to find bugs and verify properties in programs [1]. We describe two recent advances in counter-example driven refinement:

- We present a counter-example driven refinement technique that combines verification and testing [4]. In our approach, we simultaneously use testing and proving, with the goal of either finding a test that demonstrates that P violates ϕ, or a proof that demonstrates that all executions of P satisfy ϕ. The most interesting aspect of the approach is that unsuccessful proof attempts are used to generate tests, and unsuccessful attempts to generate tests are used to refine proofs. Besides being theoretically elegant, the approach has practical advantages –precise alias information obtained during tests can be used to greatly aid the efficiency of constructing proofs [5].

- In the past, counter-example driven refinement schemes have worked with a particular form of abstraction called predicate abstraction [1]. We present approaches to refine any abstract interpretation automatically using counterexamples. Several challenges arise: refining using disjunctions leads to powerset domains, and the use of joins forces us to consider counterexample DAGs instead of counterexample traces. We present our solutions to these problems [3,2]. We also present experiences implementing our techniques in a tool Dagger.

References

  1. 1.
    Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  2. 2.
    Gulavani, B.S., Chakroborty, S., Nori, A.V., Rajamani, S.K.: Automatically refining abstract interpretations. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 443–458. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  3. 3.
    Gulavani, B.S., Rajamani, S.K.: Counterexample driven refinement for abstract interpretation. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 474–488. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  4. 4.
    Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: SYNERGY: A new algorithm for property checking. In: FSE 2006: Foundations of Software Engineering, pp. 117–127. ACM Press, New York (2006)Google Scholar
  5. 5.
    Beckman, N.E., Nori, A.V., Rajamani, S.K., Simmons, R.J.: Proofs from tests. In: ISSTA 2008: International Symposium on Software Testing and Analysis, pp. 3–14. ACM Press, New York (2008)CrossRefGoogle Scholar
  6. 6.
    Gopinathan, M., Rajamani, S.K.: Enforcing Object Protocols by Combining Static and Dynamic Analysis. In: OOPSLA 2008: ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages and Applications. ACM Press, New York (to appear, 2008)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Sriram K. Rajamani
    • 1
  1. 1.Microsoft ResearchIndia

Personalised recommendations