Article

Enforcing high-level protocols in low-level software

Authors:

Robert DeLine,

Manuel FähndrichAuthors Info & Claims

PLDI '01: Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation

Pages 59 - 69

https://doi.org/10.1145/378795.378811

Published: 01 May 2001 Publication History

Get Access

References

[1]

T. Ball and S. Rajamani. Automatically validating temporal safety properties of software. In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2001.]]

Google Scholar

[2]

E. Barendsen and J. Smetsers. Conventional and uniqueness typing in graph rewrite systems. In 13th Conference on Foundations of Software Technology and Theoretical Computer Science, LNCS 761, pages 41-51, Dec. 1993.]]

Digital Library

Google Scholar

[3]

K. Crary, D. Walker, and G. Morrisett. Typed memory management in a calculus of capabilities. In POPL'99 {13}.]]

Digital Library

Google Scholar

[4]

D. L. Detlefs, K. R. M. Leino, and G. Nelson. Wrestling with rep exposure. Technical Report 156, Compaq SRC, jul 1998.]]

Google Scholar

[5]

D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In Symposium on Operating Systems Design and Implementation (OSDI 2000), Oct. 2000.]]

Digital Library

Google Scholar

[6]

C. Flanagan and S. N. Freund. Type-based race detection for java. In Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2000.]]

Digital Library

Google Scholar

[7]

J. S. Foster, M. F~hndrich, and A. Aiken. A theory of type qualifiers. In Proceedings of the 1999 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 192-203, May 1999.]]

Digital Library

Google Scholar

[8]

D. Gay and A. Aiken. Memory management with explicit regions. In Proceedings of the 1998 ACM SIGPLAN Conference on Programming Language Design and Implementation, number 33:5 in SIGPLAN notices, pages 313-323, June 1998.]]

Digital Library

Google Scholar

[9]

M. P. Jones. A theory of qualified types. Science of Computer Programming, 22(3):231-256, June 1994. Selected papers of the Fourth European Symposium on Programming (Rennes, 1992).]]

Digital Library

Google Scholar

[10]

M. P. Jones. Simplifying and improving qualified types. In Proceedings of the 1995 Conference on Functional Programming Languages and Computer Architecture, pages 160-169, June 1995.]]

Digital Library

Google Scholar

[11]

B. W. Kernighan and D. M. Ritchie. The C Programming Language. Prentice Hall, 2nd edition, 1988.]]

Digital Library

Google Scholar

[12]

K. R. M. Leino and G. Nelson. An extended static checker for Modula-3. In K. Koskimies, editor, Compiler Construction (CC'98), pages 302-305, Lisbon, 1998. Springer LNCS 1383.]]

Digital Library

Google Scholar

[13]

Conference Record of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, Jan. 1999.]]

Google Scholar

[14]

M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In POPL'99 {13}, pages 105-118.]]

Digital Library

Google Scholar

[15]

F. Smith, D. Walker, and G. Morrisett. Alias types. In Proceedings of the 2000 European Symposium on Programming, Mar. 2000.]]

Digital Library

Google Scholar

[16]

R. E. Strom and D. M. Yellin. Extending typestate checking using conditional liveness analysis. IEEE Transactions on Software Engineering, 19(5):478-485, May 1993.]]

Digital Library

Google Scholar

[17]

R. E. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. tose, SE-12(1):157-171, Jan. 1986.]]

Digital Library

Google Scholar

[18]

M. Tofte and J.-P. Talpin. Implementation of the typed call-by-value calculus using a stack of regions. In Conference Record of the 21st Annual ACM SSymposium on Principles of Programming Languages, pages 188-201, Jan. 1994.]]

Digital Library

Google Scholar

[19]

D. Walker, K. Crary, and G. Morrisett. Typed memory management in a calculus of capabilities. Transactions on Programming Languages and Systems, 2001.]]

Digital Library

Google Scholar

[20]

D. Walker and G. Morrisett. Alias types for recursive data structures. In Proceedings of the 4th Workshop on Types in Compilation, Sept. 2000.]]

Digital Library

Google Scholar

Cited By

View all

Silva TBispo JCarvalho TShrivastava ASui Y(2024)Foundations for a Rust-Like Borrow Checker for CProceedings of the 25th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems10.1145/3652032.3657579(155-165)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3652032.3657579
Cheng XRen JSui Y(2024)Fast Graph Simplification for Path-Sensitive Typestate Analysis through Tempo-Spatial Multi-Point SlicingProceedings of the ACM on Software Engineering10.1145/36437491:FSE(494-516)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3643749
Roth OGil Y(2023)Fluent APIs in Functional LanguagesProceedings of the ACM on Programming Languages10.1145/35860577:OOPSLA1(876-901)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586057
Show More Cited By

