Programming languages and systems : 19th European symposium on programming, ESOP 2010, held as part of the joint European conferences on theory and practice of software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010 : proceedings

Annotation. This Book Constitutes The Refereed Proceedings Of The 19th European Symposium On Programming, Esop 2010, Held In Paphos, Cyprus, In March 2010, As Part Of Etaps 2010, The European Joint Conferences On Theory And Practice Of Software. The 30 Revised Full Papers, Presented Together With Two Invited Talks (one Abstract And One Full), Were Carefully Reviewed And Selected From 121 Full Paper Submissions. The Topics Addressed Include Programming Paradigms And Styles, Methods And Tools To Write And Specify Programs And Languages, Methods And Tools For Reasoning About Programs, Methods And Tools For Implementation, And Concurrency And Distribution. Front Matter....Pages - The Audacity of Hope: Thoughts on Reclaiming the Database Dream....Pages 1-1 Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions....Pages 2-22 Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis....Pages 23-42 Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays....Pages 43-63 A Semantic Framework for Declassification and Endorsement....Pages 64-84 Amortised Resource Analysis with Separation Logic....Pages 85-103 A PolyTime Functional Language from Light Linear Logic....Pages 104-124 Testing Polymorphic Properties....Pages 125-144 Formal Verification of Coalescing Graph-Coloring Register Allocation....Pages 145-164 A Theory of Speculative Computation....Pages 165-184 Propositional Interpolation and Abstract Interpretation....Pages 185-204 Functional Programming in Sublinear Space....Pages 205-225 Logical Concurrency Control from Sequential Proofs....Pages 226-245 Fluid Updates: Beyond Strong vs. Weak Updates....Pages 246-266 Parameterized Memory Models and Concurrent Separation Logic....Pages 267-286 Amortized Resource Analysis with Polynomial Potential....Pages 287-306 Generative Operational Semantics for Relaxed Memory Models....Pages 307-326 Automating Security Mediation Placement....Pages 327-344 TRX: A Formally Verified Parser Interpreter....Pages 345-365 On the Expressive Power of Primitives for Compensation Handling....Pages 366-386 Separating Shape Graphs....Pages 387-406 Deadlock-Free Channels and Locks....Pages 407-426 Verifying a Compiler for Java Threads....Pages 427-447 A Grammar-Based Approach to Invertible Programs....Pages 448-467 Faulty Logic: Reasoning about Fault Tolerant Programs....Pages 468-487 A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While....Pages 488-506 A Universal Calculus for Stream Processing Languages....Pages 507-528 Enforcing Stateful Authorization and Information Flow Policies in Fine ....Pages 529-549 Stateful Contracts for Affine Types....Pages 550-569 CFA2: A Context-Free Approach to Control-Flow Analysis....Pages 570-589 Weighted Dynamic Pushdown Networks....Pages 590-609 Explicit Stabilisation for Modular Rely-Guarantee Reasoning....Pages 610-629 Back Matter....Pages -