Research Publications

Protocol Checking

• Language Support for Fast and Reliable Message-based Communication in Singularity OS Manuel Fähndrich, et. al. in Eurosys2006, Leuven, Belgium.
  Available in pdf.

  Abstract €

  Message-based communication offers the potential benefits of providing stronger specification and cleaner separation between components. Compared with shared-memory interactions, message passing has the potential disadvantages of more expensive data exchange (no direct sharing) and more complicated programming.
  
  In this paper we report on the language, verification, and run-time system features that make messages practical as the sole means of communication between processes in the Singularity operating system. We show that using advanced programming language and verification techniques, it is possible to provide and enforce strong system-wide invariants that enable efficient communication and low-overhead software-based process isolation. Furthermore, specifications on communication channels help in detecting programmer mistakes early---namely at compile-time---thereby reducing the difficulty of the message-based programming model.
  
  The paper describes our communication invariants, the language and verification features that support them, as well as implementation details of the infrastructure. A number of benchmarks show the competitiveness of this approach.
   

• Static Deadlock Prevention in Dynamically Configured Communication Networks Manuel Fähndrich and Jakob Rehof and Sriram Rajamani, submitted
  Available in pdf.

  Abstract €

  We propose a modular verification technique that guarantees the absence of deadlocks in a system of communicating processes. The network model is very general. It supports dynamic process and channel creation and the ability to send channel endpoints over channels, thereby allowing arbitrary dynamically configured networks.

  The technique is based on statically approximating all potential wait cycles that could arise at runtime. The potential cycle information is computed from the local perspective of each process, leading to a modular analysis.

  We prove the soundness of the analysis (namely dead-lock freedom) on a simple but realistic language that captures the essence of such communication networks. We also describe how the technique can be applied to a substantial example.

• Typestates for Objects Manuel Fähndrich and Robert DeLine, Proceedings of European Symposium on Object Oriented Programming, Oslo, Norway, 2004
  Available in pdf.

  Abstract €

  Today's mainstream object-oriented compilers and tools do not support declaring and statically checking simple pre- and postconditions on methods and invariants on object representations. The main technical problem preventing static verification is reasoning about the sharing relationships among objects as well as where object invariants should hold. We have developed a programming model of typestates for objects with a sound modular checking algorithm. The programming model handles typical aspects of object-oriented programs such as down-casting, virtual dispatch, direct calls, and subclassing. The model also permits subclasses to extend the interpretation of typestates and to introduce additional typestates. We handle aliasing by adapting our previous work on practical linear types developed in the context of the Vault system. We have implemented these ideas in a tool called Fugue for specifying and checking typestates on Microsoft .NET-based programs.

• Heap Monotonic Typestate Manuel Fähndrich and Rustan Leino, Proceedings of the first international workshop on alias confinement and ownership (IWACO 03), colocated with ECOOP 03, Darmstadt, Germany, July 2003, Available in pdf.

  Abstract €

  The paper defines the class of heap monotonic typestates. The monotonicity of such typestates enables sound checking algorithms without the need for non-aliasing regimes of pointers. The basic idea is that data structures evolve over time in a manner that only makes their
  representation invariants grow stronger, never weaker. This assumption guarantees that existing object references with particular typestates remain valid in all program futures, while still allowing objects to attain new stronger typestates. The system is powerful enough to establish properties of circular data structures.

• The Fugue Protocol Checker: Is your software Baroque? Robert DeLine and Manuel Fähndrich, MSR-TR-2004-07, Available in pdf

  Abstract €

  Even in a safe programming language, such as C# or Java, disobeying the rules for using an interface can cause exceptions at run time. Such rules govern how system resources are managed, the order of method calls, and the formatting of string parameters, such as SQL queries and XML element tags. This paper introduces the Fugue protocol checker that allows the rules for using an interface to be recorded as declarative specifications in an existing language. Fugue provides a range of annotations that allow a developer to specify interface rule with varying precision. At the simplest end of the range, a specifier can mark those methods that allocate and release resources. A specifier can also limit the order in which an object's methods may be called to the transitions of a finite state machine.
  
  At the most complex end of the range, a specifier can give a method a plug-in pre- and postconditon, which is arbitrary code that examines an object's current state and a static approximation of the method's actuals, decides whether the call is legal and returns the object's state after the call. We used these features to specify rules for using the ado.net library for accessing relational databases, and found several errors in an internal Microsoft Research web site, which extensively uses this library.

  
   

