K. Rustan

A basis for verifying multi-threaded programs (2009)

Abstract. The specification of object-oriented and other pointer-based programs must be able to describe the structure of the program’s dynamically allocated data as well as some abstract view of...

Flexible Immutability with Frozen Objects (2009)

Abstract. Advanced multi-threaded programs apply concurrency concepts in sophisticated ways. For instance, they use fine-grained locking to increase parallelism and change locking orders dynamically...

ETH Zurich (2009)

John Hatcliff, Gary T. Leavens, K. Rustan, M. Leino, Peter Müller, Matthew Parkinson

Behavioral interface speci cation languages allow programmers to express the intended behavior of programs such as functional behavior and resource consumption. Formal speci cations of program...

K. Rustan, M. Leino, Peter Müller, Angela Wallenburg

Abstract. Object immutability is a familiar concept that allows safe sharing of objects. Existing language support for immutability is based on immutable classes. However, class-based approaches are...

The Boogie 2 Type System: Design and Verification Condition Generation (2009)

Reasoning about Comprehensions with First-Order SMT Solvers ABSTRACT (2009)

Abstract. Intermediate languages are a paradigm to separate concerns in software verification systems when bridging the gap between (realworld) programming languages and the logics understood by...

Real estate of names (2009)

This paper presents a technique for translating common comprehension expressions (sum, count, product, min, and max) into verification conditions that can be tackled by two off-the-shelf first-order...

Object Invariants in Dynamic Contexts (2009)

A common convention for writing names (identifiers) in mathematical formulas makes poor use of the real estate on the page occupied by those names. Here is a design principle for using space more...

Language Constructs and Features General Terms (2009)

Abstract. Object invariants describe the consistency of object-oriented data structures and are central to reasoning about the correctness of object-oriented software. Yet, reasoning about object...

K. Rustan, M. Leino, Compaq Src, Yunhong Zhou, Compaq Src

data groups to specify and check side effects

lazily proof-explicating (2009)

K. Rustan, M. Leino, Madan Musuvathi, Xinming Ou

two-tier technique for supporting quantifiers in a

or: A (2008)

Extended Static Checking: a Ten-Year Perspective (2008)

widenings to infer loop invariants

Automatic Verification of Textbook Programs That Use (2008)

Abstract. A powerful approach to finding errors in computer software is to translate a given program into a verification condition, a logical formula that is valid if and only if the program is free...

K. Rustan, M. Leino, Rosemary Monahan

Abstract. This paper presents a technique for translating common comprehension expressions (sum, count, product, min, and max) into verification conditions that can be tackled by two first-order SMT...

Generating error traces from verification-condition counterexamples (2008)

K. Rustan, M. Leino, Todd Millstein B, Jamesb. Saxe C

A technique for finding errors in computer programs is to translate a given program and its correctness criteria into a logical formula in mathematics and then let an automatic theorem prover check...

ABSTRACT Extended Static Checking for Java (2008)

Cormac Flanagan, K. Rustan, M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, ...

Software development and maintenance are costly endeavors. The cost can be reduced if more software defects are detected earlier in the development cycle. This paper introduces the Extended Static...

An overview of JML tools and applications www.jmlspecs.org (2008)

Lilian Burdy A, Yoonsik Cheon C, David Cok B, Joe Kiniry E, ...

f Microsoft Research

References (2008)

Sarfraz Khurshid, Orna Grumberg, Mike Barnett, Robert Deline, Manuel Fahndrich, ...

The students are expected to have basic knowledge of data structures and object-oriented programming, and considerable programming experience. Outline The process of software validation includes...

Extended Static Checking: a Ten-Year Perspective (2008)

ABSTRACT Class-Local Object Invariants (2008)

Abstract. A powerful approach to finding errors in computer software is to translate a given program into a verification condition, a logical formula that is valid if and only if the program is free...

Bibliography (2008)

Ac Martín Abadi, Luca Cardelli, A Theory, Objects Springer, ...

[Ble79] Woodrow W. Bledsoe. A maximal method for set variables. Machine

ABSTRACT Extended Static Checking for Java (2008)

The correctness of object-oriented programs relies on object invariants. A system for verifying such programs requires a systematic method for coping with object invariants that can be violated...

Cormac Flanagan, K. Rustan, M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, ...

