Publications

    2013

    • Sebastian Burckhardt, Manuel Fahndrich, Peli de Halleux, Jun Kato, Sean McDirmid, Michal Moskal, and Nikolai Tillmann, It's Alive! Continuous Feedback in UI Programming, in PLDI, ACM SIGPLAN, June 2013
      Live programming allows programmers to edit the code of a running program and immediately see the effect of the code changes. This tightening of the traditional edit-compile-run cycle reduces the cognitive gap between program code and behavior, improving the learning experience of beginning programmers while boosting the productivity of seasoned ones. Unfortunately, live programming is difficult to realize in practice as imperative languages lack well-defined abstraction boundaries that make live programming responsive or its feedback comprehensible. This paper enables live programming for user interface programming by cleanly separating the rendering and non-rendering aspects of a UI program, allowing the display to be refreshed on a code change without restarting the program. A type and effect system formalizes this separation and provides an evaluation model that incorporates the code update step. By putting live programming on a more formal footing, we hope to enable critical and technical discussion of live programming systems.
    • Manuel Fahndrich and Francesco Logozzo, Proceedings of the 20th Static Analysis Symposium, Springer Verlag, June 2013
      Static analysis is increasingly recognized as a fundamental tool for program verification, bug detection, compiler optimization, program understanding, and software maintenance. The series of Static Analysis Symposia has served as the primary venue for the presentation of theoretical, practical, and application advances in the area. This year's symposium, the 20th International Static Analysis Symposium (SAS 2013), was held on June 19-21, 2013, in Seattle and co-located with ACM's PLDI Conference. Three workshops were affiliated with SAS 2013: NSAD 2013 (The 5th Workshop on Numerical and Symbolic Abstract Domains) on June 19th, SASB 2013 (The 4th Workshop on Static Analysis and Systems Biology) on June 19th, and TAPAS 2013 (The 4th Workshop on Tools for Automatic Program Analysis) on June 19th. We received 78 abstract and in the end 56 complete paper submissions. Each submission was reviewed on average by 3.2 program committee members. The committee decided to accept 23 papers. This year, for the first time, SAS invited the submission of virtual machine artifacts in support of submitted papers. We received 22 such VMs. Out of the 23 accepted papers, 11 have associated VMs. During the review process we used the VMs only in order to lend additional support to papers, not to detract from their acceptance. The VMs are archived on http://staticanalysis.org/ as a scientific record of the state of the art at this point in time and they will hopefully serve as a comparison base for future research. We were able to secure three invited talks by Eric Lippert (Coverity) on "The Psychology of C# Analysis", Eric Goubault (CEA) on "Static Analysis by Abstract Interpretation of Numerical Programs and Systems, and FLUCTUAT", and Sriram Sankaranarayanan (University of Colorado) on "Static analysis in the continuously changing world". We would like to thank the program committee and all the external reviewers for their participation in the reviewing process. We are grateful for the generous sponsorship by Microsoft Research. Our thanks go out to David Schmidt and Hans Boehm for organizing the co-location with PLDI, to Manuel Hermenegildo for help with hosting the VMs, and to the EasyChair team for the use of their very handy system.
    • Michael Barnett, Mehdi Bouaziz, Manuel Fahndrich, and Francesco Logozzo, A case for static analyzers in the cloud, in Bytecode 2013, , March 2013
      A cloud-based static analyzer runs as service. Clients issue analysis requests through the local network or over the internet. The analysis takes advantage of the large computation resources offered by the cloud: the underlying infrastructure ensures scaling and unlimited storage. Cloud-based analyzers may relax performance-precision trade-offs usually associated with desktop-based analyzers. More cores enable more precise and responsive analyses. More storage enables perfect caching of the analysis results, shareable among different clients, and queryable off-line. To realize these advantages, cloud-based analyzers need to be architected differently than desktop ones. We describe our ongoing effort of moving a desktop analyzer, Clousot, into a cloud-based one, Cloudot.
    • Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Francesco Logozzo, Automatic Inference of Necessary Preconditions, in in Proceedings of the 14th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'13), Springer Verlag, January 2013
      We consider the problem of automatic precondition inference. We argue that the common notion of sufficient precondition inference (i.e., under which precondition is the program correct?) imposes too large a burden on callers, and hence it is unfit for automatic program analysis. Therefore, we define the problem of necessary precondition inference (i.e., under which precondition, if violated, will the program always be incorrect?). We designed and implemented several new abstract interpretation-based analyses to infer atomic, disjunctive, universally and existentially quantified necessary preconditions. We experimentally validated the analyses on large scale industrial code. For unannotated code, the inference algorithms find necessary preconditions for almost 64% of methods which contained warnings. In 27% of these cases the inferred preconditions were also sufficient, meaning all warnings within the method body disappeared. For annotated code, the inference algorithms find necessary preconditions for over 68% of methods with warnings. In almost 50% of these cases the preconditions were also sufficient. Overall, the precision improvement obtained by precondition inference (counted as the additional number of methods with no warnings) ranged between 9% and 21%.

    2012

    • Mehdi Bouaziz, Francesco Logozzo, and Manuel Fahndrich, Inference of Necessary Field Conditions with Abstract Interpretation , in 10th Asian Symposium on Programming Languages and Systems (APLAS 2012), Springer, December 2012
      We present a new static analysis to infer necessary field conditions for object-oriented programs. A necessary field condition is a property that should hold on the fields of a given object, for otherwise there exists a calling context leading to a failure due to bad object state. Our analysis also infers the provenance of the necessary condition, so that if a necessary field condition is violated then an explanation containing the sequence of method calls leading to a failing assertion can be produced. When the analysis is restricted to readonly fields, i.e., fields that can only be set in the initialization phase of an object, it infers object invariants. We provide empirical evidence on the usefulness of necessary field conditions by integrating the analysis into cccheck, our static analyzer for .NET. Robust inference of readonly object field invariants was the #1 request from cccheck users.
    • Nikolai Tillmann, Michal Moskal, Jonathan de Halleux, Manuel Fahndrich, and Sebastian Burckhardt, TouchDevelop — App Development on Mobile Devices, in Proc. 20th International Symposium on Foundations of Software Engineering (FSE 2012), Demonstration, ACM, November 2012
      Mobile devices are becoming the prevalent computing platform for most people. TouchDevelop is a new mobile development environment that enables anyone with a Windows Phone to create new apps directly on the smartphone, without a PC or a traditional keyboard. At the core is a new mobile programming language and editor that was designed with the touchscreen as the only input device in mind. Programs written in TouchDevelop can leverage all phone sensors such as GPS, cameras, accelerometer, gyroscope, and stored personal data such as contacts, songs, pictures. Thousands of programs have already been written and published with TouchDevelop.
    • Francesco Logozzo, Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Mike Barnett, A Semantic Integrated Development Environment, in Companion of the Proceedings of the to the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2012), ACM SIGPLAN, October 2012
      We present SIDE, a Semantic Integrated Development Environment. SIDE uses static analysis to enrich existing IDE features and also adds new features. It augments the way existing compilers find syntactic errors - in real time, as the programmer is writing code without execution - by also finding semantic errors, \emph{e.g.}, arithmetic expressions that may overflow. If it finds an error, it suggests a repair in the form of code - e.g., providing an equivalent yet non-overflowing expression. Repairs are correct by construction. SIDE also enhances code refactoring (by suggesting precise yet general contracts), code review (by answering what-if questions), and code searching (by answering questions like ``find all the callers where x < y''). SIDE is built on the top of CodeContracts and the Roslyn CTP. CodeContracts provide a lightweight and programmer-friendly specification language. SIDE uses the CodeContracts static checker (based on Abstract Interpretation) to obtain a deep semantic understanding of what the program does.
    • Sebastian Burckhardt, Manuel Fahndrich, Daan Leijen, and Benjamin P. Wood, Cloud Types for Eventual Consistency, in Proceedings of the 26th European Conference on Object-Oriented Programming (ECOOP), Springer, 15 June 2012
      Mobile devices commonly access shared data stored on a server. To ensure responsiveness, many applications maintain local replicas of the shared data that remain instantly accessible even if the server is slow or temporarily unavailable. Despite its apparent simplicity and commonality, this scenario can be surprisingly challenging. In particular, a correct and reliable implementation of the communication protocol and the conflict resolution to achieve eventual consistency is daunting even for experts. To make eventual consistency more programmable, we propose the use of specialized cloud data types. These cloud types provide eventually consistent storage at the programming language level, and thus abstract the numerous implementation details (servers, networks, caches, protocols). We demonstrate (1) how cloud types enable simple programs to use eventually consistent storage without introducing undue complexity, and (2) how to provide cloud types using a system and protocol comprised of multiple servers and clients.
    • Manuel Fahndrich, Michael Barnett, Daan Leijen, and Francesco Logozzo, Integrating a Set of Contract Checking Tools into Visual Studio, in Proceedings of the 2012 Second International Workshop on Developing Tools as Plug-ins (TOPI 2012), IEEE, 3 June 2012
      Integrating tools and extensions into existing languages, compilers, debuggers, and IDEs can be difficult, workintensive, and often results in a one-off integration. In this paper, we report on our experience of building and integrating the CodeContract tool set into an existing programming environment. The CodeContract tools enable 1) authoring of contracts (preconditions, postconditions, and object invariants), 2) instrumenting contract checks into code, 3) statically checking code against contracts, and 4) visualizing contracts and results. We identify three characteristics of our integration that allowed us to reuse existing compilers and IDEs, increase the reach of our tools to multiple languages and target platforms, and maintain the tools over three consecutive versions of C# and Visual Studio with little effort. These principles are 1) use source embedding for new language features, 2) use target analysis and rewriting, and 3) use generic plug-ins to isolate tools from the IDE.
    • Sebastian Burckhardt, Manuel Fahndrich, Daan Leijen, and Mooly Sagiv, Eventually Consistent Transactions, in Proceedings of the 22n European Symposium on Programming (ESOP), Springer, 24 March 2012
      When distributed clients query or update shared data, eventual consistency can provide better availability than strong consistency models. However, programming and implementing such systems can be difficult unless we establish a reasonable consistency model, i.e. some minimal guarantees that programmers can understand and systems can provide effectively. To this end, we propose a novel consistency model based on eventually consistent transactions. Unlike serializable transactions, eventually consistent transactions are ordered by two order relations (visibility and arbitration) rather than a single order relation. To demonstrate that eventually consistent transactions can be effectively implemented, we establish a handful of simple operational rules for managing replicas, versions and updates, based on graphs called revision diagrams. We prove that these rules are sufficient to guarantee correct implementation of eventually consistent transactions. Finally, we present two operational models (single server and server pool) of systems that provide eventually consistent transactions.

    2011

    • Sebastian Burckhardt, Manuel Fahndrich, Daan Leijen, and Mooly Sagiv, Eventually Consistent Transactions (full version), no. MSR-TR-2011-117, October 2011
      When distributed clients query or update shared data, eventual consistency can provide better availability than strong consistency models. However, programming and implementing such systems can be difficult unless we establish a reasonable consistency model, i.e. some minimal guarantees that programmers can understand and systems can provide effectively. To this end, we propose a novel consistency model based on eventually consistent transactions. Unlike serializable transactions, eventually consistent transactions are ordered by two order relations (visibility and arbitration) rather than a single order relation. To demonstrate that eventually consistent transactions can be effectively implemented, we establish a handful of simple operational rules for managing replicas, versions and updates, based on graphs called revision diagrams. We prove that these rules are sufficient to guarantee correct implementation of eventually consistent transactions. Finally, we present two operational models (single server and server pool) of systems that provide eventually consistent transactions.
    • Marat Akhin, Nikolai Tillmann, Manuel Fahndrich, Jonathan de Halleux, and Michal Moskal, Code Similarity in TouchDevelop: Harnessing Clones, no. MSR-TR-2011-103, 9 September 2011
      The number of applications available in mobile marketplaces is increasing rapidly. It's very easy to become overwhelmed by the sheer size of their codebase. We propose to use code clone analysis to help manage existing applications and develop new ones. First, we propose an automatic application ranking scheme based on (dis)similarity. Traditionally, applications in app stores are ranked manually, by user or moderator input. We argue that automatically computed (dis)similarity information can be used to reinforce this ranking and help in dealing with possible application cloning. Second, we consider code snippet search, a task commonly performed by application developers. We view it as a special instance of the clone detection problem which allows us to perform precise search with little to no configuration and completely agnostic of code formatting, variable renamings, etc. We built a prototype of our approach in TouchDevelop, a novel application development environment for Windows Phone, and will use it as a testing ground for future evaluation.
    • Manuel Fahndrich and Francesco Logozzo, Checking Compatibility of Bit Sizes in Floating Point Comparison Operations, in Proceedings of the 3rd workshop on Numerical and Symbolic Abstract Domains, Electronic Proceedings in Theoretical Computer Science, September 2011
      We motivate, define and design a simple static analysis to check that comparisons of floating point values use compatible bit widths and thus compatible precision ranges. Precision mismatches arise due to the difference in bit widths of processor internal floating point registers (typically 80 or 64 bits) and their corresponding widths when stored in memory (64 or 32 bits). The analysis gurantees that floating point values from memory (i.e. array elements, instance and static fields) are not compared against floating point numbers in registers (i.e. arguments or locals). Without such an analysis, static symbolic verification is unsound and hence may report false negatives. The static analysis is fully implemented in Clousot, our static contract checker based on abstract interpretation.
    • Xusheng Xiao, Nikolai Tillmann, Manuel Fahndrich, Peli de Halleux, and Michal Moskal, Transparent Privacy Control via Static Information Flow Analysis, no. MSR-TR-2011-93, 2 August 2011
      A common problem faced by modern mobile-device platforms is that third-party applications in the marketplace may leak private information without notifying users. Existing approaches adopted by these platforms provide little information on what applications will do with the private information, failing to effectively assist users in deciding whether to install applications and in controlling their privacy. To address this problem, we propose a transparent privacy control approach, where an automatic static analysis reveals to the user how private information is used inside an application. This flow information provides users with better insights, enabling them to determine when to use anonymized instead of real information, or to force script termination when scripts access private information. To further reduce the user burden in controlling privacy, our approach provides a default setting based on an extended information flow analysis that tracks whether private information is obscured before escaping through output channels. We built our approach into TouchDevelop, a novel application-creation environment that allows users to write application scripts on mobile devices, share them in a web bazaar, and install scripts published by other users. To evaluate our approach, we plan to study a portion of published scripts in order to evaluate the effectiveness and performance of information flow analysis. We also plan to carry out a user survey to evaluate the usability of our privacy control and guide our future design.
    • Daan Leijen, Sebastian Burckhardt, and Manuel Fahndrich, Prettier Concurrency: Purely Functional Concurrent Revisions, in Haskell Symposium 2011 (Haskell'11), ACM SIGPLAN, Tokyo, Japan, 7 July 2011
      This article presents an extension to the work of Launchbury and Peyton-Jones on the ST monad. Using a novel model for concurrency, called "concurrent revisions", we show how we can use concurrency together with imperative mutable variables, while still being able to safely convert such computations (in the Rev monad) into pure values again. In contrast to many other transaction models, like software transactional memory (STM), concurrent revisions never use rollback and always deterministically resolve conflicts. As a consequence, concurrent revisions integrate well with side-effecting I/O operations. Using deterministic conflict resolution, concurrent revisions can deal well with situations where there are many conflicts between different threads that modify a shared data structure. We demonstrate this by describing a concurrent game with conflicting concurrent tasks.
    • Mike Barnett, Manuel Fahndrich, K. Rustan M. Leino, Peter Mueller, Wolfram Schulte, and Herman Venter, Specification and Verification: The Spec# Experience, in Communications of the ACM, vol. 54, no. 6, pp. 81--91, Association for Computing Machinery, Inc., June 2011
    • Nikolai Tillmann, Michal Moskal, Jonathan de Halleux, and Manuel Fahndrich, TouchDevelop - Programming Cloud-Connected Mobile Devices via Touchscreen, no. MSR-TR-2011-49, 15 April 2011
      The world is experiencing a technology shift. In 2011, more touchscreen-based mobile devices like smartphones and tablets will be sold than desktops, laptops, and netbooks combined. In fact, in many cases incredibly powerful and easy-to-use smart phones are going to be the first and, in less developed countries, possibly the only computing devices which virtually all people will own, and carry with them at all times. Furthermore, mobile devices do not only have touchscreens, but they are also equipped with a multitude of sensors, such as location information and acceleration, and they are always connected to the cloud. TouchDevelop is a novel application creation environment for anyone to script their smartphones anywhere -- you do not need a separate PC. TouchDevelop allows you to develop mobile device applications that can access your data, your media, your sensors and allows using cloud services including storage, computing, and social networks. TouchDevelop targets students, and hobbyists, not necessarily the professional developer. Typical TouchDevelop applications are written for fun, or for personalizing the phone. TouchDevelop's typed, structured programming language is built around the idea of only using a touchscreen as the input device to author code. It has built-in primitives which make it easy to access the rich sensor data available on a mobile device. In our vision, the state of the program is automatically distributed between mobile clients and the cloud, with automatic synchronization of data and execution between clients and cloud, liberating the programmer from worrying (or even having to know about) the details. We report on our experience with our first prototype implementation for the Windows Phone 7 platform, which already realizes a large portion of our vision. It is available on the Windows Phone Marketplace.
    • Sebastian Burckhardt, Daan Leijen, and Manuel Fahndrich, Roll Forward, Not Back: A Case for Deterministic Conflict Resolution, in The 2nd Workshop on Determinism and Correctness in Parallel Programming (WODET'11), Newbeach, California, March 2011
      Enabling applications to execute various tasks in parallel is difficult if those tasks exhibit read and write conflicts. In recent work, we developed a programming model based on concurrent revisions that addresses this challenge: each forked task gets a conceptual copy of all locations that are declared to be shared. Each such location has a specific isolation type; on joins, state changes to each location are merged deterministically based on its isolation type. In this paper, we study how to specify isolation types abstractly using operation-based compensation functions rather than state based merge functions. Using several examples including a list with insert, delete and modify operations, we propose compensation tables as a concise, general and intuitively accessible mechanism for determining how to merge arbitrary operation sequences. Finally, we provide sufficient conditions to verify that a state-based merge function correctly implements a compensation table.
    • Nikolai Tillmann, Michal Moskal, Jonathan de Halleux, and Manuel Fahndrich, TouchDevelop: programming cloud-connected mobile devices via touchscreen, in Proceedings of the 10th SIGPLAN symposium on New ideas, new paradigms, and reflections on programming and software, ACM, New York, NY, USA, 2011

    2010

    • Manuel Fahndrich and Francesco Logozzo, Static contract checking with Abstract Interpretation, in Proceedings of the Conference on Formal Verification of Object-oriented Software (FoVeOOS 2010) , Springer Verlag, October 2010
      We present an overview of Clousot, our current tool to statically check CodeContracts. CodeContracts enable a compiler and language-independent specification of Contracts (precondition, postconditions and object invariants). Clousot checks every method in isolation using an assume/guarantee reasoning: For each method under analysis Clousot assumes its precondition and asserts the postcondition. For each invoked method, Clousot asserts its precondition and assumes the postcondition. Clousot also checks the absence of common runtime errors, such as null-pointer errors, buffer or array overruns, divisions by zero, as well as less common ones such as checked integer overflows or floating point precision mismatches in comparisons. At the core of Clousot there is an abstract interpretation engine which infers program facts. Facts are used to discharge the assertions. The use of abstract interpretation (vs usual weakest precondition-based checkers) has two main advantages: (i) the checker automatically infers loop invariants letting the user focus only on boundary specifications; (ii) the checker is deterministic in its behavior (which abstractly mimics the flow of the program) and it can be tuned for precision and cost. Clousot embodies other techniques, such as iterative domain refinement, goal-directed backward propagation, precondition and postcondition inference, and message prioritization.
    • Manuel Fahndrich, Static Verification for Code Contracts, in SAS'10 Proceedings of the 17th international conference on Static analysis , Springer Verlag, September 2010
      The Code Contracts project at Microsoft Research enables programmers on the .NET platform to author specifications in existing languages such as C# and VisualBasic. To take advantage of these specifications, we provide tools for documentation generation, runtime contract checking, and static contract verification. This talk details the overall approach of the static contract checker and examines where and how we trade-off soundness in order to obtain a practical tool that works on a full- edged object-oriented intermediate language such as the .NET Common Intermediate Language.
    • Michael Bebenita, Florian Brandner, Manuel Fahndrich, Francesco Logozzo, Wolfram Schulte, Nikolai Tillmann, and Herman Venter, SPUR: A Trace-Based JIT Compiler for CIL, no. MSR-TR-2010-27, 25 March 2010
      Tracing just-in-time compilers (TJITs) determine frequently executed traces (hot paths and loops) in running programs and focus their optimization effort by emitting optimized machine code specialized to these traces. Prior work has established this strategy to be especially beneficial for dynamic languages such as JavaScript, where the TJIT interfaces with the interpreter and produces machine code from the JavaScript trace. This direct coupling with a JavaScript interpreter makes it difficult to harness the power of a TJIT for other components that are not written in JavaScript, e.g., the DOM mplementation or the layout engine inside a browser. Furthermore, if a TJIT is tied to a particular high-level language interpreter, it is difficult to reuse it for other input languages as the optimizations are likely targeted at specific idioms of the source language. To address these issues, we designed and implemented a TJIT for Microsoft’s Common Intermediate Language CIL (the target language of C#, VisualBasic, F#, and many other languages). Working on CIL enables TJIT optimizations for any program compiled to this platform. In addition, to validate that the performance gains of a TJIT for JavaScript do not depend on specific idioms of JavaScript that are lost in the translation to CIL, we provide a performance evaluation of our JavaScript runtime which translates JavaScript to CIL and then runs on top of our CIL TJIT.
    • Mike Barnett, Manuel Fahndrich, and Francesco Logozzo, Embedded Contract Languages, in ACM SAC - OOPS, Association for Computing Machinery, Inc., March 2010
      Specifying application interfaces (APIs) with information that goes beyond method argument and return types is a long-standing quest of programming language researchers and practitioners. The number of type system extensions or specification languages is roughly equal to the number of tools that consume them. In other words, every tool comes with its own specification language. In this paper we argue that for modern object-oriented languages, using an embedding of contracts as code is a better approach. We exemplify our embedding of Code Contracts on the Microsoft managed execution platform (.NET) using the C# programming language. The embedding works as well in Visual Basic. We discuss the numerous advantages of our approach and the technical challenges, as well as the status of tools that consume the embedded contracts
    • Michael Bebenita, Florian Brandner, Manuel Fahndrich, Francesco Logozzo, Wolfram Schulte, Nikolai Tillmann, and Herman Venter, SPUR: a trace-based JIT compiler for CIL, in Proceedings of the ACM international conference on Object oriented programming systems languages and applications, ACM, New York, NY, USA, 2010

    2009

    • Songtao Xia, Manuel Fahndrich, and Francesco Logozzo, Inferring Dataflow Properties of User Defined Table Processors, in Proceeding of the 16th International Static Analysis Symposium (SAS'09), Springer Verlag, August 2009
      In SCOPE, a SQL style cloud-level data-mining scripting language, table processing capabilities are often provided by user defined .NET methods. The Scope compiler can optimize its query plan if it knows certain dataflow relations between the input and output tables. Useful relations are dependence or equality between input and output columns, or constraints over the output columns. Automatically and accurately inferring these properties is difficult due to the special compilation scheme of .NET iterators, the need to reason about numerical relations for naming or estimating column numbers, aliasing and escaping, and the need to automatically infer universally quantified loop invariants. We designed and implemented Scooby, a custom-tailored, abstract interpretation-based, domain specific static analyzer for .NET iterators. We adopt and extend the state-of-the-art abstraction and quantified invariant inference techniques to solve these problems in a way that suits our application domain. Scooby is able to discover these properties for every-day SCOPE programs automatically, efficiently, and accurately.
    • Michael Barnett, Manuel Fahndrich, Francesco Logozzo, Peli de Halleux, and Nikolai Tillmann, Exploiting the Synergy between Automated-Test-Generation and Programming-by-Contract, in Proc. 31st International Conference on Software Engineering (ICSE'2009) , IEEE, May 2009
      This demonstration presents two tools, Code Contracts and Pex, that utilize specification constructs for advanced testing, runtime checking, and static checking of object-oriented .NET programs.
    • Francesco Logozzo and Manuel Fahndrich, Pentagons: A Weakly Relational Abstract Domain for the Efficient Validation of Array Accesses, in Science of Computer Programming, Springer Verlag, 2009
      We introduce Pentagons, a weakly relational numerical abstract domain useful for the validation of array accesses in byte-code and intermediate languages (IL). This abstract domain captures properties of the form of x in [a, b] & x < y. It is more precise than the well known Interval domain, but it is less precise than the Octagon domain. The goal of Pentagons is to be a lightweight numerical domain useful for adaptive static analysis, where Pentagons is used to quickly prove the safety of most array accesses, restricting the use of more precise (but also more expensive) domains to only a small fraction of the code. We implemented the Pentagons abstract domain in Clousot, a generic abstract interpreter for .NET assemblies. Using it, we were able to validate 83% of array accesses in the core runtime library mscorlib.dll in a little bit more than 3 minutes.

    2008

    • Manuel Fahndrich, Sriram K. Rajamani, and Jakob Rehof, Static Deadlock Prevention in Dynamically Configured Communication Networks, in Perspectives On Concurrency, Festchrift for Prof. P. S. Thiagarajan's 60th birthday, K. Lodaya, M. Mukund and R. Ramanujam (eds), Universities Press, December 2008
      We propose a technique to avoid deadlocks in a system of communicating processes. Our 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. Deadlocks happen in such networks if there is a cycle created by a set of channels, and processes along the cycle circularly wait for messages from each other. Our approach allows cycles of channels to be created, but avoids circular waiting by ensuring that for every cycle C, some process P breaks circular waits by selecting to communicate on both endpoints involved in the cycle C at P. We formalize this strategy as a calculus with a type system. Our type system keeps track of markers called obstructions where wait cycles are intended to be broken. Programmers annotate message types with design decisions on how obstructions are managed. Using these annotations, our type checker works modularly and independently on each process,without suffering any state space explosion. We prove the soundness of the analysis (namely deadlock 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.
    • Pietro Ferrara, Francesco Logozzo, and Manuel Fähndrich, Safer unsafe code for .NET, in Proceedings of the 23rd ACM Conference on Object-Oriented Programming (OOPSLA'08), Association for Computing Machinery, Inc., October 2008
      The .NET intermediate language (MSIL) allows expressing both statically verifiable memory and type safe code (typically called managed), as well as unsafe code using direct pointer manipulations. Unsafe code can be expressed in C# by marking regions of code as unsafe. Writing unsafe code can be useful where the rules of managed code are too strict. The obvious drawback of unsafe code is that it opens the door to programming errors typical of C and C++, namely memory access errors such as buffer overruns. Worse, a single piece of unsafe code may corrupt memory and destabilize the entire runtime or allow attackers to compromise the security of the platform. We present a new static analysis based on abstract interpretation to check memory safety for unsafe code in the .NET framework. The core of the analysis is a new numerical abstract domain, Stripes, which is used to efficiently compute memory invariants. Stripes is combined with lightweight abstract domains to raise the precision, yet achieving scalability. We implemented this analysis in Clousot, a generic static analyzer for .NET. In combination with contracts expressed in Foxtrot, an MSIL based annotation language for .NET, our analysis provides static safety guarantees on memory accesses in unsafe code. We tested it on all the assemblies of the .NET framework. We compare our results with those obtained using existing domains, showing how they are either too imprecise (eg, Intervals or Octagons) or too expensive (Polyhedra) to be used in practice.
    • Francesco Logozzo and Manuel Fähndrich, Pentagons: A weakly relational domain for the efficient validation of array accesses, in Proceedings of the 23th ACM Symposium on Applied Computing , Association for Computing Machinery, Inc., March 2008
      We introduce Pentagons (\Pentagons), a weakly relational numerical abstract domain useful for the validation of array accesses in byte-code and intermediate languages (IL). This abstract domain captures properties of the form of x in [a, b] && x < y. It is more precise than the well known Interval domain, but it is less precise than the Octagon domain. The goal of Pentagons is to be a lightweight numerical domain useful for adaptive static analysis, where Pentagons is used to quickly prove the safety of most array accesses, restricting the use of more precise (but also more expensive) domains to only a small fraction of the code. We implemented the Pentagons abstract domain in Clousot, a generic abstract interpreter for .NET assemblies. Using it, we were able to validate 83% of array accesses in the core runtime library mscorlib.dll in less than 8 minutes.
    • Francesco Logozzo and Manuel Fähndrich, On the Relative Completeness of Bytecode Analysis versus Source Code Analysis, in Proceedings of the International Conference on Compiler Construction, Springer Verlag, 2008
      We discuss the challenges faced by bytecode analyzers designed for code verification compared to similar analyzers for source code. While a bytecode-level analysis brings many simplifications, eg, fewer cases, independence from source syntax, name resolution, etc., it also introduces precision loss that must be recovered either via preprocessing, more precise abstract domains, more precise transfer functions, or a combination thereof. The paper studies the relative completeness of a static analysis for bytecode compared to the analysis of the program source. We illustrate it through examples originating from the design and the implementation of Clousot, a generic static analyzer based on Abstract Interpretation for the analysis of MSIL.

    2007

    • Manuel Fähndrich and Songtao Xia, Establishing Object Invariants with Delayed Types, in Proceedings of the 22nd ACM Conference on Object-Oriented Programming, Systems, and Applications, ACM, October 2007
      Mainstream object-oriented languages such as C# and Java provide an initializationmodel for objects that does not guarantee programmer controlled initialization of fields. Instead, all fields are initialized to default values (0 for scalars and null for non-scalars) on allocation. This is in stark contrast to functional languages, where all parts of an allocation are initialized to programmer-provided values. These choices have a direct impact on two main issues: 1) the prevalence of null in object oriented languages (and its general absence in functional languages), and 2) the ability to initialize circular data structures. This paper explores connections between these differing approaches and proposes a fresh look at initialization. Delayed types are introduced to express and formalize prevalent initialization patterns in object-oriented languages.
    • Mike Barnett, Manuel Fahndrich, Diego Garbervetsky, and Francesco Logozzo, Annotations for (more) Precise Points-to Analysis, in IWACO 2007, 2007

    2006

    • Manuel Fähndrich, Michael Carbin, and James R. Larus, Reflective Program Generation with Patterns, in Proceedings of the 2006 Conference on Generative Programming and Component Engineering, ACM, October 2006
      Runtime reflection facilities, as present in Java and .NET, are powerful mechanisms for inspecting existing code and metadata, as well as generating new code and metadata on the fly. Such power does come at a high price though. The runtime reflection support in Java and .NET imposes a cost on all programs, whether they use reflection or not, simply by the necessity of keeping all metadata around and the inability to optimize code because of future possible code changes. A second—often overlooked—cost is the difficulty of writing correct reflection code to inspect or emit new metadata and code and the risk that the emitted code is not well-formed. In this paper we examine a subclass of problems that can be addressed using a simpler mechanism than runtime reflection, which we call compile-time reflection.We argue for a high-level construct called a transform that allows programmers to write inspection and generation code in a pattern matching and template style, avoiding at the same time the complexities of reflection APIs and providing the benefits of staged compilation in that the generated code and metadata is known to be well-formed and type safe ahead of time.
    • Galen C. Hunt, Mark Aiken, Paul Barham, Manuel Fahndrich, Chris Hawblitzel, Orion Hodson, James R. Larus, Steven Levi, Nick Murphy, Bjarne Steensgaard, David Tarditi, Ted Wobber, and Brian D. Zill, Sealing OS Processes to Improve Dependability and Security, no. MSR-TR-2006-51, April 2006
      On most modern operating systems, a process is a hardware-protected abstraction for executing potentially mutable code and data. Common features of processes include: dynamic code loading, dynamic code generation, access to cross-process shared memory, and a universal API. This paper argues that many of the dependability and security weaknesses of modern systems are exacerbated by an open process architecture. Moreover, this architecture impairs the ability of tools to analyze code statically, to improve its performance or dependability. By contrast, a sealed process architecture prohibits dynamic code loading, prohibits self-modifying code, prohibits shared memory, and replaces a universal API with a process-limited API. This paper describes an implementation of a sealed process architecture in the Singularity operating system, discusses its merits, and evaluates its impact. Among the benefits are: improved static program analysis, strong security guarantees, elimination of OS redundancies found in language runtimes such as the JVM and CLR, and better software engineering.
    • Manuel Fähndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen Hunt, James R. Larus, and Steven Levi, Language Support for Fast and Reliable Message-based Communication in Singularity OS, in Proceedings of the EuroSys 2006 Conference, Association for Computing Machinery, Inc., April 2006
      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.
    • Mark Aiken, Manuel Fähndrich, Chris Hawblitzel, Galen Hunt, and James Larus, Deconstructing Process Isolation, no. MSR-TR-2006-43, April 2006
      Most operating systems enforce process isolation through hardware protection mechanisms such as memory segmentation, page mapping, and differentiated user and kernel instructions. Singularity is a new operating system that uses software mechanisms to enforce process isolation. A software isolated process (SIP) is a process whose boundaries are established by language safety rules and enforced by static type checking. With proper system support, SIPs can provide a low cost isolation mechanism that provides failure isolation and fast inter-process communication. To compare the performance of Singularity’s approach against more conventional systems, we implemented an optional hardware isolation mechanism. Protection domains are hardware-enforced address spaces, which can contain one or more SIPs. Domains can either run at the kernel’s privilege levels and share an exchange heap or be fully isolated from the kernel and run at the normal application privilege level. These domains can construct Singularity configurations that are similar to micro-kernel and monolithic kernel systems. Hardware-based isolation incurs non-trivial performance costs (up to 25-33%) and complicates system implementation. Software isolation has less than 5% overhead on these benchmarks. The lower cost of SIPs permits them to provide protection and failure isolation at a finer granularity than conventional processes. Singularity’s ability to employ hardware isolation selectively, rather than at every process boundary, supports the construction of more resilient system architectures.

    2005

    • Mike Barnett, Robert DeLine, Bart Jacobs, Manuel Fahndrich, Rustan Leino, Wolfram Schulte, and Herman Venter, The Spec# programming system: Challenges and directions., in Verified Software: Theories, Tools, Experiments (LNCS4171, ISSN 0302-9743), Springer Verlag, 10 October 2005
    • Galen Hunt, James R. Larus, Martin Abadi, Mark Aiken, Paul Barham, Manuel Fahndrich, Chris Hawblitzel, Orion Hodson, Steven Levi, Nick Murphy, Bjarne Steensgaard, David Tarditi, Ted Wobber, and Brian D. Zill, An Overview of the Singularity Project, no. MSR-TR-2005-135, October 2005
      Singularity is a research project in Microsoft Research that started with the question: what would a software platform look like if it was designed from scratch with the primary goal of dependability? Singularity is working to answer this question by building on advances in programming languages and tools to develop a new system architecture and operating system (named Singularity), with the aim of producing a more robust and dependable software platform. Singularity demonstrates the practicality of new technologies and architectural decisions, which should lead to the construction of more robust and dependable systems.

    2004

    • Robert DeLine and Manuel Fähndrich, Typestates for objects, in ECOOP 2004 — Object-Oriented Programming, 18th European Conference, Springer Verlag, June 2004
      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 downcasting, 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.
    • James R. Larus, Thomas Ball, Manuvir Das, Robert DeLine, Manuel Fähndrich, Jon Pincus, Sriram K. Rajamani, and Ramanathan Venkatapathy, Righting Software, in IEEE Software, vol. 21, no. 3, pp. 92–100, Institute of Electrical and Electronics Engineers, Inc., May 2004
      Correctness tools can improve software development by systematically detecting programming errors. Microsoft Research has developed two generations of these tools that help programmers find and fix errors early in the development process.
    • Robert DeLine and Manuel Fähndrich, The Fugue Protocol Checker: Is Your Software Baroque?, no. MSR-TR-2004-07, January 2004
      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. This paper introduces Fugue, a modular static checker for languages that compile to the Common Language Runtime. Fugue allows the rules for using an interface to be recorded as declarative specifications and 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 ado.net, a library for accessing relational databases, and found several errors in an internal Microsoft Research web site, which extensively uses this library.

    2003

    • Manuel Fähndrich and K. Rustan M. Leino, Declaring and checking non-null types in an object-oriented language, in Proceedings of the 2003 ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2003, ACM, November 2003
      Distinguishing non-null references from possibly-null references at the type level can detect null-related errors in objectoriented 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.
    • Mike Barnett, Rob DeLine, Manuel Fähndrich, K. Rustan M. Leino, and Wolfram Schulte, Verification of Object-Oriented Programs With Invariants, in Formal Techniques for Java-like Programs (FTfJP), July 2003
    • Manuel Fähndrich and K. Rustan M. Leino, Heap monotonic typestate, in Proceedings of the first International Workshop on Alias Confinement and Ownership (IWACO), July 2003
      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.

    2002

    • Manuel Fähndrich and Robert DeLine, Adoption and Focus: Practical Linear Types for Imperative Programming, in Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), ACM, May 2002
      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 an 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.

    2001

    • Manuel Fahndrich and Robert DeLine, Adaption and Focus: Practical Linear Types for Imperative Programming, in Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation , Association for Computing Machinery, Inc., November 2001
      A type system with linearity is useful for checking software protocols andresource 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 an 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.
    • Robert DeLine and Manuel Fähndrich, Enforcing high-level protocols in low-level software, in Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), ACM, May 2001
      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.
    • J. Rehof and M. Fähndrich, Type-Based Flow Analysis: From Polymorphic Subtyping to CFL-Reachability, in Proceedings POPL 2001, 28'th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2001
      We present a novel approach to scalable implementation of type-based flow analysis with polymorphic subtyping. By giving a new presentation of polymorphic subtyping with instantiation constraints, we are able to apply context-free language (CFL) reachability techniques to type-based flow analysis. We develop a CFL-based algorithm for computing flow information in time O(n^3), where n is the size of the typed program. The algorithm substantially improves upon the best previously known algorithm for this problem with complexity O(n^8). Our technique also yields the first demand-driven algorithm for polymorphic subtype-based flow-computation. It works directly on higher-order programs with structured data, supports context-sensitive, global flow summarization and includes polymorphic recursion.
    • Manuvir Das, Manuel Fähndrich, Ben Liblit, and Jakob Rehof, Estimating the Impact of Scalable Pointer Analysis on Optimization, no. MSR-TR-2001-20, January 2001
      This paper addresses the following question: Do scalable control-flow-insensitive pointer analyses provide the level of precision required to make them useful in compiler optimizations? We first describe alias frequency, a metric that measures the ability of a pointer analysis to determine that pairs of memory accesses in C programs cannot be aliases. We believe that this kind of information is useful for a variety of optimizations, while remaining independent of a particular optimization. We show that control-flow and context insensitive analyses provide the same answer as the best possible pointer analysis on at least 95% of all statically generated alias queries. In order to understand the potential run-time impact of the remaining 5% queries, we weight the alias queries by dynamic execution counts obtained from profile data. Flow-insensitive pointer analyses are accurate on at least 95% of the weighted alias queries as well. We then examine whether scalable pointer analyses are inaccurate on the remaining 5% alias queries because they are context-insensitive. To this end, we have developed a new context-sensitive pointer analysis that also serves as a general engine for tracing the flow of values in C programs. To our knowledge, it is the first technique for performing context-sensitive analysis with subtyping that scales to millions of lines of code. We find that the new algorithm does not identify fewer aliases than the contextinsensitive analysis.

    2000

    • M. Fähndrich, J. Rehof, and M. Das, Scalable Context-Sensitive Flow Analysis Using Instantiation Constraints, in Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2000
      This paper shows that a type graph (obtained via polymorphic type inference) harbors explicit directional flow paths between functions. These flow paths arise from the instantiations of polymorphic types and correspond to call-return sequences in first-order programs. We show that flow information can be computed efficiently while considering only paths with well matched call-return sequences, even in the higher-order case. Furthermore, we present a practical algorithm for inferring type instantiation graphs and provide empirical evidence to the scalability of the presented techniques by applying them in the context of points-to analysis for C programs.
    • Jeffrey S. Foster, Manuel Fähndrich, and Alexander Aiken, Polymorphic versus Monomorphic Flow-insensitive Points-to Analysis for C, in Proceedings of the 7th International Static Analysis Symposium, June 2000
      We carry out an experimental analysis for two of the design dimensions of flow-insensitive points-to analysis for C: polymorphic versus monomorphic and equality-based versus inclusion-based. Holding other analysis parameters fixed, we measure the precision of the four design points on a suite of benchmarks of up to 90,000 abstract syntax tree nodes. Our experiments show that the benefit of polymorphism varies significantly with the underlying monomorphic analysis. For our equalitybased analysis, adding polymorphism greatly increases precision, while for our inclusion-based analysis, adding polymorphism hardly makes any difference. We also gain some insight into the nature of polymorphism in points-to analysis of C. In particular, we find considerable polymorphism available in function parameters, but little or no polymorphism in function results, and we show how this observation explains our results.
    • M. Fähndrich, J. Rehof, and M. Das, From Polymorphic Subtyping to CFL Reachability: Context-Sensitive Flow Analysis Using Instantiation Constraints, no. MSR-TR-99-84, March 2000
      We present a novel approach to computing context-sensitive flow of values through procedures and data structures. Our approach combines and extends techniques from two seemingly disparate areas: polymorphic subtyping and interprocedural dataflow analysis based on context-free language reachability. The resulting technique offers several advantages over previous approaches: it works directly on higher-order programs, provides demand-driven interprocedural queries, and improves the asymptotic complexity of a known algorithm based on polymorphic subtyping from O(n^8) to O(n^3) for computing all queries. For intra-procedural flow restricted to equivalence classes, our algorithm yields linear inter-procedural flow queries.
    • Zhendong Su, Manuel Fähndrich, and Alexander Aiken, Projection Merging: Reducing Redundancies in Inclusion Constraint Graphs, in Proceedings POPL 2000, 27'th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2000
      Inclusion-based program analyses are implemented by adding new edges to directed graphs. In most analyses, there are many different ways to add a transitive edge between two nodes, namely through each different path connecting the nodes. This path redundancy limits the scalability of these analyses. We present projection merging, a technique to reduce path redundancy. Combined with cycle elimination, projection merging achieves orders of magnitude speedup of analysis time on programs over that of using cycle elimination alone.

    1999

    • Manuel Fähndrich, BANE: A Library for Scalable Constraint-Based Program Analysis, May 1999
      Program analysis is an important aspect of modern program development. Compilers use program analysis to prove the correctness of optimizing program transformations. Static error detection tools use program analysis to alert the programmer to the presence of potential errors. This dissertation focuses on the expressiveness and implementation of constraint-based program analyses, i.e., analyses that are expressed as solutions to a system of constraints. We show that structuring the implementation of program analyses around a library of generic constraint solvers promotes reuse, gives control over precision-efficiency tradeoffs, and enables optimizations that yield orders of magnitude speedups over standard implementations. The first part of the dissertation develops the formalism of mixed constraints which provides a combination of several constraint formalisms with distinct precision-efficiency tradeoffs. We provide a semantics for constraints and constraint resolution algorithms. The second part of the dissertation describes an implementation of mixed constraints and a number of novel techniques to support the practical resolution of large constraint systems. We give empirical results supporting the claims of scalability, reuse, and choice of precision-efficiency tradeoffs provided by the mixed constraint framework.

    1998

    • M. Fähndrich, J. Foster, Z. Su, and A. Aiken, Partial Online Cycle Elimination in Inclusion Constraint Graphs, in Proceedings of the 1998 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 1998
      Many program analyses are naturally formulated and implemented using inclusion constraints. We present newresults 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 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 substantial experiment.
    • Alexander Aiken, Manuel Fähndrich, and Zhendong Su, Detecting Races in Relay Ladder Logic Programs, in Proceedings of the 1st Conference on Tools and Algorithms for the Analysis and Construction of Systems, March 1998
      Relay Ladder Logic (RLL) is a programming language widely used for complex embedded control applications such as manu- facturing 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 demon- strate that our analysis is useful in detecting some flaws in production RLL programs that are difficult to find by other techniques.
    • M. Fähndrich, J. Foster, Alexander Aiken, and Jason Cu, Tracking down Exceptions in Standard ML Programs, no. UCB//CSD-96-996, February 1998
      We describe our experience 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 error and control-flow exceptions. Furthermore, using our tools, we have uncovered two minor exception-related bugs in the three programs we scrutinized.

    1997

    • Manuel Fähndrich and Alexander Aiken, Program Analysis Using Mixed Term and Set Constraints, in Proceedings of the 4th International Static Analysis Symposium, Springer Verlag, September 1997
    • Manuel Fähndrich and John Boyland, Staticallly Checkable Pattern Abstractions, in Proceedings of the International Conference on Functional Programming (ICFP '97), June 1997
      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.
    • Manuel Fähndrich and Alexander Aiken, Refined Type Inference for ML, in Proceedings of the 1st Workshop on Types in Compilation, June 1997

    1996

    1995

    • A. Aiken and M. Fähndrich, Dynamic Typing and Subtype Inference, in Proceedings of the 1995 Conference on Functional Programming Languages and Computer Architecture, June 1995
      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.
    • A. Aiken, M. Fähndrich, and R. Levien, Better Static Memory Management: Improving region-based analysis of higher-order languages, in Proceedings of the 1995 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 1995
      Static memory management replaces runtime garbage collection with compile-time annotations that make all memory allocation and deallocation explicit in a 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.