[1] Aaron Bradley and Zohar Manna. Chapter 1: Propositional Logic. Calculus of Computation. 2010. PDF
[2] Joao Marques-Silva, Ines Lynce, and Sharad Malik. Chapter 4: Conflict-Driven Clause Learning SAT Solvers. Handbook of Satisfiability. 2008. PDF
[3] Carla P. Gomes, Henry Kautz, Ashish Sabharwal, and Bart Selman. Chapter 2: Satisfiability Solvers. Handbook of Knowledge Representation. 2008. PDF
[4] Chris Tucker, David Shuffelton, Ranjit Jhala, and Sorin Lerner. OPIUM: Optimal Package Install/Uninstall Manager. International Conference on Software Engineering (ICSE). 2007. PDF
[5] Leonardo de Moura and Nikolaj Bjorner. Satisfiability Modulo Theories: Introduction and Applications. Communications of the ACM, vol. 54, no. 9. 2011. Web
[6] Aaron Bradley and Zohar Manna. Chapter 9: Quantifier-Free Equality and Data Structures. Calculus of Computation. 2010. PDF
[7] Aaron Bradley and Zohar Manna. Chapter 10: Combining Decision Procedures. Calculus of Computation. 2010. PDF
[8] Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Chapter 12: Satisfiability Modulo Theories. Handbook of Satisfiability. 2008. PDF
[9] Koen Claessen and Niklas Sorensson. New techniques that improve MACE-style finite model finding. CADE-19 Workshop: Model Computation–Principles, Algorithms, Applications. 2003. PDF
[10] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, vol. 12, no. 10. 1969. ACM DL
[11] Aaron Bradley and Zohar Manna. Chapter 5: Program Correctness Mechanics. Calculus of Computation. 2010. PDF
[12] Mike Barnett and K. Rustan M. Leino. Weakest-precondition of unstructured programs. Workshop on Program Analysis for Software Tools and Engineering (PASTE). 2005. ACM DL
[13] Domagoj Babic and Alan J. Hu. Calysto: Scalable and Precise Extended Static Checking. International Conference on Software Engineering (ICSE). 2008. ACM DL
[14] Julian Dolby, Mandana Vaziri, and Frank Tip. Finding bugs efficiently with a SAT solver. Foundations of Software Engineering (FSE). 2007. ACM DL
[15] Greg Dennis, Felix Sheng-Ho Chang, and Daniel Jackson. Modular Verification of Code with SAT. International Symposium on Software Testing and Analysis (ISSTA). 2007. ACM DL
[16] Corina S. Pasareanu and Willem Visser. A survey of new trends in symbolic execution for software testing and analysis. Software Tools for Technology Transfer. 2009. PDF
[17] Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter. Constraints as Control. Principles of Programming Languages (POPL). 2012. ACM DL
[18] Aleksander Milicevic, Derek Rayside, Kuat Yessenov, and Daniel Jackson. Unifying execution of imperative and declarative code. International Conference on Software Engineering (ICSE). 2011. ACM DL
[19] Hesam Samimi, Ei Darli Aung, and Todd Millstein. Falling back on executable specifications. European Conference on Object-Oriented Programming (ECOOP). 2010. PDF
[20] Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. Combinatorial sketching for finite programs. Architectural Support for Programming Languages and Operating Systems (ASPLOS). 2006. ACM DL
[21] Emina Torlak and Rastislav Bodik. A lightweight symbolic virtual machine for solver-aided host languages. Programming Language Design and Implementation (PLDI). 2014. PDF
[22] James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. Optimizing Synthesis with Metasketches. Principles of Programming Languages (POPL). 2016. PDF