news articles our work projects publications software directions

SRC Research Reports


Here is a list of all SRC Research Reports, with links to the abstracts. When PostScript or PDF files are available, there are links from the abstract to those files. If you are using Netscape, you can save those files on your local disk by right clicking on the appropriate link and choosing "Save Link As". Alternatively, here are instructions for using FTP to retrieve SRC reports.

You can also use this form to order hardcopy reports and videotapes from us. Select the reports of interest, and then click this button: , which will open another form asking for your name and address.

The online version of each report marked with [scanned] was recreated by scanning a paper version to produce images rather than text. The resultant files are relatively large and cannot be searched, but may be read online or printed.


166. Efficient and flexible value sampling.
Michael Burrows, Ulfar Erlingson, Shun-Tak A. Leung, Mark Vandevoorde, Carl Waldspurger, Kevin Walker, and Bill Weihl. (October, 2000).
Include this report in my order

165. A practical, robust method for generating variable range tables.
Caroline Tice and Susan L. Graham. (September, 2000).
Include this report in my order

164. Key instructions: Solving the code location problem for optimized code.
Caroline Tice and Susan L. Graham. (August, 2000).
Include this report in my order

163. Disk paxos.
Eli Gafni and Leslie Lamport. (June, 2000).
Include this report in my order

162. An efficient matching algorithm for a high-throughput, low-latency data switch.
Thomas Rodeheffer and James B. Saxe. (November, 1998).
Include this report in my order

161. A logic of object-oriented programs.
Martin Abadi and K. Rustan M. Leino. (September, 1998).
Include this report in my order

159. Extended static checking.
David Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. (December, 1998).
Include this report in my order

158. A type system for Java bytecode subroutines.
Raymie Stata and Martin Abadi. (June, 1998).
Include this report in my order

157. The Virtual Book.
David Chaiken, Mark Hayter, Jay Kistler, and David Redell. (November, 1998).
Include this report in my order

156. Wrestling with rep exposure.
David Detlefs, K. Rustan M. Leino, and Greg Nelson. (July, 1998).
Include this report in my order

155. A comparison of two distributed disk systems.
Edward K. Lee, Chandramohan Thekkath, Chris Whitaker, and Jim Hogg. (April, 1998).
Include this report in my order

154. Protection in programming-language translations.
Martin Abadi. (April, 1998).
Include this report in my order

153. Continuous monitoring and performance specification.
Sharon Perl, Bill Weihl, and Brian Noble. (June, 1998).
Include this report in my order

152. Fairness and hyperfairness.
Leslie Lamport. (March, 1998).
Include this report in my order

151. Reports 100-150: The abstracts.
Compiled by James Mason. (March, 1998).
Include this report in my order

150. Smooth scheduling in a cell-based switching network.
Thomas Rodeheffer and James B. Saxe. (February, 1998).
Include this report in my order

149. A calculus for cryptographic protocols: The spi calculus.
Martin Abadi and Andrew D. Gordon. (January, 1998).
Include this report in my order

148. Service combinators for Web computing.
Luca Cardelli and Rowan Davies. (June, 1997).
Include this report in my order

147. Should your specification language be typed?.
Leslie Lamport and Lawrence C. Paulson. (May, 1997).
Include this report in my order

146. Studies of Windows NT Performance using Dynamic Execution Traces.
Sharon Perl and Richard L. Sites. (April, 1997).
Include this report in my order

145. Modularity in the presence of subclassing.
Raymie Stata. (April, 1997).
Include this report in my order

144. Program fragments, linking, and modularization.
Luca Cardelli. (February, 1997).
Include this report in my order

143. To provide or to bound: Sampling in fully dynamic graph algorithms.
Monika Henzinger and Mikkel Thorup. (October, 1996).
Include this report in my order

142. Collaborative active textbooks: A web-based algorithm animation system for an electronic classroom.
Marc Brown and Marc A. Najork. (September, 1996).
Include this report in my order

141a. Distributed active objects.
Marc Brown and Marc A. Najork. (May, 1996).
Has associated video, also available for order.
Include this report in my order
Include video in my order: NTSC PAL SECAM

