[1] Bradley, A. and Manna, Z. Chapter 1: Propositional Logic. Calculus of Computation. 2010. PDF.
[2] Marques-Silva, J., Lynce, I. and Malik, S. Chapter 4: Conflict-Driven Clause Learning SAT Solvers. Handbook of Satisfiability. 2008. PDF.
[3] Gomes, C.P., Kautz, H., Sabharwal, A. and Selman, B. Chapter 2: Satisfiability Solvers. Handbook of Knowledge Representation. 2008. PDF.
[4] Tucker, C., Shuffelton, D., Jhala, R. and Lerner, S. OPIUM: Optimal Package Install/Uninstall Manager. International Conference on Software Engineering (ICSE). 2007. PDF.
[5] de Moura, L. and Bjorner, N. Satisfiability Modulo Theories: Introduction and Applications. Communications of the ACM. Vol 54, No 9. 2011. Web.
[6] Bradley, A. and Manna, Z. Chapter 9: Quantifier-Free Equality and Data Structures. Calculus of Computation. 2010. PDF.
[7] Bradley, A. and Manna, Z. Chapter 10: Combining Decision Procedures. Calculus of Computation. 2010. PDF.
[8] Barrett, C., Sebastiani, R., Seshia, S.A. and Tinelli, C. Chapter 12: Satisfiability Modulo Theories. Handbook of Satisfiability. 2008. PDF.
[9] Claessen, K. and Sorensson, N. New techniques that improve MACE-style finite model finding. CADE-19 Workshop: Model Computation—Principles, Algorithms, Applications. 2003. PDF.
[10] Hoare, C.A.R. An axiomatic basis for computer programming. Communications of the ACM. Vol 12, No 10. 1969. ACM DL.
[11] Barnett, M. and Leino, K.R.M. Weakest-precondition of unstructured programs. SIGSOFT Softw. Eng. Notes. Vol 31, No 1. 2005. ACM DL.
[12] Babic, D. and Hu, A.J. Calysto: Scalable and Precise Extended Static Checking. International Conference on Software Engineering (ICSE). 2008. ACM DL.
[13] Dolby, J., Vaziri, M. and Tip, F. Finding bugs efficiently with a SAT solver. Foundations of Software Engineering (FSE). 2007. ACM DL.
[14] Dennis, G., Chang, F.S.-H. and Jackson, D. Modular Verification of Code with SAT. International Symposium on Software Testing and Analysis (ISSTA). 2007. ACM DL.
[15] Cadar, C. et al. Symbolic execution for software testing in practice: preliminary assessment. International Conference on Software Engineering (ICSE). 2011. ACM DL.
[16] Emerson, E.A. The Beginning of Model Checking: A Personal Perspective. 25 Years of Model Checking, Lecture Notes in Computer Science. Vol 5000. 2008. Springer PDF.
[17] Clarke, E.M. and Schlingloff, B.-H. Chapter 21: Model checking. Handbook of Automated Reasoning. 2001. PDF.
[18] Jhala, R. and Majumdar, R. Software model checking. ACM Compu. Surv. Vol 41, No 4. 2009. ACM DL.
[19] Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S. and Saraswat, V. Combinatorial sketching for finite programs. Architectural Support for Programming Languages and Operating Systems (ASPLOS). 2006. ACM DL.
[20] Köksal, A.S., Kuncak, V. and Suter, P. Constraints as control. Principles of Programming Languages (POPL). 2012. ACM DL.
[21] Milicevic, A., Rayside, D., Yessenov, K. and Jackson, D. Unifying execution of imperative and declarative code. International Conference on Software Engineering (ICSE). 2011. ACM DL.
[22] Samimi, H., Aung, E.D. and Millstein, T. Falling back on executable specifications. European conference on Object-oriented programming (ECOOP). 2010. PDF.