OOPSLA 01: Selected Papers I

Tue 10:30-12:00 pm - Rose Ballroom A
Efficient Modular Glass Box Software Model Checking
Michael Roberson, University of Michigan, United States
Chandrasekhar Boyapati, University of Michigan, United States
sponsorWei-Ngan Chin, National University of Singapore,

Glass box software model checking incorporates novel techniques to identify similarities in the state space of a model checker and safely prune large numbers of redundant states without explicitly checking them. It is significantly more efficient than other software model checking approaches for checking certain kinds of programs and program properties.

This paper presents Pipal, a system for modular glass box software model checking. Extending glass box software model checking to perform modular checking is important to further improve its scalability. Extending glass box software model checking to perform modular checking is nontrivial because unlike traditional software model checkers such as JPF and CMC, a glass box software model checker does not check every state separately—instead, it checks a large set of states together in each step. We present a solution and demonstrate Pipal's effectiveness on a variety of programs.

An Experiment About Static and Dynamic Type Systems
Stefan Hanenberg, University of Duisburg-Essen, Germany
sponsorTheo D'Hondt, Software Languages Lab, Vrije Universiteit Brussel, Belgium

Although static type systems are an essential part in teaching and research in software engineering and computer science, there is hardly any knowledge about what the impact of static type systems on the development time or the resulting quality for a piece of software is. On the one hand there are authors that state that static type systems decrease an application's complexity and hence its development time (which means that the quality must be improved since developers have more time left in their projects). On the other hand there are authors that argue that static type systems increase development time (and hence decrease the code quality) since they restrict developers to express themselves in a desired way. This paper presents an empirical study with 49 subjects that studies the impact of a static type system for the development of a parser over 27 hours working time. The study's result reveals that (under the conditions of the experiment) the existence of the type system has neither a positive nor a negative impact on the development time of an application.

A Simple Inductive Synthesis Methodology and its Applications
Shachar Itzhaky, Tel-Aviv University, Israel
Sumit Gulwani, Microsoft Research, United States
Neil Immerman, University of Massachusetts, United States
Mooly Sagiv, Tel-Aviv University, Israel
sponsorLenore Zuck, National Science Foundation, University of Illinois at Chicago,

Given a high-level specification and a low-level programming language, our goal is to automatically synthesize an asymptotically optimal program that meets the specification. In this paper, we present a new algorithm and methodology for inductive synthesis that allows us to do this.

We use Second Order logic as our generic high level specification logic. For our low-level languages we choose small application-specific logics that can be immediately translated into code that runs in expected linear time in the worst case.

We explain our methodology and provide examples of the synthesis of several graph classifiers, e.g, linear-time tests of whether the input graph is connected, acyclic, etc. In another set of applications we automatically derive many finite differencing expressions equivalent to ones that Paige built by hand in his thesis. Finally we describe directions for automatically combining such automatically generated building blocks to synthesize efficient code implementing more complicated specifications.

Key words: Transformational Programming, Finite Differencing, High Level Program, Inductive Synthesis

 

2009 Highlights

Gerard HolzmannGerard Holzmann discusses Spin, a design analyzer tool, and Scrub, a code review tool, used by Jet Propulsion Laboratory to analyze and fix the software used for critical solar system exploration missions.

Watch the video on InfoQ.

More Highlights