References
Reading
[1] Emina Torlak and Rastislav Bodik. A lightweight symbolic virtual machine for solver-aided host languages. Programming Language Design and Implementation (PLDI). 2014. PDF
[2] James Bornholt and Emina Torlak. Finding Code That Explodes Under Symbolic Evaluation. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). 2018. PDF
[3] Aaron Bradley and Zohar Manna. Chapter 1: Propositional Logic. Calculus of Computation. 2010. PDF
[4] Joao Marques-Silva, Ines Lynce, and Sharad Malik. Chapter 4: Conflict-Driven Clause Learning SAT Solvers. Handbook of Satisfiability. 2008. PDF
[5] Carla P. Gomes, Henry Kautz, Ashish Sabharwal, and Bart Selman. Chapter 2: Satisfiability Solvers. Handbook of Knowledge Representation. 2008. PDF
[6] Edmund Clarke, Daniel Kroening, and Flavio Lerda. A Tool for Checking ANSI-C Programs. Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 2004. Springer
[7] Leonardo de Moura and Nikolaj Bjorner. Satisfiability Modulo Theories: Introduction and Applications. Communications of the ACM, vol. 54, no. 9. 2011. Web
[8] Aaron Bradley and Zohar Manna. Chapter 9: Quantifier-Free Equality and Data Structures. Calculus of Computation. 2010. PDF
[9] Aaron Bradley and Zohar Manna. Chapter 10: Combining Decision Procedures. Calculus of Computation. 2010. PDF
[10] Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Chapter 12: Satisfiability Modulo Theories. Handbook of Satisfiability. 2008. PDF
[11] Baoluo Meng, Andrew Reynolds, Cesare Tinelli, and Clark Barrett. Relational Constraint Solving in SMT. Automated Deduction (CADE 26). 2017. Springer
[12] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, vol. 12, no. 10. 1969. ACM DL
[13] Aaron Bradley and Zohar Manna. Chapter 5: Program Correctness Mechanics. Calculus of Computation. 2010. PDF
[14] K. Rustan M. Leino. Accessible Software Verification with Dafny. IEEE Software. 2017. IEEE Xplore
[15] Roberto Baldoni, Emilio Coppa, Daniele Cono D’elia, Camil Demetrescu, and Irene Finocchi. A Survey of Symbolic Execution Techniques. ACM Computing Surveys (CSUR). 2018. ACM DL
[16] Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter. Constraints as Control. Principles of Programming Languages (POPL). 2012. ACM DL
[17] 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
[18] Ali Sinan Köksal, Yewen Pu, Saurabh Srivastava, Rastislav Bodík, Jasmin Fisher, Nir Piterman. Synthesis of biological models from mutation experiments. Principles of Programming Languages (POPL). 2013. ACM DL
[19] Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. Program Synthesis. Foundations and Trends in Programming Languages. 2017. PDF
Code
L01: bvudiv2.rkt, gotchas.rkt
L02: bvlang.rkt, revpos.rkt
L05: zune.rkt, config.rkt
L07: cc.rkt
L09: dpllt.rkt
L10: fs.als, fs.thm, pigeonhole.als, pigeonhole.smt2
L13: Demo.dfy