
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Nels E. Beckman, Aditya V. Nori, Sriram K. Rajamani, Robert J. Simmons, Sai Deep Tetali, Aditya V. Thakur, "Proofs from Tests," IEEE Transactions on Software Engineering, vol. 36, no. 4, pp. 495508, July/August, 2010.  
BibTex  x  
@article{ 10.1109/TSE.2010.49, author = {Nels E. Beckman and Aditya V. Nori and Sriram K. Rajamani and Robert J. Simmons and Sai Deep Tetali and Aditya V. Thakur}, title = {Proofs from Tests}, journal ={IEEE Transactions on Software Engineering}, volume = {36}, number = {4}, issn = {00985589}, year = {2010}, pages = {495508}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2010.49}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Proofs from Tests IS  4 SN  00985589 SP495 EP508 EPD  495508 A1  Nels E. Beckman, A1  Aditya V. Nori, A1  Sriram K. Rajamani, A1  Robert J. Simmons, A1  Sai Deep Tetali, A1  Aditya V. Thakur, PY  2010 KW  Software model checking KW  directed testing KW  abstraction refinement. VL  36 JA  IEEE Transactions on Software Engineering ER   
[1] E.W. Dijkstra, "The Humble Programmer," Comm. ACM, vol. 15, no. 10, pp. 859866, 1972.
[2] P. Godefroid, N. Klarlund, and K. Sen, "Dart: Directed Automated Random Testing," Proc. Programming Language Design and Implementation, pp. 213223, 2005.
[3] C. Cadar, V. Ganesh, P.M. Pawlowski, D.L. Dill, and D.R. Engler, "EXE: Automatically Generating Inputs of Death," Proc. ACM Conf. Computer and Comm. Security, 2006.
[4] K. Sen, D. Marinov, and G. Agha, "Cute: A Concolic Unit Testing Engine for C," Proc. Foundations of Software Eng., pp. 263272, 2005.
[5] B.S. Gulavani, T.A. Henzinger, Y. Kannan, A.V. Nori, and S.K. Rajamani, "Synergy: A New Algorithm for Property Checking," Proc. Foundations of Software Eng., pp. 117127, 2006.
[6] T. Ball, R. Majumdar, T. Millstein, and S.K. Rajamani, "Automatic Predicate Abstraction of C Programs," Proc. Programming Language Design and Implementation, pp. 203213, 2001.
[7] T.A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, "Lazy Abstraction," Proc. Principles of Programming Languages, pp. 5870, 2002.
[8] E.W. Dijkstra, A Discipline of Programming. Prentice Hall, 1997.
[9] T. Ball and S.K. Rajamani, "Automatically Validating Temporal Safety Properties of Interfaces," Proc. SPIN Workshop Model Checking of Software, pp. 103122, 2001.
[10] T.A. Henzinger, R. Jhala, R. Majumdar, and K.L. McMillan, "Abstractions from Proofs," Proc. Principles of Programming Languages, pp. 232244, 2004.
[11] N.E. Beckman, A.V. Nori, S.K. Rajamani, and R.J. Simmons, "Proofs from Tests," Proc. Int'l Symp. Software Testing and Analysis, pp. 103122, 2008.
[12] P. Godefroid and N. Klarlund, "Software Model Checking: Searching for Computations in the Abstract or the Concrete," Proc. Integrated Formal Methods, pp. 2032, 2005.
[13] E. Gunter and D. Peled, "Model Checking, Testing and Verification Working Together," Formal Aspects of Computing, vol. 17, no. 2, pp. 201221, 2005.
[14] G. Yorsh, T. Ball, and M. Sagiv, "Testing, Abstraction, Theorem Proving: Better Together!" Proc. Int'l Symp. Software Testing and Analysis, pp. 145156, 2006.
[15] D. Kroening, A. Groce, and E.M. Clarke, "Counterexample Guided Abstraction Refinement via Program Execution," Proc. Int'l Conf. Formal Eng. Methods, pp. 224238, 2004.
[16] P. Godefroid, "Compositional Dynamic Test Generation," Proc. Principles of Programming Languages, pp. 4754, 2007.
[17] R. Majumdar and K. Sen, "Latest: Lazy Dynamic Test Input Generation," Technical Report UCB/EECS200736, Electrical Eeng. and Computer Science Dept., Univ. of California, http://www.eecs.berkeley.edu/Pubs/TechRpts/ 2007EECS200736.html, Mar. 2007.
[18] P. Godefroid, A.V. Nori, S.K. Rajamani, and S. Tetali, "Compositional MayMust Program Analysis: Unleashing the Power of Alternation," Proc. Principles of Programming Languages, 2010.
[19] E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, "CounterexampleGuided Abstraction Refinement," Proc. Computer Aided Verification, pp. 154169, 2000.
[20] D.L. Detlefs, K.R.M. Leino, G. Nelson, and J.B. Saxe, "Extended Static Checking," Technical Report/Research Report 159, Compaq Systems Research Center, Dec. 1998.
[21] M. Barnett, B.Y.E. Chang, R. DeLine, B. Jacobs, and K.R.M. Leino, "Boogie: A Modular Reusable Verifier for ObjectOriented Programs," Proc. Formal Methods for Components and Objects, pp. 364387.
[22] K.S. Namjoshi and R.P. Kurshan, "Syntactic Program Transformations for Automatic Abstraction," Proc. Computer Aided Verification, pp. 435449, 2000.
[23] T. Ball, personal communication.
[24] T. Ball and S.K. Rajamani, "Slic: A Specification Language for Interface Checking of C," Technical Report MSRTR200121, Microsoft Research, 2001.
[25] L. de Moura and N. Bjorner, "Z3: An Efficient Smt Solver," Proc. Tools and Algorithms for the Construction and Analysis of Systems, 2008.
[26] S. Qadeer and D. Wu, "KISS: Keep it Simple and Sequential," Proc. Programming Language Design and Implementation, pp. 1424, 2004.
[27] B. Cook, A. Podelski, and A. Rybalchenko, "Termination Proofs for Systems Code," Proc. Programming Language Design and Implementation, pp. 415426, 2006.