Cover Image

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.

Bibliographic Details
Main Author: Wies, Thomas.
Format: eBook
Language:English
Published: Cham : Springer International Publishing AG, 2023.
Edition:1st ed.
Series:Lecture Notes in Computer Science Series
Subjects:
Electronic books.
Online Access:Click to View
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.

Similar Items