• Adoption and Focus: Practical Linear Types for Imperative Programming Manuel Fähndrich and Robert DeLine, Proceedings of the ACM Conference on Programming Language Design and Implementation, Berlin, June 2002, Available in pdf

  Abstract €

  A type system with linearity is useful for checking software protocols
  and resource management at compile time. Linearity provides powerful
  reasoning about state changes, but at the price of restrictions on
  aliasing. The hard division between linear and nonlinear types forces
  the programmer to make a trade-off between checking a protocol on an
  object and aliasing the object. Most onerous is the restriction that
  any type with a linear component must itself be linear. Because of
  this, checking a protocol on a object imposes aliasing restrictions on
  any data structure that directly or indirectly points to the object.
  We propose a new type system that reduces these restrictions with the
  adoption and focus constructs. Adoption safely allows a programmer to
  alias objects on which she is checking protocols, and focus allows the
  reverse. A programmer can alias data structures that point to linear
  objects and use focus for safe access to those objects. We discuss how
  we implemented these ideas in the Vault programming language.
  
  
   

• Enforcing High-Level Protocols in Low-Level Software Robert DeLine and Manuel Fähndrich, Proceedings of the ACM Conference on Programming Language Design and Implementation, Snowbird, June 2001 Available in pdf

  Abstract €

  The reliability of infrastructure software, such as operating
  systems and web servers, is often hampered by the mismanagement of
  resources, such as memory and network connections. The Vault
  programming language allows a programmer to describe resource
  management protocols that the compiler can statically enforce. Such
  a protocol can specify that operations must be performed in a
  certain order and that certain operations must be performed before
  accessing a given data object. Furthermore, Vault enforces
  statically that resources cannot be leaked. We validate the utility
  of our approach by enforcing protocols present in the interface
  between the Windows 2000 kernel and its device drivers.
  
   

   

Type Systems

• Declaring and Checking Non-Null Types in an Object-Oriented Language Manuel Fähndrich and Rustan Leino, Proceedings of the 18th ACM Conference on Object-Oriented Programming Systems, Languages, and Applications, Anaheim, CA, October 2003, Available in pdf

  Abstract €

  Distinguishing non-null references from possibly null references at
  the type level can detect null-related errors in object-oriented
  programs at compile-time. This paper gives a proposal for
  retrofitting a language such as C# or Java with non-null
  types. It addresses the central complications that arise in
  constructors, where declared non-null fields may not yet have been
  initialized, but the partially constructed object is already
  accessible. The paper reports experience with an implementation
  for annotating and checking null-related properties in C# programs.

• A Theory of Type Qualifiers. Jeffrey S. Foster, Manuel Fähndrich, and Alexander Aiken. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'99). Atlanta, Georgia. May 1999. gzipped PostScript.

