Resource bound certification

DOI10.1145/325694.325716MaRDI QIDQ5178852zbMATH OpenOpenAlexFDO

Authors Karl Crary, Stephanie Weirich

Publication date 17 March 2015

Published in Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/325694.325716

Mathematics Subject Classification ID

Cryptography (94A60) Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Programming Languages and Systems
• Formal Certification of a Resource-Aware Language Implementation
• scientific article; zbMATH DE number 1335897
• Certified complexity (CerCo)
• scientific article; zbMATH DE number 4197469
• Tools and Algorithms for the Construction and Analysis of Systems
• From complementation to certification
• The query complexity of certification

Cited in

(28)

• Automated techniques for provably safe mobile code.
• Oracle-guided scheduling for controlling granularity in implicitly parallel languages
• Denotational semantics as a foundation for cost recurrence extraction for functional languages
• Programming Languages and Systems
• Distributed call-tracking for security
• A Coq library for internal verification of running-times
• Closed-form upper bounds in static cost analysis
• Termination checking with types
• Linear dependent types in a call-by-value scenario
• Programming Languages and Systems
• A type system for counting instances of software components
• More Typed Assembly Languages for Confidentiality
• Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis
• Worst-case input generation for concurrent programs under non-monotone resource metrics
• Semantic foundations for cost analysis of pipeline-optimized programs
• Typable fragments of polynomial automatic amortized resource analysis
• Certified abstract cost analysis
• FM 2005: Formal Methods
• Space-aware ambients and processes
• Logic for Programming, Artificial Intelligence, and Reasoning
• A Type System for Usage of Software Components
• Cost analysis of object-oriented bytecode programs
• Verified Root-Balanced Trees
• More precise yet widely applicable cost analysis
• Amortized complexity verified
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• Safety Guarantees from Explicit Resource Management
• A type system for lock-free processes

This page was built for publication: Resource bound certification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5178852)