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.