Software development and maintenance are costly endeavors. The cost can be reduced if more software defects are detected earlier in the development cycle. This paper introduces the Extended Static...

Abstract Data groups: Specifying the modification of extended state (2008)

Verification of Equivalent-Results Methods (2008)

This paper explores the interpretation of specifications in the context of an object-oriented programming language with subclassing and method overrides. In particular, the paper considers...

Heap Monotonic Typestates (Extended Abstract) (2008)

Abstract. Methods that query the state of a data structure often return identical or equivalent values as long as the data structure does not change. Program verification depends on this fact, but it...

Manuel Fähndrich, K. Rustan, M. Leino

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...

Data abstraction and information hiding (2008)

K. Rustan, M. Leino, Greg Nelson

This paper describes an approach for verifying programs in the presence of data abstraction and information hiding, which are key features of modern programming languages with objects and modules....

ABSTRACT Extended Static Checking for Java (2008)

Cormac Flanagan, K. Rustan, M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, ...

Software development and maintenance are costly endeavors. The cost can be reduced if more software defects are detected earlier in the development cycle. This paper introduces the Extended Static...

A SAT Characterization of Boolean-Program Correctness (2008)

A Verifying Compiler for a (2008)

Abstract. Boolean programs, imperative programs where all variables have type boolean, have been used effectively as abstractions of device drivers (in Ball and Rajamani’s SLAM project). To find...

or: A (2008)

A verification methodology for model fields (2008)

widenings to infer loop invariants

Inferring Object Invariants (Extended Abstract) (2008)

Abstract. Model fields are specification-only fields that encode abstractions of the concrete state of a data structure. They allow specifications to describe the behavior of object-oriented programs...

Loop invariants on demand (2008)

The program state for object-oriented languages, such as Java or C#, consists of both variables local to procedures and variables stored in the global heap. The variables stored in the heap are the...

Using history invariants to verify observers (2008)

Abstract. This paper describes a sound technique that combines the precision of theorem proving with the loop-invariant inference of abstract interpretation. The loop-invariant computations are...

Inferring Object Invariants (Extended Abstract) (2008)

Abstract. This paper contributes a technique that expands the set of object invariants that one can reason about in modular verification. The technique uses history invariants, two-state invariants...

Language Constructs and Features General Terms (2008)

The program state for object-oriented languages, such as Java or C#, consists of both variables local to procedures and variables stored in the global heap. The variables stored in the heap are the...

K. Rustan, M. Leino, Compaq Src, Yunhong Zhou, Compaq Src

data groups to specify and check side effects

Modular verification of static class invariants (2008)

Under consideration for publication in Formal Aspects of Computing Specification and verification challenges for sequential object-oriented programs (2008)

Abstract. Object invariants describe the consistency of object-oriented data structures and are central to reasoning about the correctness of object-oriented software. But object invariants are not...

Gary T. Leavens, K. Rustan, M. Leino, Peter Müller

Abstract. The state of knowledge in how to specify sequential programs in object-oriented languages such as Java and C # and the state of the art in automated verification tools for such programs...

Using history invariants to verify observers (2008)

A Verifying Compiler for a (2008)

Abstract. This paper contributes a technique that expands the set of object invariants that one can reason about in modular verification. The technique uses history invariants, two-state invariants...

Efficient Weakest Preconditions (2008)

Desired computer-program properties can be described by logical formulas called verification conditions. Different mathematically-equivalent forms of these verification conditions can have a great...

This is Boogie 2 (2008)

1 A Programming Model for Concurrent Object-Oriented Programs (2008)

Abstract. Boogie is an intermediate verification language, designed to make the prescription of verification conditions natural and convenient. It serves as a common intermediate representation for...

Bart Jacobs, Frank Piessens, Jan Smans, K. Rustan, M. Leino, Wolfram Schulte

Reasoning about multithreaded object-oriented programs is difficult, due to the nonlocal nature of object aliasing and data races. We propose a programming regime (or programming model) that rules...

Semantics of exceptions (2007)

Report 160 Data abstraction and information hiding (2007)

This note describes a trace semantics of exceptions from which a weakest precondition semantics is derived. We present a theorem that suggests how exceptions should be used. 1

K. Rustan, K. Rustan, M. Leino, M. Leino, Greg Nelson, Greg Nelson

