Academics: Part 3 of 5: "Program Analysis"

“Had Darth Vader employed formal methods to the design of his Death Star, perhaps it would not have been vulnerable to the starfighter attack that led to its destruction.”

- Jose Meseguer and Grigore Rosu, professors of computer science at UIUC, in their research description

-----------------------------------------------------------

For my third post in this series I will talk about...

Program Analysis and Understanding with Jeff Foster

This is a graduate level course that is a lot different than any of the other computer science courses I have taken. We do very little programming in the class; instead, the focus is using mathematical logic to prove properties of computer programs.

Some of the topics we have learned about so far include:

Dataflow Analysis - this involves tracking different facts about the data manipulated by a program (like "variable X is always zero here" or "variable Y will always be overwritten by another value before it is used) through the execution of a program. The algorithm for doing this is actually reasonably straightfoward - basically, you first generate a "control flow graph" shoing all the different possible ways that control can proceed through the program (for example, an if statement would be a branch in the control flow graph, since control could go two one of two different places depending on the result of the if statement) and then propagate the facts along the edges of the graph. One area of active research now is dataflow analysis for multithreaded programs - where there are two or more separate "threads" of execution, and it is not known which thread will be executed first and when the operating system will decide to switch the control between threads. This of course makes dataflow analysis a lot harder because you don't actually know what the "control flow graph" looks like.

Automated Proof Systems - This involves repesenting logical statements (like "for all integers A and B, A+B = B+A") and proofs of those statements in a form that a computer can manipulate. For example, in the example above, you would first have to define "integer" - the way you do that is by saying "0 is an integer, and for every integer X, there exists a successor S(X)." From this definition it is possible to define operations like addition and multiplication, and then prove statements like the one above. The way you prove statements in Coq (the proof system we are using) is by giving a series of "tactics" that specify how to get from the hypotheses (the things you know are true) to the goal (the thing you are trying to prove.) Examples of tactics are:

Rewrite - If you know that A=B, then you can replace all the A's in an expression with B's, or vice versa.

Destruct - This "breaks apart" a term into all the possibilities for what it is, so you can do analysis on a case-by-case basis. For example if X is a boolean value (true or false), then "destruct X" would create two branches of the proof - one where X is true and one where X is false. This allows you to prove things like DeMorgan's Laws (by enumerating all the cases).

Apply - If you know that "if A then B", and your goal is B, this changes the goal to be A. This makes sense because if you know A and if you know "if A then B" then you know B.

(One good thing about automated proof systems from a teacher's perspective is that it makes it really easy to grade the homeworks. If the proof goes through and doesn't generate an error, then it must be correct.)

Automated proof systems are also useful in proving things about computer programs. If you define the syntax of a programming language in Coq, then you can represent statements like "the expression X+Y evaluates to 7 given the variable values X=3 and Y=4" and prove things like that the final result of an expression is the same no matter what order you evaluate its terms in (this is true in the simplified language we are studying, but not true in many real programming languages.)

Also, just yesterday my professor was quoted in a Diamondback article. (See the second page of the article for his quote.)

-----------------------------

P.S. The quote at the top of this post is inaccurate. Darth Vader had nothing to do with the design or construction of the Death Star.

Academics: Part 2 of 5: "Answer Poverty"

Today, we did our final presentation for our Gemstone project.

Our Gemstone project was titled "ANSWER Poverty," which stands for "Assessing the Need for Services which Effectively Reduce Poverty." During our project, we interviewed recent immigrants living in Langley Park, a community just a few minutes away from Campus that has a high number of low-income immigrants. Our goal was to find out their experiences with and knowledge of financial services. The point of our project was to find ways of bringing people who currently use "fringe" financial services like check cashing, money wiring to pay bills, payday loans, etc. into the mainstream banking system, so they don't lose a large percentage of their paycheck to things like check cashing fees.

What we found in our focus groups was surprising in many ways. First of all, most of our focus group participants didn't even know what check cashing was, and only one out of several dozen total participants mentioned using it. This was surprising because Langley Park has a lot of check cashing outlets, which is why we chose it. We also found that for many members of our target population, mainstream banks could have fees such as overdraft fees and below-minimum-balance fees that exceeded even those offered by fringe financial institutions. We also expected that language barriers would be a difficulty, because many recent immigrants only speak Spanish. We found out that most of the time there was someone on the bank staff that could speak Spanish, but that a lot of bank literature was in English only so they couldn't understand it. We ended our presentation with recommendations on what banks and other financial service providers could do to offer more consumer-friendly services. At the end we got feedback from a panel of expert "discussants" we had recruited in order to give us advice for how we should revise our thesis.

There were, however, a few hitches and embarrasing moments. Twice during the presentation, we referred to "cash checking" instead of "check cashing." Also, during our rehearsal, I discovered that during the process of "cleaning up" the slides, on one of the slides I made featuring a graph showing the racial composition of counties in the United States versus the number of banks per capita, that one of my teammates had replaced the phrase "non-Hispanic white" with "non-white Hispanic." Fortuntely we caught this error before it made it into our final presentation. Also, at the beginning of our presentation we included a video showing the sights and sounds of Langley Park. One of our discussants was Bill Hanna, a professor at UMCP who also runs several community organizations that focus on Langley Park, and he politely informed us that several of the shots in our video featured locations that weren't even in Langley Park.

However, overall, the experience was exciting and we learned a lot. Also, at the presentation, they were distributing pledge forms asking people to donate money to the Gemstone Program in order to make sure future generations of students have the same opportunities we did. If you are interested in donating to the Gemstone Program you can contact Jim Wallace.

And finally, this was the last day on the job for one of our team's mentors, Jerry Grossman (although he will still be coming to our meetings to advise our team for the next few weeks as we finalize our final thesis). Starting next week he will be working at the USAID (U.S. Agency for International Development) as an "economic growth officer." I imagine he will have his work cut out for him there.

(We have two mentors. Our other mentor is Brian Beard, whose area of expertise is on poverty assessment tools in developing countries.)

By the way, Mom and Dad, they will but putting out a DVD of our presentations at some point and I will send it to you when they do so you can see it. Also if you are interested in meeting our mentors or other team members I can see if that can be arranged when you are in town for graduation.)

