The SLam calculus is a typed-calculus that maintains security information as well as type information. The type system propagates security information for each objectinfourforms: the object's...
Journal of Functional Programming, 1(4):375–416, 1991a. Summary in (2008)
Anindya Banerjee, Nevin Heintze, Luca Cardelli, Luca Cardelli, Benjamin Pierce
Abadi, Martín and Luca Cardelli. On subtyping and matching. In European Conference
Summer Intern San Mateo, CA (2008)
Olivier Tardieu, Supervisors Dr, Nevin Heintze, Prof David, B. Macqueen
Developed programming languages and models for the design of heterogeneous embedded systems.
A General Framework for Program Reasoning (2007)
Nevin Heintze, R Azvan Voicu, Joxan Jaffar, Joxan Jaffar
We present a framework for reasoning about programs that incorporates programmer specified assertions and subsumes both Hoare-Logic verification and program analysis. Our aim is to support...
A Generic Algorithm for CLP Analysis (2007)
Exte Nd Ed, Extended Abstract, Nevin Heintze, Joxan Jaffar
) Nevin Heintze y and Joxan Jaffar z June 13, 1995 Logic program analyzers typically employ abstract interpretation and consist of two main components: an abstract domain and a generic iterative...
A Decision Procedure for a Class of Set Constraints (Extended Abstract) (2007)
N. Heintze, J. Jaffar, Nevin Heintze, Joxan Jaffar
) Nevin Heintze School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213 (nch@cs.cmu.edu) Joxan Jaffar IBM T.J. Watson Research Center P.O. Box 218 Yorktown Heights, NY 10598...
Set-Based Analysis of ML Programs (Extended Abstract) (2007)
) Nevin Heintze y School of Computer Science Carnegie Mellon University nch@cs.cmu.edu Abstract Reasoning about program variables as sets of "values" leads to a simple, accurate and...
Propagation for Program Reasoning (2007)
We present an abstract algorithm for propagating assertions through a program. Its key feature is an integration of key concepts of program reasoning such as weakest preconditions, strongest...
Set Based Analysis of Arithmetic (2006)
Set based analysis is an approach to compile-time program analysis that is based on a simple approximation: all dependencies between variables are ignored. In effect, program variables are treated as...
ML Partial Evaluation Using Set-Based Analysis (2006)
Malmkjaer, Karoline, Heintze, Nevin, Danvy, Oliver
We describe the design and implementation of an off-line partial evaluator for Standard ML programs. Our partial evaluator consists of two phases: analysis and specialization. Analysis: Set-based...
Zhenjiang Hu, Shin-cheng Mu, Nevin Heintze, Julia Lawall, Michael Leuschel, Peter Sestoft
Abstract. This paper presents an application of bidirectional transformations to design and implementation of a novel editor supporting interactive refinement in the development of structured...
Zhenjiang Hu, Shin-cheng Mu, Nevin Heintze, Julia Lawall, Michael Leuschel, Peter Sestoft
Abstract. This paper presents an application of bidirectional transformation to the design and implementation of a novel editor supporting interactive refinement in the development of structured...
Ultra-fast aliasing analysis using CLA: a million lines of C code in a second (2001)
We describe the design and implementation of a system for very fast points-to analysis. On code bases of about a million lines of unpreprocessed C code, our system performs eldbased Andersen-style...
A Framework for Combining Analysis and Verification (2000)
Nevin Heintze, Razvan Voicu, Joxan Jaffar, Joxan Jaffar
interpretation using this domain infers that x0, y0 are even at the end of the loop, although it cannot infer anything about x, y. Combining the results from the Hoare-style reasoner with this...
A Framework for Combining Analysis and Verification (2000)
Nevin Heintze, Joxan Jaffar, Razvan Voicu
We present a general framework for combining program verification and program analysis. This framework enhances program analysis because it takes advantage of user assertions, and it enhances program...
Region analysis and the polymorphic lambda calculus (1999)
Anindya Banerjee, Nevin Heintze, Jon G. Riecke
We show how to translate the region calculus of Tofte and Talpin, a typed lambda calculus that can statically delimit the lifetimes of objects, into an extension of the polymorphic lambda calculus...
Region analysis and the polymorphic lambda calculus (1999)
Anindya Banerjee, Nevin Heintze, Jon G. Riecke
We show how to translate the region calculus of Tofte and Talpin, a typed lambda calculus which can statically delimit the lifetimes of objects, into an extension of the polymorphic lambda calculus...
A Core Calculus of Dependency (1999)
Martn Abadi Systems, Martn Abadi, Anindya Banerjee, Nevin Heintze, Jon G. Riecke
Notions of program dependency arise in many settings: security, partial evaluation, program slicing, and call-tracking. We argue that there is a central notion of dependency common to these settings...
A Core Calculus of Dependency (1999)
Martín Abadi, Anindya Banerjee, Nevin Heintze, Jon G. Riecke
Notions of program dependency arise in many settings: security, partial evaluation, program slicing, and call-tracking. We argue that there is a central notion of dependency common to these settings...
A Core Calculus of Dependency (1999)
Martn Abadi Systems, Martn Abadi, Anindya Banerjee, Nevin Heintze, Jon G. Riecke
Notions of program dependency arise in many settings: security, partial evaluation, program slicing, and call-tracking. We argue that there is a central notion of dependency common to these settings...
Region Analysis and the Polymorphic Lambda Calculus (1999)
Anindya Banerjee, Nevin Heintze, Jon G. Riecke
We show how to translate the region calculus of Tofte and Talpin, a typed lambda calculus which can statically delimit the lifetimes of objects, into an extension of the polymorphic lambda calculus...
Set Based Program Analysis. (1998)
The central component of standard approaches to compile-time program analysis is an abstract domain for approximating program values. Importantly, the domain must be chosen so that an iterative fixed...
Set Based Analysis of ML Programs, (1998)
Reasoning about a program by treating program variables as sets of values leads to a simple, accurate and intuitively appealing notion of program approximation. This paper presents such an approach...
Control-Flow Analysis and Type Systems, (1998)
We establish a series of equivalences between type systems and control-flow analyses. Specifically, we take four type systems from the literature (involving simple types, subtypes and recursion) and...
The SLam Calculus: Programming with Secrecy and Integrity (1998)
The SLam calculus is a typed -calculus that maintains security information as well as type information. The type system propagates security information for each object in four forms: the...
The SLam Calculus: Programming with Secrecy and Integrity (1998)
We describe the SLam calculus, a typed -calculus that maintains security information as well as type information. The type system propagates both secrecy and integrity, maintaining four distinct...
The SLam Calculus: Programming with Security and Integrity (1998)
We describe the SLam calculus, a typed -calculus that maintains security information as well as type information. The calculus maintains four different forms of security information: which agents...
Subtransitive CFA using Types (1998)
Bratin Saha, Bratin Saha, Nevin Heintze, Nevin Heintze, Dino Oliva, Dino Oliva
We present an experimental evaluation of Heintze and McAllester's linear-time subtransitive CFA algorithm, in the context of SML/NJ v110.7. As described in [9], linear-time termination of the...
Cryptographic Postage Indicia, (1997)
Tygar, J. D., Yee, Bennet, Heintze, Nevin
We apply cryptographic techniques to the problem of fraud in metered mail. We describe a mail system that combines off-the-shelf barcode technology, tamper-proof devices, and cryptography in a...
Linear-time Subtransitive Control Flow Analysis (1997)
Nevin Heintze, David Mcallester
We present a linear-time algorithm for boundedtype programs that builds a directed graph whose transitive closure gives exactly the results of the standard (cubic-time) Control-Flow Analysis (CFA)...
On the Cubic Bottleneck in Subtyping and Flow Analysis (1997)
Nevin Heintze, David Mcallester
A variety of program analysis methods have worst case time complexity that grows cubicly in the length of the program being analyzed. Cubic complexity typically arises in control flow analyses and...
On the Complexity of Set-Based Analysis (1997)
David Mcallester, Nevin Heintze
: We formally define the set-based abstraction of any language whose operational semantics can be defined by environment evaluation. The Aiken-Wimmers soft type system precisely corresponds to this...
On the Complexity of Set-Based Analysis (1997)
Nevin Heintze, David Mcallester
: We define a general notion of set-based analysis --- any language whose operational semantics is defined by environment evaluation has a well defined set-based abstraction. This general definition...
On the Cubic Bottleneck in Subtyping and Flow Analysis (1997)
Nevin Heintze, David Mcallester
We prove that certain data-flow and control-flow problems are 2NPDA-complete. This means that these problems are in the class 2NPDA and that they are hard for that class. The fact that they are in...
Cryptographic postage indicia (1996)
J. D. Tygar, Bennet S. Yee, Nevin Heintze
Abstract. Metered mail provides substantial opportunities for fraud. (Indeed, losses due to meter fraud in the United States are said to exceed $100 million annually.) We apply cryptographic...
Designing cryptographic postage indicia (1996)
J. D. Tygar, Bennet Yee, Nevin Heintze
We apply cryptographic techniques to the problem of fraud in metered mail. We describeamail system that combines o-the-shelf barcode technology, tamper-proof devices, and cryptography in a...
Designing cryptographic postage indicia (1996)
J. D. Tygar, Bennet Yee, Nevin Heintze
We apply cryptographic techniques to the problem of fraud in metered mail. We describeamail system that combines o-the-shelf barcode technology, tamper-proof devices, and cryptography in a...
Designing Cryptographic Postage (1996)
J. D. Tygar, Bennet Yee, Nevin Heintze
This research was partially supported by the US Postal Service. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the...
Model checking electronic commerce protocols (1996)
Nevin Heintze, J. D. Tygar, Jeannette Wing, H. Chi Wong
The paper develops model checking techniques to examine NetBill and Digicash. We show how model checking can verify atomicity properties by analyzing simpli ed versions of these protocols that retain...
Cryptographic postage indicia (1996)
J. D. Tygar, Bennet S. Yee, Nevin Heintze
Abstract. Metered mail provides substantial opportunities for fraud. (Indeed, losses due to meter fraud in the United States are said to exceed $100 million annually.) We apply cryptographic...
Designing cryptographic postage indicia (1996)
J. D. Tygar, Bennet Yee, Nevin Heintze
We apply cryptographic techniques to the problem of fraud in metered mail. We describe a mail system that combines off-the-shelf barcode technology, tamper-proof devices, and cryptography in a...
Designing cryptographic postage indicia (1996)
J. D. Tygar, Bennet Yee, Nevin Heintze
We apply cryptographic techniques to the problem of fraud in metered mail. We describe a mail system that combines off-the-shelf barcode technology, tamper-proof devices, and cryptography in a...
Designing Cryptographic Postage (1996)
J. D. Tygar, Bennet Yee, Nevin Heintze
This research was partially supported by the US Postal Service. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the...
Cryptographic postage indicia (1996)
J. D. Tygar, Bennet S. Yee, Nevin Heintze
Metered mail provides substantial opportunities for fraud. (Indeed, losses due to meter fraud in the United States are said to exceed $100 million annually.) We apply cryptographic techniques to...
Model checking electronic commerce protocols (1996)
Nevin Heintze, Nevin Heintze, J. D. Tygar, Jeannette Wing, H. Chi Wong
The paper develops model checking techniques to examine NetBill and Digicash. We show how model checking can verify atomicity properties by analyzing simplified versions of these protocols that...
A Model for Secure Protocols and Their Compositions (1996)
This paper develops a foundation for reasoning about protocol security. We adopt a model-based approach for defining protocol security properties. This allows us to describe security properties in...
Scalable Document Fingerprinting (1996)
) Nevin Heintze Bell Laboratories Murray Hill, NJ 07974 nch@research.bell-labs.com Abstract As more information becomes available electronically, document search based on textual similarity is...
Model Checking Electronic Commerce Protocols (Extended Abstract) (1996)
Nevin Heintze, J. D. Tygar, Jeannette Wing, H. C. Wong
The paper develops model checking techniques to examine NetBill and Digicash. We show how model checking can find atomicity problems by analyzing simplified versions of these protocols that retain...
A Model for Secure Protocols and Their Compositions (Extended Abstract) (1996)
We give a formal model of protocol security. Our model allows us to reason about the security of protocols, and considers issues of beliefs of agents, time, and secrecy. We prove a composition...
A Model for Secure Protocols and Their Compositions (Extended Abstract) (1996)
We give a formal model of protocol security. Our model allows us to reason about the security of protocols, and considers issues of beliefs of agents, time, and secrecy. We prove a composition...
Cryptographic Postage Indicia (1996)
Tygar And Bennet, J. D. Tygar, Bennet Yee, Nevin Heintze
We apply cryptographic techniques to the problem of fraud in metered mail. We describe a mail system that combines off-the-shelf barcode technology, tamper-proof devices, and cryptography in a...
Control-Flow Analysis for ML in Linear Time (1996)
Nevin Heintze, David Mcallester
Standard control-flow analysis (often called 0-CFA) is thought to be a cubic time problem --- the standard algorithm for it is cubic time and the conventional wisdom is that this algorithm cannot be...
Model Checking Electronic Commerce Protocols (Extended Abstract) (1996)
Nevin Heintze, J. D. Tygar, Jeannette Wing, H. C. Wong
) Nevin Heintze J. D. Tygar Jeannette Wing H. C. Wong Bell Laboratories Carnegie Mellon Univ. Carnegie Mellon Univ. Carnegie Mellon Univ. Murray Hill, NJ 07974 Pittsburgh, PA 15213 Pittsburgh, PA...
Control-flow analysis and type systems (1995)
Abstract. We establish a series of equivalences between type systems and control-flow analyses. Specifically, we take four type systems from the literature (involving simple types, subtypes and...
Control-flow analysis and type systems (1995)
We establish a series of equivalences between type systems and control-flow analyses. Specifically, we take four type systems from the literature (involving simple types, subtypes and recursion) and...
A Generic Algorithm for CLP Analysis (1995)
Nevin Heintze School, Nevin Heintze, Joxan Jaffar
Logic program analyzers typically employ abstract interpretation and consist of two main components: an abstract domain and a generic iterative fixed-point computation or "engine". In...
Control-Flow Analysis and Type Systems (1995)
We establish a series of equivalences between type systems and control-flow analyses. Specifically, we take four type systems from the literature (involving simple types, subtypes and recursion) and...
ML partial evaluation using set-based analysis (1994)
Karoline Malmkjær, Nevin Heintze, Olivier Danvy
8313, issued by ESD/AVS under Contract No. F19628-91-C-0168. It was also partially sponsored
ML partial evaluation using set-based analysis (1994)
Karoline Malmkjaer, Nevin Heintze, Olivier Danvy
We describe the design and implementation of an off-line partial evaluator for Standard ML programs. Our partial evaluator consists of two phases: analysis and specialization. Analysis: Set-based...
Set Constraints and Set-Based Analysis (1994)
This paper contains two main parts. The first examines the set constraint calculus, discusses its history, and overviews the current state of known algorithms and related issues. Here we will also...
Meta-Programming in CLP(R) (1994)
Nevin Heintze, Spiro Michaylov, Peter J. Stuckey
A widely used property of Prolog is that it is possible to write Prolog programs to construct and manipulate other Prolog programs in a very general manner. Unfortunately, this property is not...
ML Partial Evaluation using Set-Based Analysis (1994)
Karoline Malmkjær, Nevin Heintze, Olivier Danvy
We describe the design and implementation of an off-line partial evaluator for Standard ML programs. Our partial evaluator consists of two phases: analysis and specialization. Analysis: Set-based...
ML Partial Evaluation using Set-Based Analysis (1994)
Karoline Malmkj Nevin, Nevin Heintze, Olivier Danvy
We describe the design and implementation of an off-line partial evaluator for Standard ML programs. Our partial evaluator consists of two phases: analysis and specialization. Analysis: Set-based...
ML Partial Evaluation using Set-Based Analysis (1994)
Karoline Malmkjaer, Nevin Heintze, Olivier Danvy
We describe the design and implementation of an off-line partial evaluator for Standard ML programs. Our partial evaluator consists of two phases: analysis and specialization. Analysis: Set-based...
Set based analysis of arithmetic (1993)
The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the U.S. Government.
Set Based Analysis of ML Programs (1993)
Exte Nd Ed, Nevin Heintze, Um Cmu-cs-fox
) NEVIN HEINTZE July 1993 CMU-CS-93-193 (Also appears as Fox Memorandum CMU-CS-FOX-93-03.) School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213 Abstract Reasoning about a...
Set based analysis of ML programs (extended abstract (1993)
Reasoning about a program by treating program variables as sets of "values " leads to a simple, accurate and intuitively appealing notion of program approximation. This paper...
Set Constraints in Program Analysis (1993)
domains employed in abstract interpretation are typically required to satisfy the finite ascending chains condition (or some analogous condition) and this represents a fundamental restriction on the...
Set Based Analysis and Arithmetic (Extended Abstract) (1993)
) NEVIN HEINTZE School of Computer Science Carnegie Mellon University December 1993 Set based analysis is an approach to compile-time program analysis that is based on a simple approximation: all...
Set Based Analysis of Arithmetic (1993)
Nevin Heintze December, Nevin Heintze
Set based analysis is an approach to compile-time program analysis that is based on a simple approximation: all dependencies between variables are ignored. In effect, program variables are treated as...
Set based analysis of ML programs (extended abstract (1993)
O(n3) algorithm for computing the set based approximation of a program. Wethen show how the analysis can be extended in a natural way to deal with arrays, arithmetic, exceptions and continuations. We...
Timed Models for Protocol Security (1992)
The notion of time is prerequisite for describing and verifying the security properties of key management protocols. Without it, properties relating to the expiration of keys and the freshness of...
An Engine for Logic Program Analysis (1992)
Most logic program analyzers employ a standard approach based on abstract interpretation. At the core of these is a generic algorithm or "engine" which is parameterized by an abstract...
Semantic Types for Logic Programs (1992)
Interpretation: Towards the Global Optimisation of PROLOG Programs", Proceedings 4 th IEEE Symposium on Logic Programming, pp 192 - 204, September 1987. [2] F. G`ecseg and M. Steinby, "Tree...
Practical Aspects of Set Based Analysis (1992)
This paper demonstrates that very substantial progress can be made towards a practical system by redesigning the algorithms according to implementation criteria, designing appropriate representations...
Timed Models for Protocol Security (1992)
Nevin Heintze And, Nevin Heintze, J. D. Tygar
The notion of time is prerequisite for describing and verifying the security properties of key management protocols. Without it, properties relating to the expiration of keys and the freshness of...
Semantic Types for Logic Programs (1992)
By Nevin Heintze, Nevin Heintze, Joxan Jaffar
Interpretation: Towards the Global Optimisation of PROLOG Programs", Proceedings 4 th IEEE Symposium on Logic Programming, pp 192 - 204, September 1987. [2] F. G`ecseg and M. Steinby, "Tree...
Timed Models for Protocol Security (1992)
Nevin Heintze And, Nevin Heintze, J. D. Tygar
The notion of time is prerequisite for describing and verifying the security properties of key management protocols. Without it, properties relating to the expiration of keys and the freshness of...
Timed Models for Protocol Security (1992)
The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the o cial policies, either expressed or implied, of the U.S. Government.
CLP(R) and Some Electrical Engineering Problems (1991)
Nevin Heintze, Spiro Michaylov, Peter Stuckey
The Constraint Logic Programming Scheme defines a class of languages designed for programming with constraints using a logic programming approach. These languages are soundly based on a unified...
A Decision Procedure for a Class of Set Constraints (1991)
A set constraint is of the form exp 1 ' exp 2 where exp 1 and exp 2 are set expressions constructed using variables, function symbols, projection symbols, and the set union, intersection and...
Set-Based Program Analysis (Extended Abstract) (1991)
) Nevin Heintze and Joxan Jaffar y 1 January 1991 Summary Program analysis involves approximating the semantics of programs. One important kind of approximation, that of ignoring intervariable...
A Finite Presentation Theorem for Approximating Logic Programs (1990)
In program analysis, a key notion used to approximate the meaning of a program is that of ignoring inter-variable dependencies. We formalize this notion in logic programming in order to define an...
A Decision Procedure for a Class of Set Constraints (1990)
Nevin Heintze And, Nevin Heintze, Joxan Jaffar
A set constraint is of the form exp 1 ' exp 2 where exp 1 and exp 2 are set expressions constructed using variables, function symbols, projection symbols, and the set union, intersection and...
A Finite Presentation Theorem for Approximating Logic Programs (Extended Abstract) (1990)
) Nevin Heintze Joxan Jaffar School of Computer Science IBM T.J. Watson Research Center Carnegie Mellon University PO Box 218 Pittsburgh, PA 15213 Yorktown Heights, NY 10598 Summary The notion of...
Control-safe logic programming (1989)
Submitted for the degree of Master of Science, Dept. of Computer Science. Summary: leaves ii-iv. Typescript. Bibliography: leaves 80-85.
Control-safe logic programming (1989)
Submitted for the degree of Master of Science, Dept. of Computer Science. Summary: leaves ii-iv. Typescript. Bibliography: leaves 80-85.
On Meta-Programming in CLP(R) (1989)
Nevin Heintze, Spiro Michaylov, Peter Stuckey, Roland Yap
The manipulation of CLP(!) programs in CLP(!) is severely limited, since equality for this language is not based on the syntactic structure of terms. We propose an extended language, CLP(!+M), which...