140. Zippers: A focus+context display of web pages.
Marc Brown and Bill Weihl. (May, 1996).
Include this report in my order

139a. Webcard: Integrated and uniform access to mail, news, and the web.
Marc Brown. (July, 1996).
Has associated video, also available for order.
Include this report in my order
Include video in my order: NTSC PAL SECAM

138. Migratory applications.
Luca Cardelli and Krishna Bharat. (February, 1996).
Include this report in my order

137. Proving possibility properties.
Leslie Lamport. (July, 1995).
Include this report in my order

136. A functional specification of the Alpha AXP shared memory model.
Manfred Broy. (April, 1995).
Include this report in my order

135a. Deckscape: An experimental Web browser.
Marc Brown and Robert A. Shillner. (March, 1995).
Has associated video, also available for order.
Include this report in my order
Include video in my order: NTSC PAL SECAM

134a. From quadrangular sets to the budget matroids.
Lyle Ramshaw and James B. Saxe. (May, 1995).
Has associated video, also available for order.
Include this report in my order
Include video in my order: NTSC PAL SECAM

133a. The third annual video review of computational geometry.
Marc Brown and John Hershberger, editors. (December, 1994).
Has associated video, also available for order.
Include this report in my order
Include video in my order: NTSC PAL SECAM

132. Processes are in the Eye of the Beholder.
Leslie Lamport. (December, 1994).
Include this report in my order

131a. The Juno-2 constraint-based drawing editor.
Allan Heydon and Greg Nelson. (December, 1994).
Has associated video, also available for order.
Include this report in my order
Include video in my order: NTSC PAL SECAM

130a. Visual obliq: A system for building distributed, multi-user applications by direct manipulation.
Krishna Bharat and Marc Brown. (October, 1995).
Has associated video, also available for order.
Include this report in my order
Include video in my order: NTSC PAL SECAM

129. Obliq-3D tutorial and reference manual.
Marc A. Najork. (December, 1994).
Include this report in my order

128a. A library for visualizing combinatorial structures.
Marc A. Najork and Marc Brown. (September, 1994).
Has associated video, also available for order.
Include this report in my order
Include video in my order: NTSC PAL SECAM

127. TLA in pictures.
Leslie Lamport. (September, 1995).
Include this report in my order

126. The 1993 SRC Algorithm Animation Festival.
Marc Brown. (August, 1994).
Include this report in my order

125. Prudent engineering practice for cryptographic protocols.
Martin Abadi and Roger M. Needham. (June, 1994).
Include this report in my order

124. A block-sorting lossless data compression algorithm.
Michael Burrows and D. J. Wheeler. (May, 1994).
Include this report in my order

123. Inside Hector: The systems view.
Loretta Guarino Reid and Jim Meehan. (April, 1994).
Include this report in my order

122. Obliq: A language with distributed scope.
Luca Cardelli. (June, 1994).
Include this report in my order

121. Extensible syntax with lexical scoping.
Luca Cardelli, Florian Matthes, and Martin Abadi. (February, 1994).
Include this report in my order

120. Dynamic typing in polymorphic languages.
Martin Abadi, Luca Cardelli, Benjamin C. Pierce, and Didier Rémy. (January, 1994).
Include this report in my order

119. How to write a long formula.
Leslie Lamport. (December, 1993).
Include this report in my order

118. Conjoining specifications.
Martin Abadi and Leslie Lamport. (December, 1993).
Include this report in my order

117. Authentication in the Taos Operating System.
Edward P. Wobber, Martin Abadi, Michael Burrows, and Butler Lampson. (December, 1993).
Include this report in my order

116. Distributed garbage collection for Network Objects.
Andrew D. Birrell, David Evers, Greg Nelson, Sue Owicki, and Edward P. Wobber. (December, 1993).
Include this report in my order

115. Network objects.
Andrew D. Birrell, Greg Nelson, Susan Owicki, and Edward P. Wobber. (December, 1995).
Include this report in my order

114. Automated proofs of object code for a widely used microprocessor.
Yuan Yu. (October, 1993).
Include this report in my order

