Syllabus
The table below gives the planned syllabus for the seminar. The syllabus lists the topics and papers to be discussed.
Material describing the course is available elsewhere.
Students should study the paper to be discussed prior to the meeting so that they can participate in the discussion.
This syllabus is provisional and subject to change. If it is necessary to revise the schedule, then this page will be updated to reflect the changes.
Date | Paper or Topic | Discussion Leader |
---|---|---|
Aug. 22 | Overview, background, planning | Gary |
Aug. 29 | Continuity and Robustness of Programs [Chaudhuri-Gulwani-Lublinerman12] | Gary Leavens |
Sep. 5 | Program Slicing Enhances a Verification Technique Combining Static and Dynamic Analysis [Chebaro-etal11] | Rochelle Elva |
Sep. 12 | Using Debuggers to Understand Failed Verification Attempts [Mueller-Ruskiewicz11] | Yuyan Bao |
Sep. 19 | A Dynamic Program Analysis to find Floating-Point Accuracy Problems [Benz-etal12] | Cheng Wei |
Sep. 26 | Synthesis of Loop-Free Programs [Gulwani-etal11] | Faraz Hussain |
Oct. 3 | A Type System for Complexity Flow Analysis [Marion11] | Yuyan Bao |
Oct. 10 | Separating Obligations of Subjects and Handlers for More Flexible Event Type Verification | Gary Leavens |
Oct. 17 | Modular and Verified Automatic Program Repair [Logozzo-Ball12] | Cheng Wei |
Oct. 24 | No class (SPLASH) | |
Oct. 31 | Symbolic execution and program testing [King76] | Gary Leavens |
Nov. 7 | No class | |
Nov. 14 | Checking reachability using matching logic [Rosu-Stefanescu-12] | Yuyan Bao |
Nov. 21 | No class (just before Thanksgiving) | |
Nov. 28 | Scaling symbolic execution using ranged analysis [Siddiqui-Khurshid12] | Rochelle Elva |
Bibliography
Note that you can use each paper's DOI link to get a copy of it, when you are on the UCF network.
- [Benz-etal12]
- Florian Benz, Andreas Hildebrandt, and Sebastian Hack. A dynamic program analysis to find floating-point accuracy problems. In PLDI'12 Proceedings of the 33rd ACM SIGPLAN conference on Programming Language Design and Implementation, pp. 453-462, Beijing, June 2012. http://dx.doi.org/10.1145/2254064.2254118
- [Chaudhuri-Gulwani-Lublinerman12]
- Swarat Chaudhuri, Sumit Gulwani, and Roberto Lublinerman. Continuity and robustness of programs. CACM 55(8):107-115, August 2012. http://doi.acm.org/10.1145/2240236.2240262
- [Chebaro-etal11]
- Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, and Jacques Julliand. Program Slicing Enhances a Verification Technique Combining Static and Dynamic Analysis. SAC'12, March 25-29, 2012, Riva del Garda, Italy. http://dx.doi.org/10.1145/2245276.2231980
- [Gulwani-etal11]
- Sumit Sulwani, Susmit Jha, Ashish Tiwari, and Ramarathnam Venkatesan. Synthesis of Loop-free Programs. PLDI'11, June 4-8, 2011, San Jose, California, USA. http://dx.doi.org/10.1145/1993498.1993506
- [King76]
- James C. King. Symbolic execution and program testing. Comm. ACM, 19(7):385-394, July 1976. http://dx.doi.org/10.1145/360248.360252
- [Marion11]
- Jean-Yves Marion. A Type System for Complexity Flow Analysis. Proc. of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 123-132, 2011, Toronto, Ontario, Canada. http://dx.doi.org/10.1109/LICS.2011.41
- [Logozzo-Ball12]
- Francesco Logozzo and Thomas Ball. Modular and Verified Automatic Program Repair. In OOPSLA '12, pp. 133-146, Tucson, Arizona, 2012. http://dx.doi.org/10.1145/2384616.2384626.
- [Mueller-Ruskiewicz11]
- Peter Müller and Joseph N. Ruskiewicz. Using Debuggers to Understand Failed Verification Attempts. In M. Buter and W. Schulte (eds.). FM 2011, Vol. 6664 of Lecture Notes in Computer Science, pp. 73-87, 2011. http://dx.doi.org/10.1007/978-3-642-21437-0_8
- [Rosu-Stefanescu12]
- Grigore Rosu and Andrei Stefanescu. Checking reachability using matching logic. In OOPSLA '12, pp. 555-574, Tucson, Arizona, 2012. http://doi.acm.org/10.1145/2384616.2384656
- [Siddiqui-Khurshid12]
- Junaid Haroon Siddiqui and Sarfraz Khurshid. Scaling symbolic execution using ranged analysis. In OOPSLA '12, pp. 523-536, Tucson, Arizona, 2012. http://dx.doi.org/10.1145/2384616.2384654
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Last modified Tuesday, November 6, 2012.