Skip to the content of the web site.

ECE750-T05 Static Analysis for Software Engineering, F08

I've added a link to my thoughts on talks to the resources page. - September 29, 2008.

I've created the resources page. - September 19, 2008.

I have updated the blurb (PDF format). - September 12, 2008

Lecture 1 info is on the sidebar to the left (Lecture Notes).

L1: Sep 12 Compilers + static analysis. Abstract Syntax Trees. Three-address code. Dataflow analysis. Static checking and program verification. Developer-specified versus implicit properties.
L2: Sep 19 Interprocedural Analysis. Pointer analysis. (I followed Michael Schwartzbach's notes.)
L3: Sep 26 SLAM and Spec#
Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram K. Rajamani, and Abdullah Ustuner. Thorough static analysis of device drivers. ECCS '06. (Thiago/Patrick)
Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# Programming System: An Overview. KRML 136. (Mohamed/Patrick)
L4: Oct 3
Proposals due		 Procedure summaries
Greta Yorsh, Eran Yahav, Satish Chandra. Precise and Concise Procedure Summaries. POPL '08. (Steven/Jonathan)
Viktor Kuncak, Patrick Lam, Karen Zee and Martin Rinard. Modular Pluggable Analyses for Data Structure Consistency. Transactions on Software Engineering, December 2006. (Jiewen/Mohamed)
L5: Oct 10
(Todd moderating)		 Demand-driven analyses
Xin Zheng and Radu Rugina. Demand-Driven Alias Analysis for C. POPL 2008. (Hang/Weining)
Manu Sridharan, Denis Gopan, Lexin Shan, and Rastislav Bodik. Demand-driven points-to analysis for Java. OOPSLA 2005. (Nomair/Steven)
L6: Oct 17 Null derefence checking
Domagoj Babic and Alan J. Hu. Calysto: Scalable and Precise Extended Static Checking. ICSE 2008. (Weining/Hang)
A. Loginov, E. Yahav, S. Chandra, S. Fink, N. Rinetzky, M. G. Nanda. Verifying Derefence Safety via Expanding-Scope Analysis. ISSTA 2008. (Jonathan/Steven)
Extra paper: Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended Static Checking for Java. PLDI '02.
L7: Oct 24 Verification via testing
Nels E. Beckman, Aditya V. Nori, Sriram K. Rajamani, and Robert J. Simmons. Proofs from Tests. MSR TR, January 2008. (Jiewen/Thiago) A conference version also appeared in ISSTA 2008.
L8: Oct 31
Midterm reports		 Concurrency
A. Bouajjani, S. Fratani, and S. Qadeer. Context-bounded analysis of multithreaded programs with dynamic linked structures. Proceedings of the 19th International Conference on Computer Aided Verification, 2007. (Mohamed/Jonathan)
Ravi Chugh, Jan Wen Vuong, Ranjit Jhala, and Sorin Lerner. Dataflow analysis for concurrent programs using datarace detection. PLDI 2008. (Jonathan/Jiewen)
L9: Nov 7 Typestate and tracematches
Stephen Fink, Eran Yahav, Nurit Dor, G. Ramalingam, and Emmanuel Geay. Effective typestate verification in the presence of aliasing. ISSTA 2006. (Nomair/Hang)
Eric Bodden, Patrick Lam and Laurie Hendren. Finding Programming Errors Earlier by Evaluating Runtime Monitors Ahead-of-Time. FSE 2008. (Patrick/Thiago)
L10: Nov 14 Novel program properties
(FSE conference report)
Christopher Unkel and Monica S. Lam. Automatic Inference of Stationary Fields: a Generalization of Java's Final Fields. POPL 2008. (Hang/Nomair)
David Greenfieldboyce and Jeffrey S. Foster. Type Qualifier Inference for Java. OOPSLA 2007. (Weining/Jiewen)
L11: Nov 21 Programming Tools
David Mandelin, Lin Xu, Ras Bodik and Doug Kimelman. Jungloid Mining: Helping to Navigate the API Jungle. PLDI 2005. (Thiago/Nomair)
Suresh Thummalapenta and Tao Xie. PARSEWeb: A Programmer Assistant for Reusing Open Source code on the Web. ASE 2007. (Steven/Weining)
L12: Nov 28 Project Reports & Loose Ends
Bonus paper: Sriram Sankaranarayanan, Swarat Chaudhuri, Franjo Ivancic, and Aarti Gupta. Dynamic Inference of LIkely Data Preconditions over Predicates by Tree Learning. ISSTA 2008.