This post continues our ongoing series on young PL researchers who are about to start independent research positions in academia and research labs. This week, we feature Ravi Chugh, who is starting as an assistant professor at the University of Chicago in the Fall. Continue reading
Author Archives: Swarat Chaudhuri
Program verification in the undergraduate CS curriculum
[This is the first part of a two-post series. The second part is here.]
In previous posts on this blog, I have talked about how research on programming languages and tools can contribute to K-16 education. In this post, I will share with you some of my experiences while trying to use a PL tool — specifically, a semi-automated program verifier — in an undergraduate algorithms class. The experience was a success in many ways. A program verifier gives students a hands-on understanding of how algorithms are mathematical objects, and verification tools are now mature enough for productive classroom use. I think every CS program would benefit students by introducing them to these tools at some point. At the same time, the experience exposed me to some serious limitations of current-day program verification, and opened up a number of directions for new research in this area. Continue reading
Filed under Education, Formal verification
Spotlight: Aws Albarghouthi
Our “New Scientists on the Block” series features up-and-coming PL researchers who are about to begin independent research careers in universities or research laboratories. This week, we interview Aws Albarghouthi, who is starting as an assistant professor at the University of Wisconsin, Madison, in January 2015.
Continue reading
Filed under Interviews, New scientists
Programming language research for K-16 education (Part II)
In this post, I’ll continue our ongoing discussion of applications of PL research in computer-assisted education. Specifically, I’ll summarize a talk that Loris D’Antoni of Penn gave at this year’s Workshop on Programming Language Technology for Massive Open Online Courses (PLOOC). I was intrigued by this work, and I think a lot of you may be too.
Spotlight: Emina Torlak
From time to time, the PL Enthusiast will publish interviews of “new scientists on the block”: prominent PL researchers who are about to start, or just started, independent research careers in universities or research laboratories. This week, we feature Emina Torlak, who is starting as an assistant professor at the University of Washington in Fall 2014.
Filed under Interviews, New scientists
Programming language research for K-16 education
At the recent PLDI conference, Armando Solar-Lezama and I organized a workshop called PLOOC: “Programming Language Tools for Massive Open Online Courses.” The high-level goal of the workshop was to discuss ways in which tools coming out of PL research can be used in K-16 education. Over the years, PL researchers have developed many techniques for automating and simplifying the design and analysis of programs. For the most part, these techniques have targeted the professional programmer. However, techniques developed for industrial code can also be applied to student-written programs in computer science courses.
Radhia Cousot
Automated analysis of programs is one of the major success stories in PL. The goal here is to algorithmically infer properties of a program’s runtime behavior without executing the program on concrete inputs. This may be done for many reasons, including optimization and reasoning about correctness. If you are trying to optimize a program, it helps to know that a statement executed within a loop always performs the same update, and can therefore be moved out of the loop. If you want to be certain that your C program doesn’t have buffer overflows, you want to infer bounds on the indices used for array accesses in the program.
Over the years, systems for program analysis have increased in sophistication and entered the mainstream of software development. But how do you know that what your analysis tells you is correct? To be certain that it is, we must relate the program’s semantics – what the program does at runtime – to what the analysis algorithm computes. The framework of abstract interpretation is the gold standard for doing so.
Radhia Cousot, co-inventor of abstract interpretation, passed away earlier this summer after a long struggle with cancer. While her death was tragic, I am consoled that she lived to see her work impact the world in a way that most researchers can only dream of.
Filed under Abstract interpretation, Formal verification