A survey of new trends in symbolic execution for software testing and analysis

Anand, S., Godefroid, P., Tillmann, N.: Demand-driven compositional symbolic execution. In: Proceedings of TACAS (2008)

Anand, S., Orso, A., Harrold, M.J.: Type-dependence analysis and program transformation for symbolic execution. In: Proceedings of TACAS (2007)

Anand, S., Păsăreanu, C.S., Visser, W.: Symbolic execution with abstract subsumption checking. In: Proceedings of SPIN (2006)

Anand, S., Păsăreanu, C.S., Visser, W.: JPF-SE: A symbolic execution extension to Java PathFinder. In: Proceedings of TACAS (2007)

Arons, T., Elster E., Ozer S., Shalev J., Singerman, E.: Efficient symbolic simulation of low level software. In: Proceedings of DATE (2008)

Artho C., Barringer H., Goldberg A., Havelund K., Khurshid S., Lowry M.R., Păsăreanu C.S., Rosu G., Sen K., Visser W., Washington R.: Combining test case generation and runtime verification. Theor. Comput. Sci. 336(2–3), 209–234 (2005)

Artzi, S., Kiezun, A., Dolby, J., Tip, F., Dig, D., Paradkar, A., Ernst, M.D.: Finding bugs in dynamic web applications. In: Proceedings of ISSTA (2008)

Babic, D.: Exploiting Structure for Scalable Software Verification. Ph.D. thesis, University of British Columbia, Vancouver, Canada, Aug (2008)

Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: Proceedings of PLDI (2001)

Berdine, J., Calcagno, C., O’Hearn, P.: Symbolic execution with separation logic. In: Proceedings of Third Asian Symposium (2005)

Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on Java predicates. In: Proceedings of ISSTA (2002)

Bush W.R., Pincus J.D., Sielaff D.J.: A static analyzer for finding dynamic programming errors. Softw. Pract. Experience 30(7), 775–802 (2000)

Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: automatically generating inputs of death. In: Proceedings of ACM Conference on Computer and Communications Security (2006)

The Choco Constraint Solver: http://choco.sourceforge.net/

Clarke L.A.: A system to generate test data and symbolically execute programs. IEEE Trans. Softw. Eng. 2(3), 215–222 (1976)

Coen-Porisini, A., Denaro, G., Ghezzi, C., Pezze, M.: Using symbolic execution for verifying safety-critical systems. In: Proceedings of ESEC/FSE (2001)

Colon, M., Sankaranarayanan, S., Sipma, S.: Linear invariant generation using non-linear constraint solving. In: Proceedings of CAV (2003)

Cousot, P.: The role of abstract interpretation in formal methods. In: Proceedings of SEFM (2007)

Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of POPL (1978)

Csallner, C., Smaragdakis, Y.: Check ‘n’ crash: Combining static checking and testing. In: Proceedings of ICSE (2005)

Csallner, C., Tillmann, N., Smaragdakis, Y.: DySy: Dynamic symbolic execution for invariant inference. In: Proceedings of ICSE (2008)

CVC3: http://www.cs.nyu.edu/acsys/cvc3/

The Daikon invariant detector: http://groups.csail.mit.edu/pag/daikon//

Deng, X., Lee, J., Robby: Bogor/kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems. In: Proceedings of ASE (2006)

Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Research Report 159, Compaq Systems Research Center (1998)

Emmi, M., Majumdar, R., Sen, K.: Dynamic test input generation for database applications. In: Proceedings of ISSTA (2007)

Engler, D., Dunbar, D.: Under-constrained execution: making automatic code destruction easy and scalable. In: Proceedings of ISSTA (2007)

Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of PLDI (2002)

Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Proceedings of POPL (2002)

Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. In: Proceedings of ESEC/FSE (1999)

Godefroid, P.: Software model checking via static and dynamic program analysis. In: MOVEP (2006)

Godefroid, P.: Compositional dynamic test generation. In: Proceedings of POPL (2007)

Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of PLDI (2005)

Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: SYNERGY: a new algorithm for property checking. In: Proceedings of SIGSOFT FSE (2006)

Hantler S.L., King J.C.: An introduction to proving the correctness of programs. ACM Comput. Surv. 8(3), 331–353 (1976)

Hong, H., Lee, I., Sokolsky, O., Ural, H.: A temporal logic based theory of test coverage and generation. In: Proceedings of TACAS, April (2002)