• Refined Type Inference for ML Manuel Fähndrich and Alexander Aiken, First Workshop on Types in Compilation (TIC'97), Amsterdam, June 1997
  This is a 3 page summary of the SAS'97 paper. Available in ps.gz and dvi.gz

• Dynamic Typing and Subtype Inference Alexander Aiken and Manuel Fähndrich, Proceedings of the ACM Conference on Functional Programming and Computer Architecture, San Diego, June 1995 Available in ps.gz and dvi.gz

  Abstract €

  Dynamic typing is a program analysis targeted at removing runtime tagging and untagging operations from programs written in dynamically typed languages. This paper compares dynamic typing with a subtyping system based on set constraints. The purpose is both to make precise the relationship between two superficially unrelated type systems and to illustrate how the advantages of dynamic typing and subtype inference can be combined. The central result is a theorem showing that a typing discipline at least as powerful as dynamic typing can be expressed using set constraints.

   

Flow Analysis

• Type-Based Flow Analysis: From Polymorphic Subtyping to CFL-Reachability. Manuel Fähndrich, Jakob Rehof, In POPL 01: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Postscript

• Scalable Context-Sensitive Flow Analysis Using Instantiation Constraints, Manuel Fahndrich, Jakob Rehof, and Manuvir Das, PLDI '00: Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, Vancouver, BC, Canada, June 2000. Corrected Version

• From Polymorphic Subtyping to CFL Reachability: Context-Sensitive Flow Analysis Using Instantiation Constraints. Manuel Fähndrich, Jakob Rehof, Manuvir Das. Microsoft Research Technical Report MSR-TR-99-84. Postscript

BANE

• Detecting Races in Relay Ladder Logic Programs. Alexander Aiken, Manuel Fähndrich, and Zhendong Su. To appear in the Springer International Journal on Software tools for Technology Transfer (STTT), Springer Verlag. 2000. Note: This is an extended and refined version of the TACAS'98 paper below.

• Projection Merging: Reducing Redundancies in Inclusion Constraint Graphs. Zhendong Su, Manuel Fähndrich, and Alexander Aiken. In Proceedings of the 27^th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'00). Boston, MA. January 2000. PostScript.

• Partial Online Cycle Elimination in Inclusion Constraint Graphs Manuel Fähndrich, Alexander Aiken, Jeffrey S. Foster, and Zhendong Su, Proceedings of the 1998 Conference on Programming Languages Design and Implementation, Montreal, June 1998, available in Postscript

  Abstract €

  Many program analyses are naturally formulated and implemented using inclusion constraints. We present new results on the scalable implementation of such analyses based on two insights: first, that online elimination of cyclic constraints yields orders-of-magnitude improvements in analysis time for large problems; second, that the choice of constraint representation affects the quality and efficiency of partial online cycle elimination. We present an analytical model that explains our design choices and show that the model's predictions match well with results from a large experiment.
   

• A Toolkit for Constructing Type- and Constraint-Based Program Analyses Alexander Aiken, Manuel Fähndrich, Jeffrey S. Foster, and Zhendong Su, Proceedings of the Second International Workshop on Types in Compilation, Kyoto, Japan, March 1998, Springer LNCS 1473.  

  Abstract €

  BANE (The Berkeley Analysis Engine) is a publicly available toolkit for constructing type- and constraint-based program analyses. We describe the goals of the project, the rationale for BANE's overall design, some examples coded in BANE, and briefly compare BANE with other program analysis frameworks.
   

• Detecting Races in Relay Ladder Logic Programs Alexander Aiken, Manuel Fähndrich, and Zhendong Su, Proceedings of the 1st Conference on Tools and Algorithms for the Analysis and Construction of Systems, Lisbon Portugal, March 1998, available in Postscript
  

  Abstract €

  Relay Ladder Logic (RLL) is a programming language widely used for complex embedded control applications such as manufacturing and amusement park rides. The cost of bugs in RLL programs is extremely high, often measured in millions of dollars (for shutting down a factory) or human safety (for rides). In this paper, we describe our experience in applying constraint-based program analysis techniques to analyze production RLL programs. Our approach is an interesting combination of probabilistic testing and program analysis, and we show that our system is able to detect bugs with high probability, up to the approximations made by the conservative program analysis. We demonstrate that our analysis is useful in detecting some flaws in production RLL programs that are difficult to find by other techniques.
   

• Tracking down Exceptions in Standard ML Programs Manuel Fähndrich, Jeffrey S. Foster, and Alexander Aiken, UCB Computer Science Tech Report 97-996, February 1998, Available in Postscript
  

  Abstract €

  We describe our experiences with an exception analysis tool for Standard ML. Information about exceptions gathered by the analysis is visualized using PAM, a program visualization tool for Emacs. We study the results of the analysis of three well-known programs, classifying exceptions as assertion failures, error exceptions, control-flow exceptions, and pervasive exceptions. Even though the analysis is often conservative and reports many spurious exceptions, we have found it useful for checking the consistency of control-flow exceptions. Furthermore, using our tools, we have uncovered two minor exception-related bugs in the three programs we scrutinized.
  

• Program Analysis Using Mixed Term and Set Constraints Manuel Fähndrich and Alexander Aiken, Proceedings of the 1997 Static Analysis Symposium (SAS'97), Paris, September 1997, Available in ps.gz and dvi.gz
  

  Abstract €

  There is a tension in program analysis between precision and efficiency. In constraint-based program analysis, at one extreme methods based on unification of equality constraints over terms are very fast but often imprecise. At the other extreme, methods based on the resolution of inclusion constraints over set expressions are quite precise, but are often inefficient in practice. We describe a parameterized framework for constraint-based program analyses that allows the analysis designer to embed terms and set expressions within each other. Constraints over these mixed expressions are partially between equality and inclusion, which enables an entire spectrum of program analyses with varying degrees of precision and efficiency to be expressed. We also show that there are interesting analyses that take advantage of this mixture. In particular, we report on the design and implementation of an uncaught exception analysis for core ML. Our results show that the analysis approaches the efficiency of algorithm W.
   

• Making Set-Constraint Based Program Analyses Scale Manuel Fähndrich and Alexander Aiken, Computer Science Division Tech Report 96-917, University of California at Berkeley, September 1996. This work was also presented at the Workshop on Set Constraints, Cambridge MA, August 96 Available in ps.gz and dvi.gz

Thesis

• BANE: A Library for Scalable Constraint-Based Program Analysis. Manuel Fähndrich, Ph.D. Dissertation, University of California at Berkeley, May 1999. Available in pdf

Miscellaneous

• Statically Checkable Pattern Abstractions, Manuel Fähndrich and John Boyland, Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP'97), Amsterdam, June 1997, Available in ps.gz and dvi.gz
  
  Abstract €

  Pattern abstractions increase the expressiveness of pattern matching, enabling the programmer to describe a broader class of regular forests with patterns. Furthermore, pattern abstractions support code reuse and code factoring, features that facilitate maintenance and evolution of code. Past research on pattern abstractions has generally ignored the aspect of compile-time checks for exhaustiveness and redundancy. In this paper we propose a class of expressive patterns that admits these compile-time checks.
   

• Better Static Memory Management: Improving Region-Based Analysis of Higher-Order Languages Alexander Aiken, Manuel Fähndrich, Raph Levien, Proceedings of the ACM Conference on Programming Languages, Design and Implementation, San Diego, June 1995
  Available in ps.gz and dvi.gz
  

  Abstract €

  Static memory management replaces runtime garbage collection with compile-time annotations that make all memory allocation and deallocation explicit in the program. We improve upon the Tofte/Talpin region-based scheme for compile-time memory management [TT94]. In the Tofte/Talpin approach, all values, including closures, are stored in regions. Region lifetimes coincide with lexical scope, thus forming a runtime stack of regions and eliminating the need for garbage collection. We relax the requirement that region lifetimes be lexical. Rather, regions are allocated late and deallocated as early as possible by explicit memory operations. The placement of allocation and deallocation annotations is determined by solving a system of constraints that expresses all possible annotations. Experiments show that our approach reduces memory requirements significantly, in some cases asymptotically.

• Better Static Memory Management: Improving Region-Based Analysis of Higher-Order Languages Alexander Aiken, Manuel Fähndrich, Raph Levien, Computer Science Division Tech Report 95-866, University of California, April 1995

  This report is an extended version of the PLDI paper. Available in ps.gz and dvi.gz