SRC's charter is to advance the state of the art in computer systems by doing basic and applied research in support of our company's business objectives. Our interests and projects span...

FMICS 2002 Preliminary Version An overview of JML tools and applications www.jmlspecs.org (2007)

Lilian Burdy A, Yoonsik Cheon C, David Cok B, Michael Ernst D, Joe Kiniry E, ...

f Microsoft Research

Generating error traces from verification-condition (2007)

K. Rustan, M. Leino, Todd Millstein, James B. Saxe

counterexamples

ABSTRACT Extended Static Checking for Java (2007)

Cormac Flanagan, K. Rustan, M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, ...

Software development and maintenance are costly endeavors. The cost can be reduced if more software defects are detected earlier in the development cycle. This paper introduces the Extended Static...

Copyright c (2007)

Extended Static Checking: a Ten-Year Perspective (2007)

A static program checker that performs modular checking can check one program module for errors without needing to analyze the entire program. Modular checking requires that each module be...

1 Annotation inference for modular checkers (2007)

Abstract. A powerful approach to finding errors in computer software is to translate a given program into a verification condition, a logical formula that is valid if and only if the program is free...

Cormac Flanagan, Rajeev Joshi, K. Rustan, M. Leino

This paper presents a general approach to annotation inference for a given static program checker. The approach reuses the checker as a subroutine. The approach has been used to implement annotation...

Efficient Annotation Inference for an Extended Static Checker (2007)

Cormac Flanagan, Compaq Src, K. Rustan, M. Leino, Michael Y. Levin

Submission to SAS'01.) A modular static program checker relies on annotations specifying module interfaces. Writing annotations is a burden to the programmer. The Houdini algorithm is a...

b (2007)

L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. R. Kiniry, G. T. Leavens, ...

An overview of JML tools and applications www.jmlspecs.org

Formal Methods for Industrial Critical Systems (FMICS ’03), vol. 80 of Electronic Notes in Theoretical Computer Science, pp. 73–89, Elsevier, 2003.] (2007)

Lilian Burdy, Yoonsik Cheon, David Cok, Michael D. Ernst, Joe Kiniry, Gary T. Leavens, ...

Abstract. The Java Modeling Language (JML) can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a...

Modular verification of global module invariants in (2007)

Automatic verification of textbook programs (2007)

object-oriented programs

K. Rustan, M. Leino, Rosemary Monahan

Abstract. Textbooks on program verification make use of simple programs in mathematical domains as illustrative examples. Mechanical verification tools can give students a quicker way to learn,...

Practical reasoning about invocations and implementations of pure methods (2007)

Ádám Darvas, K. Rustan, M. Leino

pure methods

Theory and Use of Conditional Composition (2006)

Manohar, Rajit, Rustan, K., Leino, M.

In this note, tagged collections and tbeir compositions were introduced. Tbese collections can be viewed as quantified expressions and can be used to manipulate lists and functions using tbe existing...

Boogie: A modular reusable verifier for object-oriented programs (2006)

Mike Barnett, Robert Deline, Bart Jacobs, K. Rustan, M. Leino

Abstract. A program verifier is a complex system that uses compiler technology, program semantics, property inference, verification-condition generation, automatic decision procedures, and a user...

Boogie: A modular reusable verifier for object-oriented programs (2006)

Mike Barnett, Robert Deline, Bart Jacobs, K. Rustan, M. Leino

Abstract. A program verifier is a complex system that uses compiler technology, program semantics, property inference, verification-condition generation, automatic decision procedures, and a user...

Loop invariants on demand (2005)

Inferring Object Invariants (Extended Abstract) (2005)

Abstract. This paper describes a sound technique that combines the precision of theorem proving with the loop-invariant inference of abstract interpretation. The loop-invariant computations are...

Safe Concurrency for Aggregate Objects with Invariants (2005)

The program state for object-oriented languages, such as Java or C#, consists of both variables local to procedures and variables stored in the global heap. The variables stored in the heap are the...

Bart Jacobs Rustan, Bart Jacobs, K. Rustan, M. Leino, Frank Piessens, Wolfram Schulte

Developing safe multithreaded software systems is difficult due to the potential unwanted interference among concurrent threads. This paper presents a flexible methodology for object-oriented...

Abstract interpretation with alien expressions and heap structures (2005)

The Spec# Programming System: Challenges and Directions. Position paper at VSTTE (2005)

