Programming Languages and Systems : : 32nd European Symposium on Programming, ESOP 2023, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings.

• Superior document: Lecture Notes in Computer Science Series ; v.13990
• Author: Wies, Thomas.
• Place / Publishing House: Cham : : Springer International Publishing AG,, 2023.; Ã2023.
• Year of Publication: 2023
• Edition: 1st ed.
• Language: English
• Series: Lecture Notes in Computer Science Series
• Physical Description: 1 online resource (579 pages)

Table of Contents

Intro -- ETAPS Foreword -- Preface -- Organization -- Contents -- Logics for Extensional, Locally Complete Analysis via Domain Refinements -- 1 Introduction -- 2 Background -- 2.1 Abstract Interpretation -- 2.2 Regular Commands. -- 3 Local Completeness Logic -- 4 Refining Abstract Domain -- 4.1 Logical Completeness -- 4.2 Derived Refinement Rules -- 4.3 Choosing The Refinement -- 5 Conclusions -- Appendix A Proofs and Supplementary Material -- A.1 Extensional Soundness (Theorem 2) -- A.2 Soundness and Completeness of (refine-ext ) -- A.3 Derived Refinement Rules -- References -- Clustered Relational Thread-ModularAbstract Interpretation with Local Traces -- 1 Introduction -- 2 Relational Domains -- 3 A Local Trace Semantics -- 4 Relational Analyses as Abstractions of Local Traces -- 5 Refinement via Finite Abstractions of Local Traces -- 6 Analysis of Thread Ids and Uniqueness -- 7 Exploiting Thread IDs to Improve Relational Analyses -- 8 Exploiting Clustered Relational Domains -- 9 Experimental Evaluation -- 10 Related Work -- 11 Conclusion and Future Work -- References -- Adversarial Reachability for Program-level Security Analysis -- 1 Introduction -- 2 Motivation -- 2.1 Fault Injection across Security Fields -- 2.2 Motivating Example -- 3 Background -- 3.1 Software-implemented Fault Injection (SWiFI) -- 3.2 Standard Reachability Formalization -- 3.3 Symbolic Execution -- 4 Adversarial Reachability -- 5 Forkless Adversarial Symbolic Execution (FASE) -- 5.1 Modelling Faults via Forkless Encoding -- 5.2 Building Adversarial Path Predicates -- 5.3 Algorithm Properties -- 5.4 Optimization via Early Detection of Fault Saturation (FASE-EDS) -- 5.5 Optimization via Injection on Demand (FASE-IOD) -- 5.6 Optimizations Combination -- 6 Implementation -- 7 Evaluation -- 7.1 Experimental Setting -- 7.2 Correctness and Completeness in Practice (RQ1).

7.3 Scalability (RQ2) -- 7.4 Performance Optimization (RQ3) -- 7.5 Other Experiments and Fault Models -- 8 Case Study: the WooKey Bootloader -- 9 Discussion -- 10 Related Work -- 11 Conclusion -- Automated Grading of Regular Expressions -- Builtin Types Viewed as Inductive Families -- Pragmatic Gradual Polymorphism with References -- Modal Crash Types for Intermittent Computing -- Gradual Tensor Shape Checking -- A Type System for Effect Handlersand Dynamic Labels -- Interpreting Knowledge-based Programs -- Contextual Modal Type Theory with Polymorphic Contexts -- A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests -- 1 Introduction -- 2 Overview -- 3 Introducing Skip-free GKAT -- 3.1 Skip-free Semantics -- 3.2 Axioms -- 4 1-free Star Expressions -- 5 Completeness for Skip-free Bisimulation GKAT -- 5.1 Transforming skip-free automata to labelled transition systems -- 5.2 Translating Syntax -- 6 Completeness for Skip-free GKAT -- 7 Relation to GKAT -- 7.1 Bisimulation semantics -- 7.2 Language semantics -- 7.3 Equivalences -- 8 Related Work -- 9 Discussion -- References -- Quorum Tree Abstractions of Consensus Protocols -- MAG: Types for Failure-Prone Communication -- System F-mu-omega with Context-free Session Types -- Safe Session-Based Concurrency with Shared Linear State -- Bunched Fuzz: Sensitivity for Vector Metrics -- Fast and Correct Gradient-Based Optimisationfor Probabilistic Programming via Smoothing -- Type-safe Quantum Programming in Idris -- Automatic Alignment in Higher-Order Probabilistic Programming Languages -- 1 Introduction -- 2 A Motivating Example -- 2.1 Aligned SMC -- 2.2 Aligned Lightweight MCMC -- 3 Syntax and Semantics -- 3.1 Syntax -- 3.2 Semantics -- 4 Alignment Analysis -- 4.1 A-Normal Form and Alignment -- 4.2 Alignment Analysis -- 4.3 Dynamic Alignment -- 5 Aligned SMC and MCMC -- 5.1 Aligned SMC.

5.2 Aligned Lightweight MCMC -- 6 Implementation -- 7 Evaluation -- 7.1 SMC: Constant Rate Birth-Death (CRBD) -- 7.2 SMC: Cladogenetic Diversification Rate Shift (ClaDS) -- 7.3 SMC: State-Space Aircraft Localization -- 7.4 MCMC: Latent Dirichlet Allocation (LDA) -- 7.5 MCMC: Constant Rate Birth-Death (CRBD) -- 8 Related Work -- 9 Conclusion -- References -- Correction to: Programming Languages and Systems -- Correction to: T. Wies (Ed.): Programming Languages and Systems, LNCS 13990, https://doi.org/10.1007/978-3-031-30044-8 -- Author Index.