Textbook 

BM 
Aaron R. Bradley and Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. 2007. 
 
Papers 

H69 
C. A. R. Hoare. An Axiomatic Basis for Computer Programming. CACM, vol. 12., no. 10, 1969. 
CES86 
Edmund M. Clarke, E. Allen Emerson and A. Prasad Sistla. Automatic Verification of FiniteState
Concurrent Systems Using Temporal Logic. TOPLAS, vol. 8, no. 2, 1986. 
GKSS08 
Carla P. Gomes, Henry Kautz, Ashish Sabharwal, and Bart Selman. Satisfiability Solvers. Handbook of Knowledge Representation, Chapter 2, 2008. 
SLM08 
Joao MarquesSilva, Ines Lynce and Sharad Malik. ConflictDriven Clause Learning
SAT Solvers. Handbook of Satisfiability, Chapter 4, 2008. 
MB11 
Leonardo de Moura and Nikolaj Bjorner. Satisfiability Modulo Theories: Introduction and Applications. CACM, vol. 54, no. 9, 2011. 
BSST08 
Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability Modulo Theories. Handbook of Satisfiability, Chapter 12, 2008. 
LM08 
Chu Min Li and Felip Manyà. MaxSAT, Hard and Soft Constraints. Handbook of Satisfiability, Chapter 19, 2008. 
BCCZ99 
Armin Biere, Alessandro Cimatti, Edmund M. Clarke and Yunshan Zhu. Symbolic Model Checking without BDDs. TACAS, 1999. 
M03 
Kenneth L. McMillan. Interpolation and SATBased Model Checking. CAV, 2003.

JM09 
Ranjit Jhala and Rupak Majumdar. Software Model Checking. ACM Computing Surveys, vol. 41, no. 4, 2009.

BMMR01 
Thomas Ball, Rupak Majumdar, Todd Millstein and
Sriram K. Rajamani. Automatic Predicate Abstraction of C Programs. PLDI, 2001.

CGJLV03 
Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu and Helmut Veith. Counterexampleguided Abstraction Refinement for Symbolic Model Checking. JACM, vol. 50, no. 5, 2003.

GKK05 
Patrice Godefroid, Nils Klarlund and Koushik Sen. DART: Directed Automated Random Testing. PLDI, 2005.

CS03 
Cristian Cadar and Koushik Sen. Symbolic Execution for Software Testing: Three Decades Later. CACM, vol. 56, no. 2, 2013.

STBSS06 
Armando SolarLezama, Liviu Tancau, Rastislav Bodik, Vijay Saraswat and Sanjit Seshia. Combinatorial Sketching for Finite Programs. ASPLOS, 2006.

SGF10 
Saurabh Srivastava, Sumit Gulwani and Jeff Foster. From Program Verification to Program Synthesis. POPL, 2010.

G10 
Sumit Gulwani. Automating String Processing in Spreadsheets using InputOutput Examples. POPL, 2010.

RVY14 
Veselin Raychev, Martin Vechev and Eran Yahav. Code Completion with Statistical Language Models. PLDI, 2014.

A13 
Rajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando SolarLezama, Emina Torlak and Abhishek Udupa: SyntaxGuided Synthesis. FMCAD, 2013.

DSS16 
Loris D'Antoni, Rishabh Singh and Roopsha Samanta. Qlose: Program Repair with Quantitative Objectives. CAV, 2016.

OG76 
Susan Owicki and David Gries. Verifying Properties of Parallel Programs: An Axiomatic Approach. CACM, vol. 19, no. 5, 1976.

L77 
Leslie Lamport. Proving the Correctness of Multiprocess Programs. Trans. on Software Engineering, vol. 3, no. 2, 1977.

EQT09 
Tayfun Elmas, Shaz Qadeer, and Serdar Tasiran. A Calculus of Atomic Actions. POPL, 2009.

G90 
Patrice Godefroid. Using Partial Orders to Improve Automatic Verification Methods. CAV, 1990.

D93 
Doron Peled. All from One, One for All:
On Model Checking Using Representatives. CAV, 1993.

WKGG09 
Chao Wang, Sudipta Kundu, Malay Ganai and Aarti Gupta. Symbolic Predictive Analysis for Concurrent Programs. FM, 2009.

QR05 
Shaz Qadeer and Jakob Rehof. ContextBounded Model Checking of Concurrent Software. TACAS, 2005.

VYY10 
Martin Vechev, Eran Yahav and Greta Yorsh. Abstractionguided Synthesis of Synchronization. POPL, 2010.

G15 
Ashutosh Gupta, Thomas A. Henzinger, Arjun Radhakrishna, Roopsha Samanta and Thorsten Tarrach Succinct Representation of Concurrent Trace Sets. POPL, 2015.

C15 
Pavol Cerny, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta and Thorsten Tarrach. From Nonpreemptive to Preemptive Scheduling using Synchronization Synthesis. CAV, 2015.