Abstract. The technique of abstract interpretation analyzes a computer program to infer various properties about the program. The particular properties inferred depend on the particular abstract...

Mike Barnett, Robert Deline, Bart Jacobs, Manuel Fähndrich, K. Rustan, M. Leino, ...

The Spec # programming system [2] is a new attempt to increase the quality of general purpose, industrial software. Using old wisdom, we propose the use of specifications to make programmer...

The Spec# Programming System: Challenges and Directions. Position paper at VSTTE (2005)

Mike Barnett, Robert Deline, Bart Jacobs, Manuel Fähndrich, K. Rustan, M. Leino, ...

The Spec # programming system [2] is a new attempt to increase the quality of general purpose, industrial software. Using old wisdom, we propose the use of specifications to make programmer...

Abstract interpretation with alien expressions and heap structures (2005)

– Conceptually elegant Clarkson: Extended Static Checking 5 Authors Author (2005)

Abstract. The technique of abstract interpretation analyzes a computer program to infer various properties about the program. The particular properties inferred depend on the particular abstract...

Michael Clarkson, K. Rustan, M. Leino, Greg Nelson, James B. Saxe, Wolfram Schulte, ...

• Purpose: finding bugs, not full verification • Nine out of the last twelve seminar papers: – ESP, buffer overflows, race detection, ownership types, pointer assertions • Approach so far:...

Verification of object-oriented programs with invariants (2004)

Mike Barnett, Robert Deline, Manuel Fähndrich, K. Rustan, M. Leino, Wolfram Schulte

An object invariant defines what it means for an object’s data to be in a consistent state. Object invariants are central to the design and correctness of objectoriented programs. This paper...

Verification of object-oriented programs with invariants (2004)

Mike Barnett, Robert Deline, Manuel Fähndrich, K. Rustan, M. Leino, Wolfram Schulte

An object invariant defines what it means for an object’s data to be in a consistent state. Object invariants are central to the design and correctness of objectoriented programs. This paper...

Abstract. Spec # is the latest in a long line of work on programming languages and systems aimed at improving the development of correct software. This paper describes the goals and architecture of...

Verification of multithreaded object-oriented programs with invariants (2004)

Abstract. The Spec # programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. This paper describes the goals and architecture of the Spec #...

Bart Jacobs, K. Rustan, M. Leino

Developing safe multithreaded software systems is difficult due to the potential unwanted interference among concurrent threads. This paper presents a sound, modular, and simple verification...

Verification of object-oriented programs with invariants (2004)

Mike Barnett, Robert Deline, Manuel Fähndrich, K. Rustan, M. Leino

Abstract. This extended abstract outlines a system for the modular verification of an object-oriented programming language. While simplified, the language has object and array references,...

Object Invariants in Dynamic Contexts (2004)

An overview of JML tools and applications (2004)

Object invariants describe the consistency of object-oriented data structures and are central to reasoning about the correctness of object-oriented software.

Lilian Burdy, Yoonsik Cheon, David R. Cok, Davidr. Cok, Michael D. Ernst, Joseph R. Kiniry, ...

The Java Modeling Language (JML) can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a specification...

Verification of object-oriented programs with invariants (2004)

Mike Barnett, Robert Deline, Manuel Fähndrich, K. Rustan, M. Leino, Wolfram Schulte

An object invariant defines what it means for an object’s data to be in a consistent state. Object invariants are central to the design and correctness of objectoriented programs. This paper...

Verification of multithreaded object-oriented programs with invariants (2004)

Bart Jacobs, K. Rustan, M. Leino

Developing safe multithreaded software systems is difficult due to the potential unwanted interference among concurrent threads. This paper presents a sound, modular, and simple verification...

Abstract. The Spec # programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. This paper describes the goals and architecture of the Spec #...

lazily proof-explicating (2004)

Abstract. The Spec # programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. This paper describes the goals and architecture of the Spec #...

K. Rustan, M. Leino, Madan Musuvathi, Xinming Ou

two-tier technique for supporting quantifiers in a

Verification of multithreaded object-oriented programs with invariants (2004)

Bart Jacobs, K. Rustan, M. Leino

Developing safe multithreaded software systems is difficult due to the potential unwanted interference among concurrent threads. This paper presents a sound, modular, and simple verification...

In memory of Edsger W. Dijkstra. (2004)