Academics: Part 1 of 5: "Redundant Signaling"

Since I haven't had much to write about recently, I'm going to write a little bit about my classes. This is going to be a series of posts, one for each class.

This first one is about my class "Introduction to Signal Processing" with Dennis Healy.

This class is actually mostly about stuff I have already learned in previous classes, such as linear algebra. Another problem is that the first 15 minutes of each lecture simply repeats the last 15 minutes of the previous lecture. Finally, even during the middle of the lectures he tends to repeat things over, and over, and over again. A couple weeks ago we learned about the Nyquist sampling theorem, which states that a continuous periodic function can be completely characterized by a set of "samples" taken from the function at discrete points in time depending on the highest frequency in the period. The same thing applies to Healy's lectures: one could "sample" the lecture by only paying attention for a brief period every 5-10 minutes and writing what is on the slide, and one would not lose any information.

(Fortunately, my other classes are a lot more fun and exicintg, and I'll tell you about them in upcoming posts.)

SURGE!

I just received notification that the University of Illinois has awarded me the following fellowship:

http://engineering.illinois.edu/students/graduate/surge/

I count as a "person with disabilities" on that list.

The amazing thing is that I never applied for this fellowship, or even knew about it in advance. What happened is that the graduate admissions person at UIUC contacted my computer science advisor saying that there as a fellowship that I could likely get, and the advisor asked me to come in and sign a form giving Disability Support Services permission to release my records to them. I did that a couple weeks ago and just today I got the e-mail saying it had been awarded. (I don't know how the graduate admissions person knew that I was a "person with disabilities" - I don't recall writing it in my application materials. Probably one of my professors wrote something about it in her recommendation letter - good thing he/she did!)

DEEP PHILOSOPHICAL QUESTION: If being "disabled" gives you special opportunities that you wouldn't have had if you weren't "disabled," does it still count as a "disability"?