113. Some useful Modula-3 interfaces.
Jim Horning, Bill Kalsow, Paul McJones, and Greg Nelson. (December, 1993).
Include this report in my order

112. Availability in the Echo file system.
Garret Swart, Andrew D. Birrell, Andy Hisgen, and Timothy Mann. (September, 1993).
Include this report in my order

111. The Echo distributed file system.
Andrew D. Birrell, Andy Hisgen, Chuck Jerian, Timothy Mann, and Garret Swart. (September, 1993).
Include this report in my order

110a. Algorithm animation using 3D interactive graphics.
Marc Brown and Marc A. Najork. (November, 1993).
Has associated video, also available for order.
Include this report in my order
Include video in my order: NTSC PAL SECAM

109. Formal parametric polymorphism.
Martin Abadi, Luca Cardelli, and Pierre-Louis Curien. (July, 1993).
Include this report in my order

108. Bridges: Tools to extend the Vesta configuration management system.
Mark Brown and John Ellis. (June, 1993).
Include this report in my order

107. The Vesta language for configuration management.
Chris Hanna and Roy Levin. (June, 1993).
Include this report in my order

106. The Vesta repository: A file system extension for software development.
Sheng-Yang Chiu and Roy Levin. (June, 1993).
Include this report in my order

105. The Vesta approach to precise configuration of large software systems.
Roy Levin and Paul McJones. (June, 1993).
Include this report in my order

104. New-value logging in the Echo replicated file system.
Andy Hisgen, Andrew D. Birrell, Chuck Jerian, Timothy Mann, and Garret Swart. (June, 1993).
Include this report in my order

103. A coherent distributed file cache with directory write-behind.
Timothy Mann, Andrew D. Birrell, Andy Hisgen, Chuck Jerian, and Garret Swart. (June, 1993).
Include this report in my order

102. Safe, efficient garbage collection for C++.
John Ellis and David Detlefs. (June, 1993).
Include this report in my order

101a. The second annual video review of computational geometry.
Marc Brown and John Hershberger, editors. (May, 1993).
Has associated video, also available for order.
Include this report in my order
Include video in my order: NTSC PAL SECAM

100. The first 99 reports.
Compiled by James Mason. (June, 1993).
Include this report in my order

099. High speed switch scheduling for local area networks.
Thomas Anderson, Sue Owicki, James B. Saxe, and Chuck Thacker. (April, 1993).
Include this report in my order

098. The 1992 SRC algorithm animation festival.
Marc Brown. (March, 1993).
Include this report in my order

097. An implementation of F<:.
Luca Cardelli. (February, 1993).
Include this report in my order

096. How to make a correct multiprocess program execute correctly on a multiprocessor.
Leslie Lamport. (February, 1993).
Include this report in my order

095. Baby Modula-3 and a theory of objects.
Martin Abadi. (February, 1993).
Include this report in my order

094. How to write a proof.
Leslie Lamport. (February, 1993).
Include this report in my order

093. Experiences with software specification and verification using LP, the Larch Proof Assistant.
Manfred Broy. (October, 1992).
Include this report in my order

092a. Hector: Connecting words with definitions.
Lucille Glassman, Dennis Grinberg, Cynthia Hibbard, Jim Meehan, Loretta Guarino Reid, and Mary-Claire van Leunen. (October, 1992).
Has associated video, also available for order.
Include this report in my order
Include video in my order: NTSC PAL SECAM

091. An old-fashioned recipe for real-time.
Martin Abadi and Leslie Lamport. (October, 1992).
Include this report in my order

090. A high-speed DES implementation for network applications.
Hans Eberle. (September, 1992).
Include this report in my order

089. Compositional refinement of interactive systems.
Manfred Broy. (July, 1992).
Include this report in my order

088. Factors in the performance of the AN1 computer network.
Sue Owicki and Anna Karlin. (June, 1992).
Include this report in my order

087a. Animation of geometric algorithms: A video review.
Marc Brown and John Hershberger, editors. (June, 1992).
Has associated video, also available for order.
Include this report in my order
Include video in my order: NTSC PAL SECAM

