| Reading | Description |
|---|---|
| [0] | Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, Michael Deardeuff. Use of Formal Methods at Amazon Web Services. 2014. |
| [1] | Aaron Bradley and Zohar Manna. Chapter 1: Propositional Logic. Calculus of Computation. 2010. |
| [2] | Joao Marques-Silva, Ines Lynce, and Sharad Malik. Chapter 4: Conflict-Driven Clause Learning SAT Solvers. Handbook of Satisfiability. 2008. |
| [3] | Carla P. Gomes, Henry Kautz, Ashish Sabharwal, and Bart Selman. Chapter 2: Satisfiability Solvers. Handbook of Knowledge Representation. 2008. |
| [4] | Chris Tucker, David Shuffelton, Ranjit Jhala, and Sorin Lerner. OPIUM: Optimal Package Install/Uninstall Manager. International Conference on Software Engineering (ICSE). 2007. |
| [5] | Leonardo de Moura and Nikolaj Bjorner. Satisfiability Modulo Theories: Introduction and Applications. Communications of the ACM, vol. 54, no. 9. 2011. |
| [6] | Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Chapter 12: Satisfiability Modulo Theories. Handbook of Satisfiability. 2008 |
| [7] | Koen Claessen and Niklas Sorensson. New techniques that improve MACE-style finite model finding. CADE-19 Workshop: Model Computation–Principles, Algorithms, Applications. 2003. |
| [8] | Daniel Jackson. Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology. 2002. |
| [9] | Allison Sullivan, Kaiyuan Wang, Razieh N. Zaeem, and Ssarfraz Khurshid. Automated test generation and mutation testing for Alloy. IEEE Conference on Software Testing, Validation and Verification (ICST). 2017. |
| [10] | C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, vol. 12, no. 10. 1969. |
| [11] | Aaron Bradley and Zohar Manna. Chapter 5: Program Correctness Mechanics. Calculus of Computation. 2010. |
| [12] | Mike Barnett and K. Rustan M. Leino. Weakest-precondition of unstructured programs. Workshop on Program Analysis for Software Tools and Engineering (PASTE). 2005. |
| [13] | Domagoj Babic and Alan J. Hu. Calysto: Scalable and Precise Extended Static Checking. International Conference on Software Engineering (ICSE). 2008. |
| [14] | Julian Dolby, Mandana Vaziri, and Frank Tip. Finding bugs efficiently with a SAT solver. Foundations of Software Engineering (FSE). 2007. |
| [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. |
| [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. |
| [17] | Clarke, E.M. and Schlingloff, B.-H. Chapter 21: Model checking. Handbook of Automated Reasoning. 2001. |
| [18] | Jhala, R. and Majumdar, R. Software model checking. ACM Compu. Surv. Vol 41, No 4. 2009. |
| [19] | 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. |
| [20] | Roberto Baldoni, Emilio Coppa, Daniele Cono D’elia, Camil Demetrescu, and Irene Finocchi. A Survey of Symbolic Execution Techniques. ACM Computing Surveys (CSUR). 2018. |
| [21] | Koushik Sen and Darko Marinov and Gul Agha. CUTE: a concolic unit testing engine for C. International symposium on Foundations of software engineering. 2005 |
| [22] | Patrice Godefroid and Nils Klarlund and Koushik Sen. DART: directed automated random testing. Programming language design and implementation. 2005 |
| [23] | 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 |
| [24] | Rajeev Alur and Arjun Radhakrishna and Abhishek Udupa. Scaling Enumerative Program Synthesis via Divide and Conquer. Tools and Algorithms for the Construction and Analysis of Systems. 2017 |
| [25] | Kaiyuan Wang and Allison Sullivan and Sarfraz Khurshid. Automated Model Repair for Alloy. International Conference on Automated Software Engineering. 2018. |
| [26] | Kaiyuan Wang and Allison Sullivan and Darko Marinov and Sarfraz Khurshid. Solver-based Sketching of Alloy Models using Test Valuations. ABZ. 2018. |
| [27] | Jinru Hua and Sarfraz Khurshid. EdSketch: Execution-Driven Sketching for Java. International SPIN Symposium on Model Checking of Software. 2017. |
| [28] | James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. Optimizing Synthesis with Metasketches. Principles of Programming Languages (POPL). 2016. |
| [29] | Emina Torlak and Rastislav Bodik. A lightweight symbolic virtual machine for solver-aided host languages. Programming Language Design and Implementation (PLDI). 2014. |
| [30] | James Bornholt and Emina Torlak. Finding Code That Explodes Under Symbolic Evaluation. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). 2018. |