Thanassis Avgerinos
- Allen, J.R., Kennedy, K., Porterfield, C., Warren, J. Conversion of control dependence to data dependence. In Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Austin, Texas, 1983). ACM Press, New York, NY, 177--189. Google Scholar
Digital Library
- Avgerinos, T., Rebert, A., Cha, S.K., Brumley, D. Enhancing symbolic execution with veritesting. In Proceedings of the 36th International Conference on Software Engineering, ICSE 2014 (Hyderabad, India, 2014). ACM, New York, NY, 1083--1094. DOI: 10.1145/2568225.2568293. URL http://doi.acm.org/10.1145/2568225.2568293. Google ScholarDigital Library
- Babic, D., Hu, A.J. Calysto: Scalable and precise extended static checking. In Proceedings of the 30th International Conference on Software Engineering (Leipzig, Germany, 2008). ACM, New York, NY, 211--220. Google ScholarDigital Library
- Bounimova, E., Godefroid, P., Molnar, D. Billions and billions of constraints: Whitebox Fuzz testing in production. In Proceedings of the 35th IEEE International Conference on Software Engineering (San Francisco, CA, 2013). IEEE Press, Piscataway, NJ, 122--131. Google ScholarDigital Library
- Cadar, C., Sen, K. Symbolic execution for software testing: three decades later. Commun. ACM 56, 2 (2013), 82--90. Google ScholarDigital Library
- Cadar, C., Dunbar, D., Engler, D. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Symposium on Operating System Design and Implementation (San Diego, CA, 2008). USENIX Association, Berkeley, CA, 209--224. Google ScholarDigital Library
- Cha, S.K., Avgerinos, T., Rebert, A., Brumley, D. Unleashing mayhem on binary code. In Proceedings of the 33rd IEEE Symposium on Security and Privacy (2012). IEEE Computer Society, Washington, DC, 380--394. Google ScholarDigital Library
- Chipounov, V., Kuznetsov, V., Candea, G. S2E: A platform for in vivo multi-path analysis of software systems. In Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems (Newport Beach, CA, 2011). ACM, New York, NY, 265--278. Google ScholarDigital Library
- de Moura, L., Bjørner, N. Satisfiability modulo theories: Introduction and applications. Commun. ACM 54, 9 (Sept. 2011), 69. ISSN 00010782. doi: 10.1145/1995376.1995394. URL http://dl.acm.org/citation.cfm?doid=1995376.1995394. Google ScholarDigital Library
- Flanagan, C., Saxe, J. Avoiding exponential explosion: Generating compact verification conditions. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (London, United Kingdom, 2001). ACM, New York, NY, 193--205. Google ScholarDigital Library
- Godefroid, P. Compositional dynamic test generation. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Nice, France, 2007). ACM, New York, NY, 47--54. Google ScholarDigital Library
- Godefroid, P., Levin, M.Y., Molnar, D. SAGE: Whitebox fuzzing for security testing. Commun. ACM 55, 3 (2012), 40--44. Google ScholarDigital Library
- Hansen, T., Schachte, P., Søndergaard, H. State joining and splitting for the symbolic execution of binaries. Runtime Verif. (2009), 76--92. Google ScholarDigital Library
- King, J.C. Symbolic execution and program testing. Commun. ACM 19, 7 (1976), 385--394. Google ScholarDigital Library
- Koelbl, A., Pixley, C. Constructing efficient formal models from high-level descriptions using symbolic simulation. Int. J. Parallel Program. 33, 6 (Dec. 2005), 645--666. Google ScholarDigital Library
- Kuznetsov, V., Kinder, J., Bucur, S., Candea, G. Efficient state merging in symbolic execution. In Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation (Beijing, China, 2012). ACM, New York, NY, 193--204. Google ScholarDigital Library
- Lattner, C., Adve, V. LLVM: A compilation framework for lifelong program analysis & transformation. In Proceedings of the International Symposium on Code Generation and Optimization: Feedback-directed and Runtime Optimization (Palo Alto, CA, 2004). IEEE Computer Society, Washington, DC, 75--86. Google ScholarDigital Library
- Leino, K.R.M. Efficient weakest preconditions. Inform. Process. Lett. 93, 6 (2005), 281--288. Google ScholarDigital Library
- Mayhem. 1.2K Crashes in Debian, 2013. URL http://lists.debian.org/debian-devel/2013/06/msg00720.html.Google Scholar
- Mayhem. Open Source Statistics & Analysis, 2013. URL http://www.forallsecure.com/summaries.Google Scholar
- Schwartz, E.J., Avgerinos, T., Brumley, D. All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask). In Proceedings of the 31st IEEE Symposium on Security and Privacy (2010). IEEE Computer Society, Washington, DC, 317--331. Google ScholarDigital Library
- Tu, P., Padua, D. Efficient building and placing of gating functions. In Proceedings of the 16th ACM Conference on Programming Language Design and Implementation (La Jolla, CA, 1995). ACM, New York, NY, 47--55. Google ScholarDigital Library
- Xie, Y., Aiken, A. Scalable error detection using boolean satisfiability. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Long Beach, CA, 2005). ACM, New York, NY, 351--363. Google ScholarDigital Library
Index Terms
- Enhancing symbolic execution with veritesting
Recommendations
Enhancing symbolic execution with veritesting
ICSE 2014: Proceedings of the 36th International Conference on Software EngineeringWe present MergePoint, a new binary-only symbolic execution system for large-scale and fully unassisted testing of commodity off-the-shelf (COTS) software. MergePoint introduces veritesting, a new technique that employs static symbolic execution to ...
Veritesting Challenges in Symbolic Execution of Java
Scaling symbolic execution to industrial-sized programs is an important open research problem. Veritesting is a promising technique that improves scalability by combining the advantages of static symbolic execution with those of dynamic symbolic ...
Staged symbolic execution
SAC '12: Proceedings of the 27th Annual ACM Symposium on Applied ComputingRecent advances in constraint solving technology and raw computation power have led to a substantial increase in the effectiveness of techniques based on symbolic execution for systematic bug finding. However, scaling symbolic execution remains a ...
Comments