HOL-Boogie — An Interactive Prover for the Boogie (2009)
Sascha Böhme, K. Rustan, M. Leino, Burkhart Wolff
Abstract Boogie is a program verification condition generator for an imperative core language. It has front-ends for the programming languages C # and C enriched by annotations in first-order logic....
Specification and Verification of Object-Oriented Software (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...
A basis for verifying multi-threaded programs (2009)
K. Rustan, M. Leino, Peter Müller
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...
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...
Flexible Immutability with Frozen Objects (2009)
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)
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...
Reasoning about Comprehensions with First-Order SMT Solvers ABSTRACT (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...
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...
Object Invariants in Dynamic Contexts (2009)
K. Rustan, M. Leino, Peter Müller
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...
Julin, R, Juutinen, S, Antalic, S, Bianco, L, ...
For the first time, excited states in 185Pb have been observed in in-beam gamma-ray spectroscopic measurements using the recoil-decay tagging method. The resulting level scheme reveals a strongly...
Language Constructs and Features General Terms (2009)
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
First observation of excited states in 175Hg (2009)
Simpson, J, Scholey, C, Back, T, Greenlees, PT, Jakobsson, U, Jones, P, ...
Spectroscopy of the neutron-deficient nucleus 167Os91 (2009)
Grahn, T, Joss, DT, Simpson, J, Scholey, C, Andgren, K, Bianco, L, ...
Nuclear Physics News is supplied free of char... (2008)
T. Bressani, Torino S. Nagamiya, R. F. Casten, Yale A. Shotter, ...
Nuclear Physics News is published on behalf of the
Extended Static Checking: a Ten-Year Perspective (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...
Automatic Verification of Textbook Programs That Use (2008)
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
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. 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...
Ac Martín Abadi, Luca Cardelli, A Theory, Objects Springer, ...
[Ble79] Woodrow W. Bledsoe. A maximal method for set variables. Machine
ABSTRACT Class-Local Object Invariants (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...
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...
Abstract Data groups: Specifying the modification of extended state (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...
Verification of Equivalent-Results Methods (2008)
K. Rustan, M. Leino, Peter Müller
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...
Heap Monotonic Typestates (Extended Abstract) (2008)
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)
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...
A verification methodology for model fields (2008)
K. Rustan, M. Leino, Peter Müller
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...
Inferring Object Invariants (Extended Abstract) (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...
Loop invariants on demand (2008)
K. Rustan, M. Leino, Francesco Logozzo
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...
Using history invariants to verify observers (2008)
K. Rustan, M. Leino, Wolfram Schulte
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...
Inferring Object Invariants (Extended Abstract) (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...
Language Constructs and Features General Terms (2008)
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)
K. Rustan, M. Leino, Peter Müller
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)
K. Rustan, M. Leino, Wolfram Schulte
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...
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...
1 A Programming Model for Concurrent Object-Oriented Programs (2008)
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)
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
Report 160 Data abstraction and information hiding (2007)
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...
Cormac Flanagan, K. Rustan, M. Leino
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...
Extended Static Checking: a Ten-Year Perspective (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...
1 Annotation inference for modular checkers (2007)
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...
L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. R. Kiniry, G. T. Leavens, ...
An overview of JML tools and applications www.jmlspecs.org
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)
object-oriented programs
Coulomb shifts and shape changes in the mass 70 region (2007)
Singh, B. S. Nara, Steer, A. N., Jenkins, D. G., Wadsworth, R., Bentley, M. A., Davies, P. J., ...
The technique of recoil beta tagging has been developed which allows prompt gamma decays in nuclei from excited states to be correlated with electrons from their subsequent short-lived beta decay....
First observation of a rotational band in the odd-Z transfermium nucleus $^{251}_{101}Md$ (2007)
Chatillon, A., Theisen, C., Bouchez, E., Butler, P.A., Clément, E., Dorvaux, O., ...
A rotational band has been unambiguously observed in an odd-proton transfermium nucleus for the first time. An in-beam $\gamma$-ray spectroscopic study of $^{251}_{101}Md$ has been performed using...
Hydrogen molecule ion: Path integral Monte Carlo approach (2007)
Kylänpää, I., Leino, M., Rantala, T. T.
Path integral Monte Carlo approach is used to study the coupled quantum dynamics of the electron and nuclei in hydrogen molecule ion. The coupling effects are demonstrated by comparing differences in...
Alpha Decay of Re-159 and Proton Emission From Ta-155 (2007)
Page, R D, Bianco, L, Darby, I G, Uusitalo, J, Joss, D T, Grahn, T, ...
The alpha decay of Re-159 has been observed for the first time in reactions of 300 MeV Ni-58 ions with an isotopically enriched Cd-106 target. The Re-159 ions were separated in-flight using the RITU...
Investigation of nuclear collectivity in the neutron mid-shell nucleus Pb-186 (2007)
PAKARINEN, J, Hellemans, Veerle, JULIN, R, JUUTINEN, S, Heyde, Kristiaan, HEENEN, PH, ...
Coulomb shifts and shape changes in the mass 70 region (2007)
Nara Singh, B.S., Steer, A.N., Jenkins, D.G., Wadsworth, R., Bentley, M.A., Davies, P.J., ...
The technique of recoil beta tagging has been developed which allows prompt gamma decays in nuclei from excited states to be correlated with electrons from their subsequent short-lived beta decay....
Automatic verification of textbook programs (2007)
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
In-beam gamma ray and conversion electron study of 250 Fm (2006)
E. Bastin, J., Butler, P.A., Jones, G.D., Page, R.D., Jenkins, D.G., ...
We report on a set of in-beam studies of excited states in 250 Fm. We detected prompt gamma rays by using the JUROSPHERE IV array and conversion electrons by using the SACRED spectrometer. Both...
In-beam gamma ray and conversion electron study of 250 Fm (2006)
E. Bastin, J., Butler, P.A., Jones, G.D., Page, R.D., Jenkins, D.G., ...
We report on a set of in-beam studies of excited states in 250 Fm. We detected prompt gamma rays by using the JUROSPHERE IV array and conversion electrons by using the SACRED spectrometer. Both...
The Scientific Objectives of the SPIRAL2 project (2006)
Ackermann, D., Adoui, L., De Angelis, G., Auger, G., Aumann, T., Azaiez, F., ...
Chatillon, A., Theisen, Ch., Greenlees, P.T., Auger, G., Bastin, J.E., Bouchez, E., ...
The odd-Z isotope $^{255}$Lr and its daughter $^{251}$Md and grand-daughter $^{247}Es were studied in two experiments performed at GANIL and the University of Jyväskylä. The $^{255}$Lr nuclei were...
Chatillon, A., Theisen, Ch., Greenlees, P.T., Auger, G., Bastin, J.E., Bouchez, E., ...
The odd-Z isotope $^{255}$Lr and its daughter $^{251}$Md and grand-daughter $^{247}Es were studied in two experiments performed at GANIL and the University of Jyväskylä. The $^{255}$Lr nuclei were...
The Scientific Objectives of the SPIRAL2 project (2006)
Ackermann, D., Adoui, L., De Angelis, G., Auger, G., Aumann, T., Azaiez, F., ...
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...
Chatillon, A., Theisen, Ch., Greenlees, P.T., Auger, G., Bastin, J.E., Bouchez, E., ...
The odd-Z isotope $^{255}$Lr and its daughter $^{251}$Md and grand-daughter $^{247}Es were studied in two experiments performed at GANIL and the University of Jyväskylä. The $^{255}$Lr nuclei were...
The Scientific Objectives of the SPIRAL2 project (2006)
Ackermann, D., Adoui, L., De Angelis, G., Auger, G., Aumann, T., Azaiez, F., ...
Chatillon, A., Theisen, Ch., Greenlees, P.T., Auger, G., Bastin, J.E., Bouchez, E., ...
The odd-Z isotope $^{255}$Lr and its daughter $^{251}$Md and grand-daughter $^{247}Es were studied in two experiments performed at GANIL and the University of Jyväskylä. The $^{255}$Lr nuclei were...
The Scientific Objectives of the SPIRAL2 project (2006)
Ackermann, D., Adoui, L., De Angelis, G., Auger, G., Aumann, T., Azaiez, F., ...
Probing the shapes of Pb-186 (2006)
PAKARINEN, J, DARBY, IG, EECKHAUDT, S, ENQVIST, T, GRAHN, T, GREENLEES, PT, ...
America, and Asia. Editor: Gabriele-Elisabeth Körner Editorial Board (2006)
R. F. Casten, Yale S. Nagamiya, A. Eiró, Lisbon H. Ströher, M. Leino
Nuclear Physics News is published on behalf of the
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...
Joss, D.T., Amzal, N., Appelbe, D.E., Back, T., Bentley, M.A., Cederwall, B., ...
In recent years, the exploitation of the recoil-decay tagging (RDT) technique with large arrays of germanium detectors has revealed much information about the structure of heavy nuclei approaching...
Kivimäki, M., Davey Smith, G., Juonala, M., Ferrie, J.E., Keltikangas-Järvinen, L., Elovainio, M., ...
Objective: To examine the association of childhood socioeconomic position (SEP) with adult cardiovascular risk factors, vascular structure, and vascular function in a contemporary population of young...
In-beam and decay spectroscopy of transfermium elements (2005)
Greenlees, P.T., Amzal, N., Bastin, J.E., Bouchez, E., Butler, P.A., Chatillon, A., ...
Over the past few years a great deal of new spectroscopic data has been obtained for transfermium nuclei. Recoil separators, coupled with modern target position and focal-plane spectrometers, allow...
Application of ultra-fast timing techniques to the study of exotic and weakly produced nuclei (2005)
Mach, H., M Walker, P., Julin, R., Leino, M., Juutinen, S., Stanoiu, M., ...
Ultra-fast time-delayed techniques have been recently applied in a number of studies where exotic nuclei were identified using advanced selection techniques. These include large Compton-suppressed Ge...
In-beam and decay spectroscopy of transfermium elements (2005)
Greenlees, P.T., Amzal, N., Bastin, J.E., Bouchez, E., Butler, P.A., Chatillon, A., ...
Over the past few years a great deal of new spectroscopic data has been obtained for transfermium nuclei. Recoil separators, coupled with modern target position and focal-plane spectrometers, allow...
Application of ultra-fast timing techniques to the study of exotic and weakly produced nuclei (2005)
Mach, H., M Walker, P., Julin, R., Leino, M., Juutinen, S., Stanoiu, M., ...
Ultra-fast time-delayed techniques have been recently applied in a number of studies where exotic nuclei were identified using advanced selection techniques. These include large Compton-suppressed Ge...
Evidence for oblate structure in Pb-186 (2005)
PAKARINEN, J, DARBY, IG, EECKHAUDT, S, ENQVIST, T, GRAHN, T, GREENLEES, PT, ...
Loop invariants on demand (2005)
K. Rustan, M. Leino, Francesco Logozzo
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) (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...
Safe Concurrency for Aggregate Objects with Invariants (2005)
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)
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...
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...
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)
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...
– Conceptually elegant Clarkson: Extended Static Checking 5 Authors Author (2005)
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:...
gamma-ray spectroscopy of Bi-191,Bi-193 (2004)
Juutinen, S, Cocks, JFC, Dorvaux, O, Eskola, K, ...
Prompt and delayed gamma rays from Bi-191,Bi-193 have been identified using the recoil-decay tagging, isomer tagging, and recoil gating techniques, resulting in extensive level schemes for both...
First identification of gamma-ray transistions in 107Te (2004)
Hadinia, B, Cederwall, B, Lagergren, K, Blomqvist, J, Bäck, T, Eeckhaudt, S, ...
Alpha decay and recoil decay tagging studies of 183Tl (2004)
Raddon, PM, Jenkins, DG, OLeary, CD, Simons, AJ, Wadsworth, R, Andreyev, AN, ...
Recoil decay tagging of gamma-rays in the extremely neutron-deficient nucleus 162Os (2004)
Joss, DT, Lagergren, K, Appelbe, DE, Barton, CJ, Simpson, J, Cederwall, B, ...
$\gamma$-ray spectroscopy of $^{191,193}$ Bi (2004)
Nieminen, P., Juutinen, S., Andreyev, A.N., Cocks, J.F.C., Dorvaux, O., Eskola, K., ...
$\gamma$-ray spectroscopy of $^{191,193}$ Bi (2004)
Nieminen, P., Juutinen, S., Andreyev, A.N., Cocks, J.F.C., Dorvaux, O., Eskola, K., ...
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...
The Spec# programming system: An overview (2004)
Mike Barnett, K. Rustan, M. Leino, Wolfram Schulte
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...
The Spec# programming system: An overview (2004)
Mike Barnett, K. Rustan, M. Leino, Wolfram Schulte
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 #...
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...
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)
K. Rustan, M. Leino, Peter Müller
Object invariants describe the consistency of object-oriented data structures and are central to reasoning about the correctness of object-oriented software.
An overview of JML tools and applications (2004)
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...
The Spec# programming system: An overview (2004)
Mike Barnett, K. Rustan, M. Leino, Wolfram Schulte
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 #...
The Spec# programming system: An overview (2004)
Mike Barnett, K. Rustan, M. Leino, Wolfram Schulte
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)
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)
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...
Pulkki, L., Kivimäki, M., Keltikangas-Järvinen, L., Elovainio, M., Leino, M., Viikari, J.
Background: The role of early personality in socioeconomic inequalities in health is not well understood. We investigated the extent to which type A components in adolescence and early adulthood...
Van De Vel, Karen; U0031962, Page, RD, Kettunen, H, Greenlees, PT, Jones, P, ...
Gamma rays from excited states of Po-190 have been observed using I the Jurosphere Ge-detector array coupled to the RITU gas-filled separator. They were associated with a collective band which from...
Gamma-ray spectroscopy of very neutron-deficient Bi isotopes (2003)
Nieminen, P., Juutinen, S., Cocks, J.F., Dorvaux, O., Enqvist, T., Grahn, T., ...
Gamma-ray spectroscopy of very neutron-deficient Bi isotopes (2003)
Nieminen, P., Juutinen, S., Cocks, J.F., Dorvaux, O., Enqvist, T., Grahn, T., ...
Strongly coupled bands in the neutron-deficient nucleus Re-167 (2003)
Joss, DT, Simpson, J, Paul, ES, Page, RD, Amzal, N, Applebe, DE, ...
alpha-decay spectroscopy of light odd-odd Bi isotopes - I: Bi-188,Bi-190 nuclei (2003)
ANDREYEV, AN, ACKERMANN, D, ANTALIC, S, BOARDMAN, H, CAGARDA, P, GERL, J, ...
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...
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)
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...
Heap Monotonic Typestates (Extended Abstract) (2003)
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...
alpha-decay spectroscopy of light odd-odd Bi isotopes - I: ^{188,190}Bi nuclei (2003)
Ackermann, D, Antalic, S, Boardman, H J, Cagarda, P, Gerl, J, ...
Detailed fine-structure a-decay studies of Bi-188,Bi-190 were performed using the complete-fusion reactions of Cr-50,Cr-52 ions with a Nd-142 target at the velocity filter SHIP. The evaporation...
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...
Andreyev, Andrei; U0055520, Huyse, Marc; U0013345, Van De Vel, Karen; U0031962, Van Duppen, Pieter; U0010286, Dorvaux, O, Greenlees, P, ...
Prompt gamma rays have been observed for the first time from the neutron-deficient nucleus Po-191 using the recoil-decay tagging technique at the RITU gas-filled separator. In addition improved alpha...
Identification of low-lying proton-based intruder states in Pb189-193 (2002)
Van De Vel, Karen; U0031962, Andreyev, Andrei; U0055520, Huyse, Marc; U0013345, Van Duppen, Pieter; U0010286, Cocks, JFC, Dorvaux, O, ...
Low-lying proton-based intruder states have been observed in the odd-mass isotopes Pb-189,Pb-191,Pb-193 in experiments at the RITU gas-filled recoil separator. The identification has been performed...
Yrast spectroscopy in the neutron deficient nucleus Os-169 (2002)
Joss, DT, Simpson, J, Page, RD, King, SL, Amzal, N, Appelbe, DE, ...
Spectroscopy of tranferium nuclei: $^{252}$No (2002)
Herzberg, R-D., Amzal, N., Becker, F., Butler, P.A., Chewter, A.J.C., Cocks, J.F.C., ...
In-beam spectroscopy of $^{253,254}$No (2002)
Herzberg, R-D., Amzal, N., Bastin, J.E., Becker, F., Brew, P.M.T., Butler, P.A., ...
Spectroscopy of tranferium nuclei: $^{252}$No (2002)
Herzberg, R-D., Amzal, N., Becker, F., Butler, P.A., Chewter, A.J.C., Cocks, J.F.C., ...
In-beam spectroscopy of $^{253,254}$No (2002)
Herzberg, R-D., Amzal, N., Bastin, J.E., Becker, F., Brew, P.M.T., Butler, P.A., ...
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...
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...
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...
In-beam studies of very neutron-deficient heavy nuclei (2002)
Greenlees, P T, Helariutta, K, Jones, P, Juutinen, S, Leppanen, A P, ...
Alpha decay studies of translead nuclei at the proton drip line (2001)
Uusitalo, J, Kettunen, H, Andreyev, Andrei; U0055520, Eskola, K, Greenlees, PT, Helariutta, K, ...
Extensive alpha -decay studies of the very neutron deficient isotopes Po-191, Rn-195, and Rn-196 have been performed at the RITU gas-filled recoil separator. The recoil-alpha-(alpha) correlation...
Recoil isomer tagging in the proton-rich odd-odd N=77 isotones, 65142Tb and 67144Ho (2001)
Scholey, C., Cullen, D. M., Paul, E. S., Boston, A. J., Butler, P. A., Enqvist, T., ...
Weissman, L, Ackermann, D, Gerl, J, ...
Two excited J(pi)=0(+) states in Pb-186 populated in the a-decay of Po-190 have been identified through alpha -particle/conversion electron coincidences in an experiment at the velocity filter SHIP....
First observation of excited states in the neutron deficient N=86 isotones Ta-159 and W-160 (2001)
Keenan, A, Page, RD, Simpson, J, Amzal, N, Cocks, JFC, Cullen, DM, ...
Isomer spectroscopy in $^{216}_{90}$Th$_{126}$ and the magicity of $^{218}_{92}$U$_{126}$ (2001)
Hauschild, K., Rejmund, M., Grawe, H., Caurier, E., Nowacki, F., Becker, F., ...
Isomer spectroscopy in $^{216}_{90}$Th$_{126}$ and the magicity of $^{218}_{92}$U$_{126}$ (2001)
Hauschild, K., Rejmund, M., Grawe, H., Caurier, E., Nowacki, F., Becker, F., ...
Houdini, an Annotation Assistant for ESC/Java (2001)
Cormac Flanagan, K. Rustan, M. Leino
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...
Houdini, an Annotation Assistant for ESC/Java (2001)
Cormac Flanagan, K. Rustan, M. Leino
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)
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...
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)
Cormac Flanagan, K. Rustan, M. Leino
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...
Houdini, an Annotation Assistant for ESC/Java (2001)
Cormac Flanagan, K. Rustan, M. Leino
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...
A triplet of differently shaped spin-zero states in the atomic nucleus Pb-186 (2000)
Weissman, L, Ackermann, D, Gerl, J, ...
Understanding the fundamental excitations of many-fermion systems is of significant current interest. In atomic nuclei with even numbers of neutrons and protons, the low-lying excitation spectrum is...
First observation of excited states in the neutron deficient nuclei Os-164 and Os-166 (2000)
King, SL, Page, RD, Simpson, J, Kennan, A, Amzal, N, Chewter, AJ, ...
Excited states have been observed for the first time in the neutron deficient nuclei Os-166 and Os-164. The nuclei were produced using the reactions Cd-106(Cu-63,p2n) Os-166, Sn-112(Ni-58,2p,2n)...
A triplet of differently shaped spin-zero states in the atomic nucleus Pb-186. (2000)
ANDREYEV, AN, HUYSE, M, VAN DUPPEN, P, WEISSMAN, L, ACKERMANN, D, GERL, J, ...
JML: notations and tools supporting detailed design in Java (2000)
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...
Bijnens, N, Leino, M, Enqvist, T, ...
By using complete fusion reactions S-32+ Er-164 and Ti-48+ Sm-144, leading to Po-196 and Po-192 compound nuclei, improved alpha-decay characteristics for neutron-deficient Po-190,Po-192 isotopes have...
Hindered (Delta l=0) alpha decay and shape staggering in Po-191 (1999)
Cocks, JFC, Helariutta, K, Kettunen, H, ...
Two alpha-decaying isomeric states were observed in Po-191 with E-alpha = 7334(10) keV and T-1/2 = 22(1) ms for Po-191g and E-alpha = 7378(10) keV and T-1/2 = 98(8) ms for Po-191m. Evidence was found...
Electromagnetic transitions and $\alpha$ decay of the $^{223}$Pa nucleus (1999)
Hoellinger, F., Gall, B.J.P., Schulz, N., Amzal, N., Butler, P.A., Greenlees, P.T., ...
Actinides with N~132 present the best explored region of pear shape nuclei. Still almost no spectroscopic information is available for the heaviest elements, Z=9198, which are predicted to be...
Recoil decay tagging studies of onset of collectivity near the Z=82 shell gap (1999)
Juutinen, S., Cocks, J.F.C., Dorvaux, O., Greenlees, P.T., Jones, P., Julin, R., ...
Excited states in the heavy nuclide $^{254}$No (1999)
Kankaanpaa, H., Leino, M., Chewter, A.J., Hessberger, F.P., Le Coz, Y., ...
The onset of deformation in neutron-deficient At nuclei (1999)
Smith, M.B., Chapman, R., Cocks, J.F.C., Dorvaux, O., Helariutta, K., Jones, P.M., ...
Indication of triple-shape coexistence in $^{188}$Pb (1999)
Le Coz, Y., Becker, F., Kankaanpaa, H., Korten, W., Mergel, E., Butler, P.A., ...
Fine structure in the $\alpha$ decay of $^{191,g,m}$Bi and $^{193,g,m}$Bi (1999)
Kettunen, H., Cocks, J.F.C., Andreyev, A.N., Dorvaux, O., Eskola, K., Greenlees, P.T., ...
Experimental identification of intruder bandheads in odd-mass $^{187-193}$Pb (1999)
Andreyev, A.N., Cocks, J.F.C., Dorvaux, O., Eskola, K., Greenlees, P., Jones, P., ...
In-beam and decay studies of neutron-deficient isotopes of heavy elements (1999)
Leino, M., Allatt, R.G., Cocks, J.F.C., Dorvaux, O., Eskola, K., Greenlees, P.T., ...
Decay and in-beam studies of neutron-deficient Po and Ra isotopes at JYFL (1999)
Leino, M., Allatt, R.G., Andreyev, A.N., Cocks, J.F.C., Dorvaux, O., Enqvist, T., ...
In-beam study of $^{254}$No (1999)
Leino, M., Kankaanpaa, H., Herzberg, R.D., Chewter, A.J., Hessberger, F.P., Le Coz, Y., ...
Identification of excited states in $^{226}$U: evidence for octupole deformation (1999)
Greenlees, P.T., Amzal, N., Andreyev, A., Butler, P.A., Cann, K.J., Cocks, J.F.C., ...
Identification of excited states in $^{226}$U (1999)
Greenlees, P.T., Amzal, N., Butler, P.A., Cann, K.J., Cocks, J.F.C., Howcroft, D., ...
Competition of fission with the population of the yrast superdeformed band in $^{194}$Pb (1999)
Deloncle, I., Porquet, M.G., Bauchet, A., Azaiez, F., Belleguic, M., Gall, B., ...
Fine structure in the alpha decays of $^{226}$U and $^{230}$Pu (1999)
Greenlees, P.T., Kuusiniemi, P., Amzal, N., Andreyev, A., Butler, P.A., Cann, K.J, ...
High-spin states in $^{205}$Rn: A new shears band structure? (1999)
Novak, J.R., Beausang, C.W., Amzal, N., Casten, R.F., Cata Danil, G., Cocks, J.F.C., ...
Electromagnetic transitions and $\alpha$ decay of the $^{223}$Pa nucleus (1999)
Hoellinger, F., Gall, B.J.P., Schulz, N., Amzal, N., Butler, P.A., Greenlees, P.T., ...
Actinides with N~132 present the best explored region of pear shape nuclei. Still almost no spectroscopic information is available for the heaviest elements, Z=9198, which are predicted to be...
Recoil decay tagging studies of onset of collectivity near the Z=82 shell gap (1999)
Juutinen, S., Cocks, J.F.C., Dorvaux, O., Greenlees, P.T., Jones, P., Julin, R., ...
Excited states in the heavy nuclide $^{254}$No (1999)
Kankaanpaa, H., Leino, M., Chewter, A.J., Hessberger, F.P., Le Coz, Y., ...
The onset of deformation in neutron-deficient At nuclei (1999)
Smith, M.B., Chapman, R., Cocks, J.F.C., Dorvaux, O., Helariutta, K., Jones, P.M., ...
Indication of triple-shape coexistence in $^{188}$Pb (1999)
Le Coz, Y., Becker, F., Kankaanpaa, H., Korten, W., Mergel, E., Butler, P.A., ...
Fine structure in the $\alpha$ decay of $^{191,g,m}$Bi and $^{193,g,m}$Bi (1999)
Kettunen, H., Cocks, J.F.C., Andreyev, A.N., Dorvaux, O., Eskola, K., Greenlees, P.T., ...
Experimental identification of intruder bandheads in odd-mass $^{187-193}$Pb (1999)
Andreyev, A.N., Cocks, J.F.C., Dorvaux, O., Eskola, K., Greenlees, P., Jones, P., ...
In-beam and decay studies of neutron-deficient isotopes of heavy elements (1999)
Leino, M., Allatt, R.G., Cocks, J.F.C., Dorvaux, O., Eskola, K., Greenlees, P.T., ...
Decay and in-beam studies of neutron-deficient Po and Ra isotopes at JYFL (1999)
Leino, M., Allatt, R.G., Andreyev, A.N., Cocks, J.F.C., Dorvaux, O., Enqvist, T., ...
In-beam study of $^{254}$No (1999)
Leino, M., Kankaanpaa, H., Herzberg, R.D., Chewter, A.J., Hessberger, F.P., Le Coz, Y., ...
Identification of excited states in $^{226}$U: evidence for octupole deformation (1999)
Greenlees, P.T., Amzal, N., Andreyev, A., Butler, P.A., Cann, K.J., Cocks, J.F.C., ...
Identification of excited states in $^{226}$U (1999)
Greenlees, P.T., Amzal, N., Butler, P.A., Cann, K.J., Cocks, J.F.C., Howcroft, D., ...
Competition of fission with the population of the yrast superdeformed band in $^{194}$Pb (1999)
Deloncle, I., Porquet, M.G., Bauchet, A., Azaiez, F., Belleguic, M., Gall, B., ...
Fine structure in the alpha decays of $^{226}$U and $^{230}$Pu (1999)
Greenlees, P.T., Kuusiniemi, P., Amzal, N., Andreyev, A., Butler, P.A., Cann, K.J, ...
High-spin states in $^{205}$Rn: A new shears band structure? (1999)
Novak, J.R., Beausang, C.W., Amzal, N., Casten, R.F., Cata Danil, G., Cocks, J.F.C., ...
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...
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...
First observation of excited states in the neutron deficient nuclei (PT)-P-168 and Pt-170 (1998)
King, SL, Simpson, J, Page, RD, Amzal, N, Back, T, Cederwall, B, ...
First observation of excited states in the neutron deficient nuclei $^{168}$Pt and $^{170}$Pt (1998)
King, S.L., Simpson, J., Page, R.D., Amzal, N., Back, T., Cederwall, B., ...
Nuclear structure information from recoil decay tagging experiments (1998)
Leino, M., Julin, R., Cocks, J.F.C., Butler, P.A., Dorvaux, O., Eskola, K., ...
First observation of excited states in $^{226}$U (1998)
Greenlees, P-T., Amzal, N., Butler, P-A., Cann, K-J., Cocks, J-F-C., Hawcroft, D., ...
First observation of excited states in the neutron deficient nuclei $^{168}$Pt and $^{170}$Pt (1998)
King, S.L., Simpson, J., Page, R.D., Amzal, N., Back, T., Cederwall, B., ...
Nuclear structure information from recoil decay tagging experiments (1998)
Leino, M., Julin, R., Cocks, J.F.C., Butler, P.A., Dorvaux, O., Eskola, K., ...
First observation of excited states in $^{226}$U (1998)
Greenlees, P-T., Amzal, N., Butler, P-A., Cann, K-J., Cocks, J-F-C., Hawcroft, D., ...
Collective rotational vibrational transition in the very neutron-deficient nuclei 171,172Pt (1998)
Cederwall, B, Back, T, Bark, R, Odergard, S, King, SL, Simpson, J, ...
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)
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...
Data groups: Specifying the modification of extended state (1998)
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)
. 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...
Recursive Object Types In A Logic Of Object-Oriented Programs (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...
David L. Detlefs, K. Rustan, M. Leino, Greg Nelson, David L. Detlefs, K. Rustan, ...
Wrestling with rep exposure
Extended static checking (1998)
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
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
David L. Detlefs, K. Rustan, M. Leino, Greg Nelson, David L. Detlefs, K. Rustan, ...
Wrestling with rep exposure
Alpha-decay characteristics of neutron-deficient Po-190, Bi-189 and Pb-186 isotopes (1997)
Bijnens, N, Enqvist, T, Kuusiniemi, P, Leino, M, ...
The neutron-deficient Po-190 and Bi-189 isotopes have been produced in the 2n respectively p2n channels of the Ti-48 + Sm-144 reaction. Cross sections for different reaction channels are given. For...
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)
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...
Virginity: A contribution to the specification of object-oriented software (1997)
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...
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.
Conditional composition (1995)
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)
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...
A myth in the modular specification of programs (1995)
When writing specifications of modular programs, two crucial elements are abstraction and clauses. Without abstraction, information hiding is not possible; without clauses, a specification must...
Production and decay of $^{269}$110 (1994)
Hofmann, S, Ninov, N, Hessberger, F P, Armbruster, P, Folger, H, Münzenberg, G, ...
Separation of actinide-made transurania by a gas-filled magnetic separator (1994)
Ninov, V, Armbruster, P, Hessberger, F P, Hofmann, S, Münzenberg, G, Fujita, Y, ...
Multicomputer Programming with Modula-3D (1993)
Rustan Leino, K. Rustan, M. Leino
In this note, we extend an object-oriented language to support programming fine-grain multicomputers. The new constructs have a simple semantics and provide a nice way to write distributed programs....
Aysto, J., Astier, A., Enqvist, T., Eskola, K., Janas, Z., Jokinen, A., ...
Aysto, J., Astier, A., Enqvist, T., Eskola, K., Janas, Z., Jokinen, A., ...
Proof of a mutual exclusion algorithm by Haldar and Subramanian. (1991)
H. Peter Hofstee, K. Rustan, M. Leino
Introduction We present a proof of a mutual exclusion algorithm by Haldar and Subramanian [1]. The original operational reasoning did not convince us of the correctness of the algorithm and even...
A semantic approach to secure information flow (1422)
K. Rustan, K. Rustan, M. Leino, M. Leino, Rajeev Joshi, 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...
A semantic approach to secure information flow (1422)
K. Rustan, K. Rustan, M. Leino, M. Leino, Rajeev Joshi, 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...