IASolver (The Brandeis Interval Arithmetic Constraint Solver): http://www.cs.brandeis.edu/~tim/Applets/IAsolver.html/

Java PathFinder: http://javapathfinder.sourceforge.net

Joshi, P., Sen, K., Shlimovich, M.: Predictive testing: Amplifying the effectiveness of software testing (short paper). In: Proceedings of ESEC/FSE (2007)

Khurshid, S., Garcia, I., Suen, Y.: Repairing structurally complex data. In: Proceedings of SPIN (2005)

Khurshid, S., Păsăreanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Proceedings of TACAS (2003)

King J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)

Koelbl A., Pixley C.: Constructing efficient formal models from high-level descriptions using symbolic simulation. Int. J. Parallel Programm. 33(6), 645–666 (2005)

Majumdar, R., Sen, K.: Hybrid concolic testing. In: Proceedings of ICSE (2007)

Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Proceedings of VMCAI, LNCS, vol. 3385, Paris (2005)

Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems:Specification (1992)

Păsăreanu, C.S., Visser, W.: Verification of java programs using symbolic execution and invariant generation. In: Proceedings of SPIN (2004)

Person, S., Dwyer, M.B., Elbaum, S., Păsăreanu, C.S.: Differential symbolic execution. In: Proceedings of FSE (2008)

PEX: Automated Exploratory Testing for .NET: http://research.microsoft.com/Pex/

Păsăreanu, C.S., Mehlitz, P., Bushnell, D., Gundy-Burlet, K., Lowry, M., Person, S., Pape, M.: Combining unit-level symbolic execution and system-level concrete execution for testing nasa software. In: Proceedings of ISSTA (2008)

Pugh, W.: The Omega test: A fast and practical integer programming algorithm for dependence analysis. In: Conference on High Performance Networking and Computing archive. Proceedings of the 1991 ACM/IEEE Conference on Supercomputing table of contents Albuquerque, New Mexico, pp. 4–13 (1991)

SAT Competitions: http://www.satcompetition.org/

Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Proceedings of ESEC/FSE (2005)

Shannon, D., Hajra, S., Lee, A., Zhan, D., Khurshid, S.: Abstracting symbolic execution with string analysis. In: Proceedings of TAIC-PART (2007)

Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Using model checking with symbolic execution to verify parallel numerical programs. In: Proceedings of ISSTA (2006)

Sinha, N.: Symbolic program analysis using term rewriting and generalization. In: Proceedings of FMCAD, Nov. (2008)

SMT Competitions: http://www.smtcomp.org/

STP (Simple Theorem Prover): http://sourceforge.net/projects/stp-fast-prover

Tiwari, A., Rues, H., Saidi, H., Shankar, N.: A technique for invariant generation. In: Proceedings of TACAS (2001)

Tomb, A., Brat, G., Visser, W.: Variably interprocedural program analysis for runtime error detection. In: Proceedings of ISSTA (2007)

Tomb, A., Brat, G.P., Visser, W.: Variably interprocedural program analysis for runtime error detection. In: Proceedings of ISSTA (2007)

Visser, W., Păsăreanu, C.S., Pelanek, R.: Test input generation for java containers using state matching. In: Proceedings of ISSTA (2006)

Visser, W., Păsăreanu, C.S., Khurshid, S.: Test input generation in Java Pathfinder. In: Proceedings of ISSTA (2004)

Wassermann, G., Yu, D., Chander, A., Dhurjati, D., Inamura, H., Su, Z.: Dynamic test input generation for web applications. In: Proceedings of ISSTA (2008)

Wegbreit B.: The synthesis of loop predicates. Commun. ACM 17(2), 102–112 (1974)

Xie, T., Marinov, D., Schulte, W., Notkin, D.: Symstra: A framework for generating object-oriented unit tests using symbolic execution. In: Proceedings of TACAS (2005)

Xu, R.-G., Godefroid, P., Majumdar, R.: Testing for buffer overflows with length abstraction. In: Proceedings of ISSTA (2008)

Yavuz-Kahveci, T., Bultan, T.: Automated verification of concurrent linked lists with counters. In: Hermenegildo, G.P.M. (ed.) Proceedings of SAS (2002)

Yices: An SMT Solver http://yices.csl.sri.com/

Yorsh, G., Ball, T., Sagiv, M.: Testing, abstraction, theorem proving: better together!. In: Proceedings of ISSTA (2006)