086. A logical view of composition.
Martin Abadi and Gordon D. Plotkin. (May, 1992).
Include this report in my order

085. On-line data compression in a log-structured file system.
Michael Burrows, Chuck Jerian, Butler Lampson, and Timothy Mann. (April, 1992).
Include this report in my order

084a. Graphical fisheye views.
Manojit Sarkar and Marc Brown. (December, 1994).
Has associated video, also available for order.
Include this report in my order
Include video in my order: NTSC PAL SECAM

083. Authentication in distributed systems: Theory and Practice.
Butler Lampson, Martin Abadi, Michael Burrows, and Edward P. Wobber. (February, 1992).
Include this report in my order

082. A guide to LP, the Larch Prover.
Stephen J. Garland and John V. Guttag. (December, 1991).
Include this report in my order

081. Extensible records in a pure calculus of subtyping.
Luca Cardelli. (January, 1992).
Include this report in my order

080. An extension of system F with subtyping.
Luca Cardelli, John C. Mitchell, Simone Martini, and Andre Scedrov. (December, 1991).
Include this report in my order

079. The temporal logic of actions.
Leslie Lamport. (January, 1991).
Include this report in my order

078. Using transformations and verification in circuit design.
James B. Saxe, Stephen J. Garland, John V. Guttag, and Jim Horning. (September, 1991).
Include this report in my order

077. Automatic reconfiguration in Autonet.
Thomas Rodeheffer and Michael D. Schroeder. (September, 1991).
Include this report in my order

076a. Color and sound in algorithm animation.
Marc Brown and John Hershberger. (August, 1991).
Has associated video, also available for order.
Include this report in my order
Include video in my order: NTSC PAL SECAM

075. Zeus: A system for algorithm animation and multi-view editing.
Marc Brown. (February, 1992).
Include this report in my order

074. Introduction to LCL: A Larch/C interface language.
John V. Guttag and Jim Horning. (July, 1991).
Include this report in my order

073. Decidability and expressiveness for first-order logics of probability.
Martin Abadi and Joseph Y. Halpern. (June, 1991).
Include this report in my order

072. LM3: A Larch interface language for Modula-3: Version 1.0.
Kevin Jones. (June, 1991).
Include this report in my order

071. Trading space for time in undirected s-t connectivity.
Andrei Broder, Anna Karlin, Prabhakar Raghavan, and Eli Upfal. (May, 1991).
Include this report in my order

070. A calculus for access control in distributed systems.
Martin Abadi, Michael Burrows, Butler Lampson, and Gordon D. Plotkin. (March, 1991).
Include this report in my order

069. Trestle tutorial.
Mark Manasse and Greg Nelson. (May, 1992).
Include this report in my order

068. Trestle reference manual.
Mark Manasse and Greg Nelson. (December, 1991).
Include this report in my order

067. Authentication and delegation with smart-cards.
Martin Abadi, Michael Burrows, Charles Kaufman, and Butler Lampson. (October, 1990).
Include this report in my order

066. Composing specifications.
Martin Abadi and Leslie Lamport. (October, 1990).
Include this report in my order

065. An axiomatization of Lamport's Temporal Logic of Actions.
Martin Abadi. (October, 1990).
Include this report in my order

064. Experience with concurrent garbage collectors for Modula-2+.
John DeTreville. (November, 1990).
Include this report in my order

063. Heap usage in the Topaz environment.
John DeTreville. (August, 1990).
Include this report in my order

062. Subtyping recursive types.
Roberto M. Amadio and Luca Cardelli. (August, 1990).
Include this report in my order

061. In Memoriam: J.C.R. Licklider 1915-1990.
J.C.R. Licklider and Bob Taylor. (August, 1990).
Include this report in my order

060. Debugging Larch Shared Language specifications.
Stephen J. Garland, John V. Guttag, and Jim Horning. (July, 1990).
Include this report in my order

