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

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) Cryptography (94A60)

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)

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