On computing the fixpoint of a set of boolean equations (2003)

Desired computer-program properties can be described by logical formulas called verification conditions. Different mathematically-equivalent forms of these verification conditions can have a great...

Kuncak, Viktor, Rustan, K., Leino, M.

In-place refinement for effect checking (2003)

Viktor Kuncak, K. Rustan, M. Leino

The refinement calculus is a powerful framework for reasoning about programs, specifications, and refinement relations between programs and specifications. In this paper we introduce a new refinement...

In-place refinement for effect checking (2003)

An Overview of JML Tools and Applications (2003)

Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, ...

The Java Modeling Language (JML) can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a specification...

An overview of JML tools and applications (2003)

Lilian Burdy, Yoonsik Cheon, Joe Kiniry, ...

The Java Modeling Language (JML) can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a specification...

An overview of JML tools and applications (2003)

Www Jmlspecs Org, Lilian Burdy, Yoonsik Cheon, David Cok, Michael D. Ernst, Joe Kiniry, ...

The Java Modeling Language (JML) can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a specification...

On Computing the Fixpoint of a Set of Boolean Equations (2003)

Viktor Kuncak, K. Rustan, M. Leino

This paper presents a method for computing a least fixpoint of a system of equations over booleans. The resulting computation can be significantly shorter than the result of iteratively evaluating...

A SAT characterization of boolean-program correctness (2003)

Heap Monotonic Typestates (Extended Abstract) (2003)