059. Autonet: a high-speed, self-configuring local area network using point-to-point links.
Michael D. Schroeder, Andrew D. Birrell, Michael Burrows, Hal Murray, Roger M. Needham, Thomas Rodeheffer, Ed Satterthwaite, and Chuck Thacker. (April, 1990).
Include this report in my order

058. Report on the Larch Shared Language: Version 2.3.
John V. Guttag, Jim Horning, and Andrés Modet. (April, 1990).
Include this report in my order

057. A temporal logic of actions.
Leslie Lamport. (April, 1990). (This report has been superseded by [079].).
Include this report in my order

056. Abstract types and the dot notation.
Luca Cardelli and Xavier Leroy. (March, 1990).
Include this report in my order

055. A semantic basis for Quest.
Luca Cardelli and Giuseppe Longo. (February, 1990).
Include this report in my order

054. Explicit substitutions.
Martin Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. (February, 1990).
Include this report in my order

053. IO streams: Abstract types, real programs.
Mark Brown and Greg Nelson. (November, 1989).
Include this report in my order

052. Modula-3 report (revised).
Luca Cardelli, James Donahue, Lucille Glassman, Mick Jordan, Bill Kalsow, and Greg Nelson. (September, 1989).
Include this report in my order

051. Experience with the Firefly multiprocessor workstation.
Sue Owicki. (September, 1989).
Include this report in my order

050a. An efficient algorithm for finding the CSG representation of a simple polygon.
David Dobkin, Leonidas J. Guibas, John Hershberger, and Jack Snoeyink. (September, 1989).
Has associated video, also available for order.
Include this report in my order
Include video in my order: NTSC PAL SECAM

049. The part-time parliament.
Leslie Lamport. (September, 1989).
Include this report in my order

048. Operations on records.
Luca Cardelli and John C. Mitchell. (August, 1989).
Include this report in my order

047. Dynamic typing in a statically-typed language.
Martin Abadi, Luca Cardelli, Benjamin C. Pierce, and Gordon D. Plotkin. (June, 1989).
Include this report in my order

046. An algorithm for data replication.
Timothy Mann, Andy Hisgen, and Garret Swart. (June, 1989).
Include this report in my order

045. Typeful programming.
Luca Cardelli. (May, 1989).
Include this report in my order

044. Pretending atomicity.
Leslie Lamport and Fred B. Schneider. (May, 1989).
Include this report in my order

043. Performance of Firefly RPC.
Michael D. Schroeder and Michael Burrows. (April, 1989).
Include this report in my order

042. WorkCrews: An abstraction for controlling parallelism.
Mark Vandevoorde and Eric Roberts. (February, 1988).
Include this report in my order

041. Evaluating the performance of software cache coherence.
Sue Owicki and Anant Agarwal. (March, 1989).
Include this report in my order

040. Implementing exceptions in C.
Eric S. Roberts. (May, 1989).
Include this report in my order

039. A logic of authentication.
Michael Burrows, Martin Abadi, and Roger M. Needham. (February, 1989).
Include this report in my order

038. Can fair choice be added to Dijkstra's calculus?.
Manfred Broy and Greg Nelson. (February, 1989).
Include this report in my order

037. Ruler, compass and computer: The design and analysis of geometric algorithms.
Leonidas J. Guibas and Jorge Stolfi. (February, 1989).
Include this report in my order

036. Primitives for computational geometry.
Jorge Stolfi. (January, 1989).
Include this report in my order

035. An introduction to programming with threads.
Andrew D. Birrell. (January, 1989).
Include this report in my order

034. Blossoms are polar forms.
Lyle Ramshaw. (January, 1989).
Include this report in my order

033. A two-view document editor with user-definable document structure.
Kenneth Brooks. (November, 1988).
Include this report in my order

032. Bounds on the cover time.
Andrei Broder and Anna Karlin. (October, 1988).
Include this report in my order

031. Modula-3 report.
Luca Cardelli, James Donahue, Lucille Glassman, Mick Jordan, Bill Kalsow, and Greg Nelson. (August, 1988). (This report has been superseded by [052].).
Include this report in my order

030. The power of temporal proofs.
Martin Abadi. (August, 1988).
Include this report in my order

