Letonchanh's List: Memory

• On the verification problem for weak memory models
• Compositional may-must program analysis: unleashing the power of alternation
• Low-level liquid types
•   Static determination of quantitative resource usage for higher-order programs

2 more annotations...

• Relaxed memory models: an operational approach
• Automated verification of practical garbage collectors

• Cyclic proofs of program termination in separation logic
•   Back to the future: revisiting precise program verification using SMT solvers
• Demand-driven alias analysis for C

1 more annotation...

• Cork: dynamic memory leak detection for garbage-collected languages

• Adventures in time and space
• Hybrid type checking

• Separation logic and abstraction
• Permission accounting in separation logic
• Region-based shape analysis with tracked locations
• The Java memory model

2 more annotations...

• Local reasoning about a copying garbage collector
•   Abstractions from proofs
• A type system for well-founded recursion

1 more annotation...

• A type theory for memory allocation and data layout
•   Static prediction of heap space usage for first-order functional programs
• Interprocedural compatibility analysis for static object preallocation
•   A real-time garbage collector with low overhead and consistent utilization

2 more annotations...

• The SLAM project: debugging system software via static analysis
• Mining specifications
• Role analysis
• Lazy abstraction
• Bounding space usage of conservative garbage collectors
•   Predicate abstraction for software verification
• Resource usage analysis

5 more annotations...

• BI as an assertion language for mutable data structures
• Stratified operational semantics for safety and correctness of the region calculus
• Type-preserving garbage collectors

1 more annotation...

• Resource bound certification
• Reducing sweep time for a nearly empty heap

• Robert Atkey: Amortised Resource Analysis with Separation Logic Logical Methods in Computer Science 7(2): (2011)
• David Aspinall, Robert Atkey, Kenneth MacKenzie, Donald Sannella: Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode. TGC 2010: 1-22

• Elvira Albert, Samir Genaim, Miguel Gómez-Zamalloa, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa: Simulating Concurrent Behaviors with Worst-Case Cost Bounds. FM 2011: 353-368
• Elvira Albert, Samir Genaim, Miguel Gómez-Zamalloa: Parametric inference of memory requirements for garbage collected languages. ISMM 2010: 121-130
• Elvira Albert, Samir Genaim, Miguel Gómez-Zamalloa: Live heap space analysis for languages with garbage collection. ISMM 2009: 129-138
• Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, Damiano Zanardini: Cost Analysis of Java Bytecode. ESOP 2007: 157-172

2 more annotations...

•   Predicate abstraction and refinement for verifying multi-threaded programs
• Multivariate amortized resource analysis
• Space overhead bounds for dynamic memory management with partial compaction

1 more annotation...