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: poly.rkt, gotchas.rkt

L02: bvlang.rkt

L05: zune.rkt

L06: ex1.smt2, ex2.smt2, ex3.smt2, ex4.smt2, ex5.smt2

L07: cc.rkt

L09: dpllt.rkt

L12: RingBuffer.dfy, Lemma.dfy