Index Terms

Recommendations

High-Level Test Synthesis: A Survey from Synthesis Process Flow Perspective

High-level test synthesis is a special class of high-level synthesis having testability as one of the important components. This article presents a detailed survey on recent developments in high-level test synthesis from a synthesis process flow ...
Layout-driven RTL binding techniques for high-level synthesis
ISSS '96: Proceedings of the 9th international symposium on System synthesis

The importance of effective and efficient accounting of layout effects is well-established in high-level synthesis (HLS), since it allows more realistic exploration of the design space and the generation of solutions with predictable metrics. This ...
High-Level Synthesis: Past, Present, and Future

Editor's note:This article presents the history and evolution of HLS from research to industry adoption. The authors offer insights on why earlier attempts to gain industry adoption were not successful, why current HLS tools are finally seeing adoption, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

PLDI '01: Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation

June 2001

331 pages

ISBN:1581134142

DOI:10.1145/378795

Chairmen:
Michael Burke
IBM T.J. Watson Research Center
,
Mary Lou Soffa
Univ. of Pittsburgh

ACM SIGPLAN Notices Volume 36, Issue 5
May 2001
330 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/381694
Editors:
Cindy Norris,
James B. Bergin
Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 May 2001

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

PLDI01

Sponsor:

SIGPLAN

PLDI01: ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation

Utah, Snowbird, USA

Acceptance Rates

PLDI '01 Paper Acceptance Rate 30 of 144 submissions, 21%;

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

413
Total Citations
View Citations
1,139
Total Downloads

Downloads (Last 12 months)38
Downloads (Last 6 weeks)3

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Silva TBispo JCarvalho TShrivastava ASui Y(2024)Foundations for a Rust-Like Borrow Checker for CProceedings of the 25th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems10.1145/3652032.3657579(155-165)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3652032.3657579
Cheng XRen JSui Y(2024)Fast Graph Simplification for Path-Sensitive Typestate Analysis through Tempo-Spatial Multi-Point SlicingProceedings of the ACM on Software Engineering10.1145/36437491:FSE(494-516)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3643749
Roth OGil Y(2023)Fluent APIs in Functional LanguagesProceedings of the ACM on Programming Languages10.1145/35860577:OOPSLA1(876-901)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586057
Gonnord LHenrio LMorel LRadanne G(2023)A Survey on Parallelism and DeterminismACM Computing Surveys10.1145/356452955:10(1-28)Online publication date: 2-Feb-2023
https://dl.acm.org/doi/10.1145/3564529
Godoy JGaleotti JGarbervetsky DUchitel SSyriani ESahraoui H(2022)Predicate abstractions for smart contract validationProceedings of the 25th International Conference on Model Driven Engineering Languages and Systems10.1145/3550355.3552462(289-299)Online publication date: 23-Oct-2022
https://dl.acm.org/doi/10.1145/3550355.3552462
Spiwack AKiss CBernardy JWu NEisenberg R(2022)Linearly qualified types: generic inference for capabilities and uniquenessProceedings of the ACM on Programming Languages10.1145/35476266:ICFP(137-164)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547626
Halpin H(2022)The Knowledge Trust: A Proposal for a Blockchain Consortium for Digital ArchivesLinking Theory and Practice of Digital Libraries10.1007/978-3-031-16802-4_35(372-378)Online publication date: 20-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-16802-4_35
Mannari CSerramazza DSalvatori E(2022)PH-Remix PrototypeLinking Theory and Practice of Digital Libraries10.1007/978-3-031-16802-4_31(344-350)Online publication date: 20-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-16802-4_31
Jakobsen MRavier ADardha O(2021)Papaya: Global Typestate Analysis of Aliased ObjectsProceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming10.1145/3479394.3479414(1-13)Online publication date: 6-Sep-2021
https://dl.acm.org/doi/10.1145/3479394.3479414
Rocha PCaires L(2021)Propositions-as-types and shared stateProceedings of the ACM on Programming Languages10.1145/34735845:ICFP(1-30)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473584
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

High-Level Test Synthesis: A Survey from Synthesis Process Flow Perspective

Layout-driven RTL binding techniques for high-level synthesis

High-Level Synthesis: Past, Present, and Future