Boolean programs, imperative programs where all variables have type boolean, have been used effectively as abstractions of device drivers (in Ball and Rajamani's SLAM project). To find errors in...

Manuel Fähndrich, K. Rustan, M. Leino

The paper defines the class of heap monotonic typestates. The monotonicity of such typestates enables sound checking algorithms without the need for nonaliasing regimes of pointers. The basic idea is...

On computing the fixpoint of a set of boolean equations (2003)

Viktor Kuncak, K. Rustan, M. Leino

This paper presents a method for computing a least fixpoint of a system of equations over booleans. The resulting computation can be significantly shorter than the result of iteratively evaluating...

An overview of jml tools and applications (2003)

Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T, ...

original version is available at www.springerlink.com

Verification of Object-Oriented Programs with Invariants (2003)

Mike Barnett, Robert DeLine, Manuel Fähndrich, Wolfram Schulte, K. Rustan, ...

This extended abstract outlines a system for the modular verification of an object-oriented programming language. While simplified, the language has object and array references, single-inheritance...

An overview of JML tools and applications (2003)

Lilian Burdy, Yoonsik Cheon, David Cok, Michael D. Ernst, Joe Kiniry, Gary T. Leavens, ...

1 Introduction JML [25, 26], which stands for "Java Modeling Language", is useful for specifying detailed designs of Java classes and interfaces. JML is a behavioral interface specification...

Non-null types in an object-oriented language (2002)

Manuel Fahndrich, K. Rustan, M. Leino

Abstract. Non-null types can detect certain null-related errors in object-oriented programs earlier and avoid other such errors altogether. This paper gives a proposal for retrofitting a language...

Extended Static Checking for Java (2002)

Cormac Flanagan Rustan, Cormac Flanagan, K. Rustan, M. Leino, Mark Lillibridge, Greg Nelson, ...

Software development and maintenance are costly endeavors. The cost can be reduced if more software defects are detected earlier in the development cycle. This paper introduces the Extended Static...

Finding (2002)

Michael Burrows, K. Rustan, M. Leino

Concurrent programs can suffer from many types of errors, not just the wellstudied problems of deadlocks and simple race conditions on variables. This paper addresses a kind of race condition that...

Finding stale-value errors in concurrent programs (2002)

Michael Burrows, K. Rustan, M. Leino

Concurrent programs can suffer from many types of errors, not just the wellstudied problems of deadlocks and simple race conditions on variables. This paper addresses a kind of race condition that...

Finding (2002)

Michael Burrows, K. Rustan, M. Leino

stale-value errors in concurrent programs

Non-null types in an object-oriented language (2002)

Manuel Fähndrich, K. Rustan, M. Leino

Abstract. Non-null types can detect certain null-related errors in object-oriented programs earlier and avoid other such errors altogether. This paper gives a proposal for retrofitting a language...

Houdini, an Annotation Assistant for ESC/Java (2001)

Houdini, an Annotation Assistant for ESC/Java (2001)

Abstract. A static program checker that performs modular checking can check one program module for errors without needing to analyze the entire program. Modular checking requires that each module be...

Annotation inference for modular checkers (2001)

A static program checker that performs modular checking can check one program module for errors without needing to analyze the entire program. Modular checking requires that each module be...

Cormac Flanagan, Rajeev Joshi, K. Rustan, M. Leino

This paper presents a general approach to annotation inference for a given static program checker. The approach reuses the checker as a subroutine. The approach has been used to implement annotation...

ESC/Java user’s manual (2001)

K. Rustan, M. Leino, Greg Nelson, James B. Saxe

kind, express or implied, including, but not limited to, the implied warranties of merchantability, fitness for a particular purpose, or non-infringement. This publication could include technical...

Houdini, an Annotation Assistant for ESC/Java (2001)

Houdini, an Annotation Assistant for ESC/Java (2001)

Abstract. A static program checker that performs modular checking can check one program module for errors without needing to analyze the entire program. Modular checking requires that each module be...

JML: notations and tools supporting detailed design in Java (2000)

A static program checker that performs modular checking can check one program module for errors without needing to analyze the entire program. Modular checking requires that each module be...

Gary T. Leavens, K. Rustan, M. Leino, Erik Poll, Clyde Ruby, Bart Jacobs, ...

2000 ACM. Permission to make digital or hard copies of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial...

A Semantic Approach to Secure Information Flow (2000)

Rajeev Joshi, K. Rustan, M. Leino

A classic problem in security is that of checking that a program has secure information #ow. Informally, this problem is described as follows: Given a program with variables partitioned into two...

JML: notations and tools supporting detailed design in Java (2000)

Gary T. Leavens, Gary T. Leavens, Clyde Ruby, Clyde Ruby, K. Rustan, ...

JML is a notation for specifying the detailed design of Java classes and interfaces. JML's assertions are stated using a slight extension of Java's expression syntax. This should make it...

Checking Java programs via guarded commands (1999)

K. Rustan, K. Rustan, M. Leino, M. Leino, James B. Saxe, ...

This paper defines a simple guarded-command--like language and its semantics. The language is used as an intermediate language in generating verification conditions for Java. The paper discusses why...

www.informatik.fernuni-hagen.de/pi5/publications.html. Checking Java programs via guarded commands (1999)

K. Rustan, M. Leino, James B. Saxe, Raymie Stata, K. Rustan, M. Leino, ...

This paper defines a simple guarded-command–like language and its semantics. The language is used as an intermediate language in generating verification conditions for Java. The paper discusses why...

Wrestling With Rep Exposure (1998)

David L. Detlefs, David L. Detlefs, K. Rustan, K. Rustan, M. Leino, ...

A central methodological problem in programming with multiple levels of abstractions is the loosely defined problem of rep exposure. This paper traces the problem of rep exposure to the precisely...

A Logic of Object-Oriented Programs (1998)

Martin Abadi, Martn Abadi, Martn Abadi, K. Rustan, K. Rustan, ...

We develop a logic for reasoning about object-oriented programs. The logic is for a language with an imperative semantics and aliasing, and accounts for self-reference in objects. It is much like a...

Extended Static Checking (1998)

David L. Detlefs, K. Rustan, M. Leino, Greg Nelson, James B. Saxe

The paper describes a mechanical checker for software that catches many common programming errors, in particular array index bounds errors, nil dereference errors, and synchronization errors in...

Specifying the Modification of Extended State (1998)

Data groups: Specifying the modification of extended state (1998)

This paper explores the interpretation of specifications in the context of an object-oriented programming language with subclassing and method overrides. In particular, the paper considers...

Rustan Leino Compaq, K. Rustan, M. Leino

This paper explores the interpretation of specifications in the context of an object-oriented programming language with subclassing and method overrides. In particular, the paper considers...

Joining Specification Statements (1998)

K. Rustan, M. Leino, Rajit Manohar

: The specification statement allows us to easily express what a program statement does. This paper shows how refinement of specification statements can be directly expressed using the predicate...

Recursive Object Types in a Logic of Object-Oriented Programs (1998)

Recursive Object Types In A Logic Of Object-Oriented Programs (1998)

. This paper formalizes a small object-oriented programming notation. The notation features imperative commandswhere objects can be shared (aliased), and is rich enough to allow subtypes and...

Extended static checking (1998)

. This paper formalizes a small object-oriented programming notation. The notation features imperative commands where objects can be shared (aliased), and is rich enough to allow subtypes and...

Report (1998)

David L. Detlefs, K. Rustan, M. Leino, Greg Nelson, David L. Detlefs, K. Rustan, ...

Wrestling with rep exposure

David L. Detlefs, David L. Detlefs, K. Rustan, K. Rustan, M. Leino, M. Leino, ...

The charter of SRC is to advance both the state of knowledge and the state of the art in computer systems. From our establishment in 1984 by Digital Equipment Corporation (now Compaq), we have...

Specifying the modification of extended state (1998)

K. Rustan, K. Rustan, M. Leino, M. Leino

d i g i t a l

and (1998)

Martín Abadi, K. Rustan, M. Leino, Martín Abadi, K. Rustan, M. Leino

A logic of object-oriented programs d i g i t a l

Report (1998)

David L. Detlefs, K. Rustan, M. Leino, Greg Nelson, David L. Detlefs, K. Rustan, ...

Wrestling with rep exposure

Checking Object Invariants (1997)

K. Rustan, K. Rustan, M. Leino, M. Leino, Raymie Stata, ...

When writing computer programs, programmers make assumptions about the relations among variables. In object-oriented programs, these assumptions include relations among the instance variables of a...

Specifying the Modification of Extended State (1997)

K. Rustan, K. Rustan, M. Leino, M. Leino

. This paper explores the interpretation of specifications in the context of an object-oriented programming language with subclassing and method overrides, for example like Java. In particular, the...

A Semantic Approach to Secure Information Flow (1997)

K. Rustan, K. Rustan, M. Leino, M. Leino, Rajeev Joshi, ...

A classic problem in security is the problem of determining whether a given program has secure information flow. Informally, this problem may be described as follows: Given a program operating on...

Recursive Object Types in a Logic of Object-Oriented Programs (1997)

Virginity: A contribution to the specification of object-oriented software (1997)

This paper formalizes a small object-oriented programming notation. The notation features imperative commands where objects can be shared (aliased), and is rich enough to allow subtypes and recursive...

K. Rustan, M. Leino, Raymie Stata

In object-oriented programs built in layers, an object at a higher level of abstraction is implemented by objects at lower levels of abstraction. It is usually crucial to correctness that a...

D I G I T a L (1997)

Systems Research Center, K. Rustan, M. Leino

This paper formalizes a small object-oriented programming notation. The notation features imperative commands where objects can be shared (aliased), and is rich enough to allow subtypes and recursive...

A Logic of Object-Oriented Programs (1997)

Mart'in Abadi, K. Rustan, M. Leino

. We develop a logic for reasoning about object-oriented programs. The logic is for a language with an imperative semantics and aliasing, and accounts for self-reference in objects. It is much like a...

A Logic of Object-Oriented Programs (1997)

Martín Abadi, K. Rustan, M. Leino

. We develop a logic for reasoning about object-oriented programs. The logic is for a language with an imperative semantics and aliasing, and accounts for self-reference in objects. It is much like a...

Checking object invariants (1997)

K. Rustan, M. Leino, Raymie Stata, K. Rustan, M. Leino, Raymie Stata

When writing computer programs, programmers make assumptions about the relations among variables. In object-oriented programs, these assumptions include relations among the instance variables of a...

Virginity: A contribution to the specification of (1997)

K. Rustan, M. Leino, Raymie Stata

object-oriented software

A Logic of Object-Oriented Programs (1997)

Martin Abadi, K. Rustan, M. Leino

We develop a logic for reasoning about object-oriented programs.

Ecstatic: An object-oriented programming language with an axiomatic (1996)

Conditional composition (1995)

semantics

Rajit Manohar, K. Rustan, M. Leino

Abstract. Generalizing the notion of function composition, we introduce the concept of conditional function composition and present a theory of such compositions. We use the theory to describe the...

Toward Reliable Modular Programs (1995)

A myth in the modular specification of programs (1995)

Software is being applied in an ever-increasing number of areas. Computer programs and systems are becoming more complex and consisting of more delicately interconnected components. Errors surfacing...