|
 ABSTRACT
This paper describes the symbolic execution of programs. Instead of supplying the normal inputs to a program (e.g. numbers) one supplies symbols representing arbitrary values. The execution proceeds as in a normal execution except that values may be symbolic formulas over the input symbols. The difficult, yet interesting issues arise during the symbolic execution of conditional branch type statements. A particular system called EFFIGY which provides symbolic execution for program testing and debugging is also described. It interpretively executes programs written in a simple PL/I style programming language. It includes many standard debugging features, the ability to manage and to prove things about symbolic expressions, a simple program testing manager, and a program verifier. A brief discussion of the relationship between symbolic execution and program proving is also included.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
 |
1
|
|
| |
2
|
Clarke, L. A system to generate test data and symbolically execute programs. Rep. No. CU-CS-060-75, Dep. of Computer Sci., U. of Colorado, Feb. 1975.
|
| |
3
|
Darlington, J. A semantic approach to automatic program improvement. Ph.D. Th., U. of Edinburgh, 1972.
|
| |
4
|
Deutsch, L.P. An interactive program verifier. Ph.D. Th., Dep. of Computer Sci., U. of California, Berkeley, May 1973.
|
| |
5
|
|
| |
6
|
Floyd, R.W. Assigning meanings to programs, Proc. Symp. Appl. Math. Vol. 19, Amer. Math. Soc., Provincetown, R.I., 1967, pp. 19-32.
|
| |
7
|
King, J.C. Proving programs to be correct. IEEE Trans. on Comp. C-20, 11 (Nov. 1971), 1331-1336.
|
| |
8
|
King, J.C. A program verifier. Proc. IFIP Cong. 71, North- Holland, Amsterdam, 1971, pp. 235-249.
|
| |
9
|
King, J.C. and Floyd, R.W. An interpretation oriented theorem prover over integers, J. Computer Syst. Sci. 6, 4(Aug. 1972), 305-323.
|
| |
10
|
|
| |
11
|
Krause, K.W., et al. Optimal software test planning through Automated network analysis. IEEE Symp. on Computer Software Reliability, April 1973, pp. 18-22.
|
| |
12
|
|
| |
13
|
Paterson, M.S. Equivalence problems in a model of computation. Ph.D. Th., U. of Cambridge, England, Aug. 1967. Also published as A.I. Tech. Memo No. 1 (Memo No. 211), MIT, Nov. 1970.
|
| |
14
|
|
| |
15
|
Topor, R.W., and Burstall, R.M. Verification of programs by symbolic execution-progress report. Unpublished report, Dep. of Machine Intelligence, U. of Edinburgh, Scotland, Dec. 1972.
|
| |
16
|
Urschler, G. Complete redundant expression elimination in flow diagrams. Rep. RC4965, IBM Research, Yorktown Heights, N.Y., Aug. 1974.
|
CITED BY 140
|
|
|
|
|
|
|
|
P. Asirelli , P. Degano , G. Levi , A. Martèlli , U. Montanari , G. Pacini , F. Sirovich , F. Turini, A flexible environment for program development based on a symbolic interpreter, Proceedings of the 4th international conference on Software engineering, p.251-263, September 17-19, 1979, Munich, Germany
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Dick Hamlet , Bruce Gifford , Borislav Nikolik, Exploring dataflow testing of arrays, Proceedings of the 15th international conference on Software Engineering, p.118-129, May 17-21, 1993, Baltimore, Maryland, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Anne Adam , Paul Gloess , Jean-Pierre Laurent, An interactive tool for program manipulation, Proceedings of the 5th international conference on Software engineering, p.460-468, March 09-12, 1981, San Diego, California, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Jedidiah R. Crandall , Zhendong Su , S. Felix Wu , Frederic T. Chong, On deriving unknown vulnerabilities from zero-day polymorphic and metamorphic worm exploits, Proceedings of the 12th ACM conference on Computer and communications security, November 07-11, 2005, Alexandria, VA, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Sebastian Danicic , Mohammed Daoudi , Chris Fox , Mark Harman , Robert M. Hierons , John R. Howroyd , Lahcen Ourabya , Martin Ward, ConSUS: a light-weight program conditioner, Journal of Systems and Software, v.77 n.3, p.241-262, September 2005
|
|
|
Cyrille Artho , Howard Barringer , Allen Goldberg , Klaus Havelund , Sarfraz Khurshid , Mike Lowry , Corina Pasareanu , Grigore Rosu , Koushik Sen , Willem Visser , Rich Washington, Combining test case generation and runtime verification, Theoretical Computer Science, v.336 n.2-3, p.209-234, 26 May 2005
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
David Brumley , Juan Caballero , Zhenkai Liang , James Newsome , Dawn Song, Towards automatic discovery of deviations in binary implementations with applications to error detection and fingerprint generation, Proceedings of 16th USENIX Security Symposium on USENIX Security Symposium, p.1-16, August 06-10, 2007, Boston, MA
|
|
|
|
|
|
|
|
|
Phil McMinn , Mark Harman , David Binkley , Paolo Tonella, The species per path approach to SearchBased test data generation, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Christopher Kruegel , Engin Kirda , Darren Mutz , William Robertson , Giovanni Vigna, Automating mimicry attacks using static binary analysis, Proceedings of the 14th conference on USENIX Security Symposium, p.11-11, July 31-August 05, 2005, Baltimore, MD
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Corina S. Pǎsǎreanu , Peter C. Mehlitz , David H. Bushnell , Karen Gundy-Burlet , Michael Lowry , Suzette Person , Mark Pape, Combining unit-level symbolic execution and system-level concrete execution for testing nasa software, Proceedings of the 2008 international symposium on Software testing and analysis, July 20-24, 2008, Seattle, WA, USA
|
|
|
|
|
|
|
|
|
Nikolai Tillmann , Jonathan de Halleux, White-box testing of behavioral web service contracts with Pex, Proceedings of the 2008 workshop on Testing, analysis, and verification of web services and applications, p.47-48, July 21-21, 2008, Seattle, Washington
|
|
|
|
|
|
Sasa Misailovic , Aleksandar Milicevic , Nemanja Petrovic , Sarfraz Khurshid , Darko Marinov, Parallel test generation and execution with Korat, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia
|
|
|
Mark Harman , Youssef Hassoun , Kiran Lakhotia , Phil McMinn , Joachim Wegener, The impact of input domain reduction on search-based test data generation, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Bassem Elkarablieh , Ivan Garcia , Yuk Lai Suen , Sarfraz Khurshid, Assertion-based repair of complex data structures, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA
|
|
|
|
|
|
|
|
|
|
|
|
Nicolas Kicillof , Wolfgang Grieskamp , Nikolai Tillmann , Victor Braberman, Achieving both model and code coverage with automated gray-box testing, Proceedings of the 3rd international workshop on Advances in model-based testing, p.1-11, July 09-12, 2007, London, United Kingdom
|
|
|
Rui Wang , XiaoFeng Wang , Kehuan Zhang , Zhuowei Li, Towards automatic reverse engineering of software security configurations, Proceedings of the 15th ACM conference on Computer and communications security, October 27-31, 2008, Alexandria, Virginia, USA
|
|
|
|
|
|
|
|
|
Xiang Fu , Kai Qian, SAFELI: SQL injection scanner using symbolic execution, Proceedings of the 2008 workshop on Testing, analysis, and verification of web services and applications, p.34-39, July 21-21, 2008, Seattle, Washington
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Manuel Costa , Jon Crowcroft , Miguel Castro , Antony Rowstron , Lidong Zhou , Lintao Zhang , Paul Barham, Vigilante: End-to-end containment of Internet worm epidemics, ACM Transactions on Computer Systems (TOCS), v.26 n.4, p.1-68, December 2008
|
|
|
|
|
|
|
|
|
Mark Harman , Fayezin Islam , Tao Xie , Stefan Wappler, Automated test data generation for aspect-oriented programs, Proceedings of the 8th ACM international conference on Aspect-oriented software development, March 02-06, 2009, Charlottesville, Virginia, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf