ROPAS
Survey Workshop on Resource Bound Checking

Program Organizer : JungTaek Kim

Period : Apr 6 ~ May 13

---

• Overview
• Location
• Schedule
• List of papers

---

Overview

  "Resource Bound Checking" is a technique by which one can estimate the upper bound of some needed resource or check constraints on the upper bound. Resource can be CPU, memory, network bandwidth, or etc. Estimating the resource bound is very hard to be accurate, so some work only check the constraints on the resource bound which is provided by programmer.
  In this survey, volunteers will present some papers about the resource bound checking technique.

---

Location

  Rm. 1215, Industrial Management building, KAIST

---

Schedule

Date	Time	Present by	Papers are
4/6	4:30 ~ 6:00	Kwangkeun Yi	Flexible type analysis ( abstract , ps, slide)
4/8	9:00 ~ 10:30	Kwangkeun Yi	Resource Bound Certification ( abstract , ps, slide)
4/8	10:30 ~ 12:00	JungTaek Kim	Automatic Complexity Analysis ( abstract , hardcopy - at ROPAS, slide)
4/12	4:30 ~ 6:00	Sun-Ae Seo	A compositional approach to time analysis of first order lazy functional programs ( abstract , hardcopy - at ROPAS, slide)
4/12	7:00 ~ 8:30	Hyunjun Eo	Complexity analysis for a lazy higher-order language ( abstract , ps, slide)
4/15	9:00 ~ 10:30	Oukseh Lee	Polymorphic Time Systems for Estimating Program Complexity ( abstract, pdf, slide )
4/15	10:30 ~ 12:00	Nikolay Shilov	A na\"{i}ve time analysis and its theory of cost equivalence ( abstract , ps, slides )
4/19	4:30 ~ 6:00	Sukyoung Ryu	Static dependent costs for estimating execution time ( abstract , pdf, slide )
4/19	7:00 ~ 8:30	JungTaek Kim	Sized types ( abstract , ps, slide)
4/22	9:00 ~ 10:30	Hyunjun Eo	Intensional polymorphism in type-erasure semantics ( abstract , ps, slide)
4/22	10:30 ~ 12:00	JungTaek Kim	Proving the correctness of reactive systems using sized types ( abstract , ps, slide)
4/27	4:30 ~ 6:00	Sukyoung Ryu	Linear types and non-size increasing polynomial time computation ( abstract , pdf, slide)
4/27	7:00 ~ 8:30	Bomshik Kim	Dependent types in practical programming ( abstract , pdf, slide)
4/29	9:00 ~ 10:30	JungTaek Kim	Calculating Sized Types ( abstract , ps)
4/29	10:30 ~ 12:00	Sun-Ae Seo	Typed Memory Management in a Calculus of Capabilities. ( abstract , ps, slide)
5/3	4:30 ~ 6:00	JungTaek Kim	Static Analysis of Store Use in Functional Programs ( abstract , hardcopy - at ROPAS, slide)
5/3	7:00 ~ 8:30	Oukseh Lee	Better Static Memory Management : Improving Region-Based Analysis of Higher-Order Languages ( abstract , ps, slide)
5/20	9:00 ~ 10:00	Oukseh Lee	Recursion and dynamic data structures in bounded space : Towards embedded ML programming (abstract, paper, slide)
5/20	10:00 ~ 11:00	Sun-Ae Seo	Guaranteeing Good Memory Bound for Parallel Programs ( abstract , pdf, slide)
5/20	11:00 ~ 12:00	JungTaek Kim	Extensibility, safety and performance in the SPIN operating system ( abstract , ps)
5/24	4:30 ~ 6:00	Nikolay Shilov	Temporal proof methodologies for real-time systems ( abstract , pdf, slides )
5/24	7:00 ~ 8:00	Kwangkeun Yi	Safe kernel extensions without runtime checking Proof-Carrying Code Efficient Representation & Validation of Proofs ( abstract , ps , slide)

---

List of papers

• Opening.
  • Flexible type analysis. ( abstract , ps, slide)
  • Resource Bound Certification ( abstract , ps, slide)
• Time consumption bound analyses
  • Automatic Complexity Analysis ( abstract , hardcopy - at ROPAS, slide)
  • A compositional approach to time analysis of first order lazy functional programs. ( abstract , hardcopy - at ROPAS, slide)
  • Complexity analysis for a lazy higher-order language. ( abstract , ps, slide)
  • Polymorphic Time Systems for Estimating Program Complexity. ( abstract , pdf)
  • A na\"{i}ve time analysis and its theory of cost equivalence. ( abstract , ps)
  • Static dependent costs for estimating execution time. ( abstract , pdf)
• Type systems related to resource bound checking
  • Sized types. ( abstract , ps)
  • Intensional polymorphism in type-erasure semantics. ( abstract , ps, slide)
  • Calculating Sized Types. ( abstract , ps)
  • Linear types and non-size increasing polynomial time computation. ( abstract , pdf)
  • Dependent types in practical programming. ( abstract , pdf)
• Memory consumption bound analyses
  • Static Analysis of Store Use in Functional Programs ( abstract , hardcopy - at ROPAS)
  • Better Static Memory Management : Improving Region-Based Analysis of Higher-Order Languages ( abstract , ps)
  • Typed Memory Management in a Calculus of Capabilities. ( abstract , ps, slide)
  • Eliminating Array Bound Checking Through Dependent Types. ( abstract , pdf)
  • Recursion and dynamic data structures in bounded space : Towards embedded ML programming. ( abstract , ps)
  • Guaranteeing Good Memory Bound for Parallel Programs. ( abstract , pdf, slide)
• Other areas related to resource bound checking
  • Extensibility, safety and performance in the SPIN operating system ( abstract , ps)
  • Proving the correctness of reactive systems using sized types. ( abstract , ps)
  • Safe kernel extensions without runtime checking. ( abstract , ps , slide)
  • Proof-carrying code. ( abstract , ps , slide)
• Additional papers
  • Temporal proof methodologies for real-time systems ( abstract , pdf)

---

Research on Program Analysis System