Combining Tests and Proofs

  • Madhu Gopinathan
  • Aditya Nori
  • Sriram Rajamani
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5295)


Proof methods (or static analysis) and test methods (or dynamic analysis) have complementary strengths. While static analysis has the potential to obtain high coverage, it typically suffers from imprecision (and imprecision is needed to scale the analysis to large programs). While dynamic analysis has the potential to be very precise, it typically suffers from poor coverage.


  1. 1.
    Necula, G.C., McPeak, S., Weimer, W.: CCured: Type-safe retrofitting of legacy code. In: POPL 2002: Principles of Programming Languages, pp. 128–139. ACM Press, New York (2002)Google Scholar
  2. 2.
    Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: SYNERGY: A new algorithm for property checking. In: Robshaw, M. (ed.) FSE 2006. LNCS, vol. 4047. pp. 117–127. Springer, Heidelberg (2006)Google Scholar
  3. 3.
    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. ACM Press, New York (to appear, 2008)Google Scholar
  4. 4.
    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

  • Madhu Gopinathan
    • 1
  • Aditya Nori
    • 2
  • Sriram Rajamani
    • 2
  1. 1.Indian Institute of Science 
  2. 2.Microsoft Research India 

Personalised recommendations