InhaltsangabeDistributed Electronic Rights in JavaScript.- The Compiler Forest.- Pretty-Big-Step Semantics.- Language Constructs for Non-Well-Founded Computation.- Laziness by Need.- FliPpr: A Prettier Invertible Printing System.- Slicing-Based Trace Analysis of Rewriting Logic Specifications with iJULIENNE.- Why3 - Where Programs Meet Provers.- Compositional Invariant Checking for Overlaid and Nested Linked Lists.- A Discipline for Program Verification Based on Backpointers and Its Use in Observational Disjointness.- Modular Reasoning about Separation of Concurrent Data Structures.- Ribbon Proofs for Separation Logic.- Abstract Refinement Types.- Constraining Delimited Control with Contracts.- Verifying Concurrent Memory Reclamation Algorithms with Grace.- Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels.- Verifying Concurrent Programs against Sequential Specifications.- On Distributability in Process Calculi.- Behavioral Polymorphism and Parametricity in Session-Based Communication.- Higher-Order Processes, Functions, and Sessions: A Monadic Integration.- Concurrent Flexible Reversibility.- Structural Lock Correlation with Ownership Types.- Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems.- Model-Checking Higher-Order Programs with Recursive Types.- Counterexample-Guided Precondition Inference.- Information Reuse for Multi-goal Reachability Analyses.- Quarantining Weakness: Compositional Reasoning under Relaxed Memory Models (Extended Abstract).- Software Verification for Weak Memory via Program Transformation.- Checking and Enforcing Robustness against TSO.- GADTs Meet Subtyping.- A Data Driven Approach for Algebraic Loop Invariants.- Automatic Type Inference for Amortised Heap-Space Analysis.

InhaltsangabeDistributed Electronic Rights in JavaScript.- The Compiler Forest.- Pretty-Big-Step Semantics.- Language Constructs for Non-Well-Founded Computation.- Laziness by Need.- FliPpr: A Prettier Invertible Printing System.- Slicing-Based Trace Analysis of Rewriting Logic Specifications with iJULIENNE.- Why3 - Where Programs Meet Provers.- Compositional Invariant Checking for Overlaid and Nested Linked Lists.- A Discipline for Program Verification Based on Backpointers and Its Use in Observational Disjointness.- Modular Reasoning about Separation of Concurrent Data Structures.- Ribbon Proofs for Separation Logic.- Abstract Refinement Types.- Constraining Delimited Control with Contracts.- Verifying Concurrent Memory Reclamation Algorithms with Grace.- Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels.- Verifying Concurrent Programs against Sequential Specifications.- On Distributability in Process Calculi.- Behavioral Polymorphism and Parametricity in Session-Based Communication.- Higher-Order Processes, Functions, and Sessions: A Monadic Integration.- Concurrent Flexible Reversibility.- Structural Lock Correlation with Ownership Types.- Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems.- Model-Checking Higher-Order Programs with Recursive Types.- Counterexample-Guided Precondition Inference.- Information Reuse for Multi-goal Reachability Analyses.- Quarantining Weakness: Compositional Reasoning under Relaxed Memory Models (Extended Abstract).- Software Verification for Weak Memory via Program Transformation.- Checking and Enforcing Robustness against TSO.- GADTs Meet Subtyping.- A Data Driven Approach for Algebraic Loop Invariants.- Automatic Type Inference for Amortised Heap-Space Analysis.