029. The existence of refinement mappings.
Martin Abadi and Leslie Lamport. (August, 1988).
Include this report in my order

028. A theorem on atomicity in distributed algorithms.
Leslie Lamport. (May, 1988).
Include this report in my order

027. Concurrent reading and writing of clocks.
Leslie Lamport. (April, 1988).
Include this report in my order

026. Parallel compilation on a tightly-coupled multiprocessor.
Mark Vandevoorde. (March, 1988).
Include this report in my order

025. Real-time concurrent collection on stock multiprocessors.
John Ellis and Kai Li. (February, 1988).
Include this report in my order

024. A simple and efficient implementation for small databases.
Andrew D. Birrell, Michael B. Jones, and Edward P. Wobber. (January, 1988).
Include this report in my order

023. Firefly: A multiprocessor workstation.
Chuck Thacker, Lawrence C. Stewart, and Ed Satterthwaite. (December, 1987).
Include this report in my order

022. Building user interfaces by direct manipulation.
Luca Cardelli. (May, 1989).
Include this report in my order

021. Evolving the unix system interface to support multithreaded programs.
Paul McJones and Garret Swart. (September, 1987).
Include this report in my order

020. Synchronization primitives for a multiprocessor: A formal specification.
Andrew D. Birrell, John V. Guttag, Jim Horning, and Roy Levin. (August, 1987).
Include this report in my order

019. Blossoming: A connect-the-dots approach to splines.
Lyle Ramshaw. (June, 1987).
Include this report in my order

018. Synchronizing time services.
Leslie Lamport. (June, 1987).
Include this report in my order

017. win and sin: Predicate transformers for concurrency.
Leslie Lamport. (May, 1987).
Include this report in my order

016. A generalization of Dijkstra's calculus.
Greg Nelson. (April, 1987).
Include this report in my order

015. A simple approach to specifying concurrent systems.
Leslie Lamport. (December, 1986).
Include this report in my order

014. An $O(n^2)$ shortest path algorithm for a non-rotating convex body.
Leonidas J. Guibas and John Hershberger. (November, 1986).
Include this report in my order

013. Retiming synchronous circuitry.
Charles E. Leiserson and James B. Saxe. (August, 1986).
Include this report in my order

012. Fractional cascading: a data structuring technique with geometric applications.
Bernard Chazelle and Leonidas J. Guibas. (June, 1986).
Include this report in my order

011. Control predicates are better than dummy variables.
Leslie Lamport. (May, 1986).
Include this report in my order

010. A polymorphic lambda-calculus with Type:Type.
Luca Cardelli. (May, 1986).
Include this report in my order

009. Topologically sweeping an arrangement.
Herbert Edelsbrunner and Leonidas J. Guibas. (April, 1986).
Include this report in my order

008. On interprocess communication.
Leslie Lamport. (December, 1985).
Include this report in my order

007. A fast mutual exclusion algorithm.
Leslie Lamport. (November, 1985).
Include this report in my order

006. A caching file system for a programmer's workstation.
David K. Gifford, Roger M. Needham, and Michael D. Schroeder. (October, 1985).
Include this report in my order

005. Larch in five easy pieces.
John V. Guttag, Jim Horning, and Jeannette M. Wing. (July, 1985).
Include this report in my order

004. Eliminating go to's while preserving program structure.
Lyle Ramshaw. (July, 1985).
Include this report in my order

003. On extending Modula-2 for building large, integrated systems.
Paul Rovner, Roy Levin, and John Wick. (January, 1985).
Include this report in my order

002. Optimal point location in a monotone subdivision.
Herbert Edelsbrunner, Leonidas J. Guibas, and Jorge Stolfi. (October, 1984).
Include this report in my order

001. A kernel language for modules and abstract data types.
Rod Burstall and Butler Lampson. (September, 1984).
Include this report in my order


Compaq Systems Research Center
130 Lytton Avenue, Palo Alto, CA 94301
Tel: (650) 853-2100 Fax: (650) 853-2104
Legal notice
Send comments to the owner of this page.
Last modified: Sunday, 05-Nov-00 17:33:32 PST