Reading list for CS 4950

[1] Edsger W. Dijkstra. Concern for correctness as a guiding principle for program construction. Circulated privately, July 1970. [ bib | .PDF ]
[2] C. A. R. Hoare. Proof of a program: FIND. Commun. ACM, 14(1):39--45, 1971. [ bib | DOI ]
[3] C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576--580, 1969. [ bib | DOI ]
[4] Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 46--57. IEEE Computer Society, 1977. [ bib | DOI ]
[5] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In E. Allen Emerson and A. Prasad Sistla, editors, Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, volume 1855 of Lecture Notes in Computer Science, pages 154--169. Springer, 2000. [ bib | DOI ]
[6] Thomas Ball, Rupak Majumdar, Todd D. Millstein, and Sriram K. Rajamani. Automatic predicate abstraction of C programs. In Michael Burke and Mary Lou Soffa, editors, Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Snowbird, Utah, USA, June 20-22, 2001, pages 203--213. ACM, 2001. [ bib | DOI ]
[7] Thomas Wahl and Vijay D'Silva. A lazy approach to symmetry reduction. Formal Aspects Comput., 22(6):713--733, 2010. [ bib | DOI ]
[8] Parosh Aziz Abdulla, Frédéric Haziza, and Lukás Holík. All for the price of few. In Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni, editors, Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings, volume 7737 of Lecture Notes in Computer Science, pages 476--495. Springer, 2013. [ bib | DOI ]
[9] Ishai Rabinovitz and Orna Grumberg. Bounded model checking of concurrent programs. In Kousha Etessami and Sriram K. Rajamani, editors, Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings, volume 3576 of Lecture Notes in Computer Science, pages 82--97. Springer, 2005. [ bib | DOI ]
[10] Cormac Flanagan and Shaz Qadeer. Transactions for software model checking. Electron. Notes Theor. Comput. Sci., 89(3):518--539, 2003. [ bib | DOI ]
[11] Domagoj Babic and Alan J. Hu. Structural abstraction of software verification conditions. In Werner Damm and Holger Hermanns, editors, Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings, volume 4590 of Lecture Notes in Computer Science, pages 366--378. Springer, 2007. [ bib | DOI ]
[12] Qinheping Hu, Jason Breck, John Cyphert, Loris D'Antoni, and Thomas W. Reps. Proving unrealizability for syntax-guided synthesis. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, volume 11561 of Lecture Notes in Computer Science, pages 335--352. Springer, 2019. [ bib | DOI ]
[13] Grigory Fedyukovich, Yueling Zhang, and Aarti Gupta. Syntax-guided termination analysis. In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, volume 10981 of Lecture Notes in Computer Science, pages 124--143. Springer, 2018. [ bib | DOI ]
[14] Edsger W. Dijkstra. Answers to questions from students of software engineering. Circulated privately, November 2000. [ bib | .PDF ]
[15] James C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385--394, 1976. [ bib | DOI ]

This file was generated by bibtex2html 1.98.