Reading: Correspondence between CPS and SSA

Tuesday, Dan will lead us in discussion of

Kelsey, R. A. 1995. A correspondence between continuation passing style and static single assignment form. In Papers From the 1995 ACM SIGPLAN Workshop on intermediate Representations (San Francisco, California, United States, January 22 - 22, 1995). ACM, New York, NY, 13-22. DOI= http://doi.acm.org/10.1145/202529.202532

Reading assignment: Trace collection through slicing

Suzanne will lead discussion of

Zhai, J., Sheng, T., He, J., Chen, W., and Zheng, W. 2009. FACT: fast communication trace collection for parallel applications through program slicing. In Proceedings of the Conference on High Performance Computing Networking, Storage and Analysis (Portland, Oregon, November 14 - 20, 2009). SC '09. ACM, New York, NY, 1-12. DOI= http://doi.acm.org/10.1145/1654059.1654087

String predicates as finite automata

One of the interesting things mentioned in the paper we discussed Tuesday was work on using automata to characterize strings. If you're interested in the paper that was reference [54], the IEEE DL link is:
http://doi.ieeecomputersociety.org/10.1109/TAIC.PART.2007.34

A related paper is Precise
analysis of string expressions by A. Christensen, A. Møller, and M. Schwartzbach, in Proc. 10th International
Static Analysis Symposium (SAS’03) June 2004.

Paper: Trends in symbolic execution

Dan will lead discussion of A Survey of New Trends in Symbolic Execution for Software Testing and Analysis, by Corina S. Păsăreanu and Willem Visser.  This looks like a nice overview as well as having a couple of new twists.

Paper: Symbolic complexity bounds

With apologies for being late in posting this ...

 http://research.microsoft.com/en-us/um/people/sumitg/pubs/cav09_speed.pdf

Related project:
http://research.microsoft.com/en-us/um/people/sumitg/pubs/speed.html

---

Addendum Monday evening: Wow, I didn't understand much of that. It seems that they are describing a bunch of refinements to a basic technique that involves placing a counter variable in the code and then inferring numerical bounds on the counter. Unfortunately I don't understand that basic technique of using counter variables. There are gobs of citations to reference [9], which is a POPL 2009 paper. I had a look at that paper, though not a deep one ... it does seem to be more complete, but it too seems to be building on the basic technique with counters, and again without explanation. I guess it's supposed be something that the intended audience already knows. But I don't.

Anybody know something about this? I'm sure I can track it down, but I'm also pretty sure I can't do it before class tomorrow.