Cover Image

Programming Languages and Systems : 30th European Symposium on Programming, ESOP 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings.

Bibliographic Details
Main Author: Yoshida, Nobuko.
Format: eBook
Language:English
Published: Cham : Springer International Publishing AG, 2021.
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
  • The Decidability of Verification under PS 2.0
  • 1 Introduction
  • 2 Preliminaries
  • 3 The Promising Semantics
  • 4 Undecidability of Consistent Reachability in PS 2.0
  • 5 Decidable Fragments of PS 2.0
  • 5.1 Formal Model of LoHoW
  • 5.2 Decidability of LoHoW with Bounded Promises
  • 6 Source to Source Translation
  • 6.1 Translation Maps
  • 7 Implementation and Experimental Results
  • 8 Related Work and Conclusion
  • References
  • Data Flow Analysis of Asynchronous Systems using Infinite Abstract Domains
  • 1 Introduction
  • 1.1 Motivating Example: Leader election
  • 1.2 Challenges in property checking
  • 1.3 Our Contributions
  • 2 Background and Terminology
  • 2.1 Modeling of Asynchronous Message Passing Systems as VCFGs
  • 2.2 Data flow analysis over iVCFGs
  • 3 Backward DFAS Approach
  • 3.1 Assumptions and Definitions
  • 3.2 Properties of Demand and Covering
  • 3.3 Data Flow Analysis Algorithm
  • 3.4 Illustration
  • 3.5 Properties of the algorithm
  • 4 Forward DFAS Approach
  • 5 Implementation and Evaluation
  • 5.1 Benchmarks and modeling
  • 5.2 Data flow analysis results
  • 5.3 Limitations and Threats to Validity
  • 6 Related Work
  • 7 Conclusions and Future Work
  • References
  • Types for Complexity of Parallel Computation in Pi-Calculus
  • 1 Introduction
  • 2 The Pi-calculus with Semantics for Work and Span
  • 2.1 Syntax, Congruence and Standard Semantics for π-Calculus
  • 2.2 Semantics and Complexity
  • 2.3 An Example Process
  • 3 Size Types for the Work
  • 3.1 Size Input/Output Types
  • 3.2 Subject Reduction
  • 4 Types for Parallel Complexity
  • 4.1 Size Types with Time
  • 4.2 Examples
  • 4.3 Complexity Results
  • 5 An Example: Bitonic Sort
  • 6 Related Work
  • 7 Perspectives
  • Acknowledgements
  • References.
  • Checking Robustness Between Weak Transactional Consistency Models-5pt
  • 1 Introduction
  • 2 Overview
  • 3 Consistency Models
  • 3.1 Robustness
  • 4 Robustness Against CC Relative to PC
  • 5 Robustness Against PC Relative to SI
  • 6 Proving Robustness Using Commutativity DependencyGraphs
  • 7 Experimental Evaluation
  • 8 Related Work
  • References
  • Verified Software Units
  • 1 Introduction
  • 2 Program verification using VST
  • 3 VSU calculus
  • 3.1 Components and soundness
  • 3.2 Derived rules
  • 4 APDs and specification interfaces
  • 4.1 Abstract predicate declarations (APDs)
  • 4.2 Abstract specification interfaces (ASIs)
  • 4.3 Verification of ASI-specified compilation units
  • 4.4 A VSU for a malloc-free library
  • 4.5 Putting it all together
  • 5 Modular verification of the Subject/Observer pattern
  • 5.1 Specification and proof reuse
  • 5.2 Pattern-level specification
  • 6 Verification of object principles
  • 7 Discussion
  • References
  • An Automated Deductive Verification Framework for Circuit-building Quantum Programs
  • 1 Introduction
  • 1.1 Quantum computing
  • 1.2 The hybrid model.
  • 1.3 The problem with quantum algorithms.
  • 1.4 Goal and challenges.
  • 1.5 Proposal.
  • 1.6 Contributions.
  • 1.7 Discussion.
  • 2 Background: Quantum Algorithms and Programs
  • 2.1 Quantum data manipulation.
  • 2.2 Quantum circuits.
  • 2.3 Reasoning on circuits and the matrix semantics.
  • 2.4 Path-sum representation.
  • 3 Introducing PPS
  • 3.1 Motivating example.
  • 3.2 Parametrizing path-sums.
  • 4 Qbricks-DSL
  • 4.1 Syntax of Qbricks-DSL.
  • 4.2 Operational semantics.
  • 4.3 Properties.
  • 4.4 Universality and usability of the chosen circuit constructs.
  • 4.5 Validity of circuits.
  • 4.6 Denotational semantics.
  • 5 Qbricks-Spec
  • 5.1 Syntax of Qbricks-Spec.
  • 5.2 The types pps and ket.
  • 5.3 Denotational semantics of the new types.
  • 5.4 Regular sequents in Qbricks-Spec.
  • 5.5 Parametricity of PPS.
  • 5.6 Standard matrix semantics and correctness of PPS semantics.
  • 6 Reasoning on Quantum Programs
  • 6.1 HQHL judgments.
  • 6.2 Deduction rules for term constructs.
  • 6.3 Deduction rules for pps.
  • 6.4 Equational reasoning.
  • 6.5 Additional deductive rules.
  • 7 Implementation
  • 8 Case studies and experimental evaluation
  • 8.1 Examples of formal specifications.
  • 8.2 Experimental evaluation.
  • 8.3 Prior verification efforts.
  • 8.4 Evaluation: benefits of PPS and Qbricks.
  • 9 Related works
  • 10 Conclusion
  • Acknowledgments.
  • References
  • Nested Session Types
  • 1 Introduction
  • 2 Overview of Nested Session Types
  • 3 Description of Types
  • 4 Type Equality
  • 4.1 Type Equality Definition
  • 4.2 Decidability of Type Equality
  • 5 Practical Algorithm for Type Equality
  • 5.1 Type Equality Declarations
  • 6 Formal Language Description
  • 6.1 Basic Session Types
  • 6.2 Type Safety
  • 7 Relationship to Context-Free Session Types
  • 8 Implementation
  • 9 More Examples
  • 10 Further Related Work
  • 11 Conclusion
  • References
  • Coupled Relational Symbolic Execution for Differential Privacy
  • 1 Introduction
  • 2 CRSE Informally
  • 3 Preliminaries
  • 4 Concrete languages
  • 4.1 PFOR
  • 4.2 RPFOR
  • 5 Symbolic languages
  • 5.1 SPFOR
  • 5.2 SRPFOR
  • 6 Metatheory
  • 7 Strategies for counterexample finding
  • 8 Examples
  • 9 Related Works
  • 10 Conclusion
  • References
  • Graded Hoare Logic and its Categorical Semantics
  • 1 Introduction
  • 2 Overview of GHL and Prospectus of its Model
  • 3 Loop Language and Graded Hoare Logic
  • 3.1 Preliminaries
  • 3.2 The Loop Language
  • 3.3 Assertion Logic
  • 3.4 Graded Hoare Logic
  • 3.5 Example Instantiations of GHL
  • 4 Graded Categories
  • 4.1 Homogeneous Coproducts in Graded Categories.
  • 4.2 Graded Freyd Categories with Countable Coproducts
  • 4.3 Semantics of The Loop Language in Freyd Categories
  • 5 Modelling Graded Hoare Logic
  • 5.1 Interpretation of the Assertion Logic using Fibrations
  • 5.2 Interpretation of Graded Hoare Logic
  • 5.3 Instances of Graded Hoare Logic
  • 6 Related Work
  • 7 Conclusion
  • References
  • Do Judge a Test by its Cover
  • 1 Introduction
  • 2 Classical Combinatorial Testing
  • 3 Generalizing Coverage
  • 4 Sparse Test Descriptions
  • 4.1 Encoding "Eventually"
  • 4.2 Defining Coverage
  • 5 Thinning Generators with QuickCover
  • 5.1 Online Generator Thinning
  • 6 Evaluation
  • 6.1 Case Study: Normalization Bugs in System F
  • 6.2 Case Study: Strictness Analysis Bugs in GHC
  • 7 Related Work
  • 7.1 Generalizations of Combinatorial Testing
  • 7.2 Comparison with Enumerative Property-Based Testing
  • 7.3 Comparison with Fuzzing Techniques
  • 8 Conclusion and Future Work
  • 8.1 Variations
  • 8.2 Combinatorial Coverage of More Types
  • 8.3 Regular Tree Expressions for Directed Generation
  • Acknowledgments
  • References
  • For a Few Dollars More
  • 1 Introduction
  • 2 Specification of Algorithms With Resources
  • 2.1 Nondeterministic Computations With Resources
  • 2.2 Atomic Operations and Control Flow
  • 2.3 Refinement on NREST
  • 2.4 Refinement Patterns
  • 3 LLVM With Cost Semantics
  • 3.1 Basic Monad
  • 3.2 Shallowly Embedded LLVM Semantics
  • 3.3 Cost Model
  • 3.4 Reasoning Setup
  • 3.5 Primitive Setup
  • 4 Automatic Refinement
  • 4.1 Heap nondeterminism refinement
  • 4.2 The Sepref Tool
  • 4.3 Extracting Hoare Triples
  • 4.4 Attain Supremum
  • 5 Case Study: Introsort
  • 5.1 Specification of Sorting
  • 5.2 Introsort's Idea
  • 5.3 Quicksort Scheme
  • 5.4 Final Insertion Sort
  • 5.5 Separating Correctness and Complexity Proofs
  • 5.6 Refining to LLVM
  • 5.7 Benchmarks
  • 6 Conclusions
  • 6.1 Related Work.
  • 6.2 Future Work
  • References
  • Run-time Complexity Bounds Using Squeezers
  • 1 Introduction
  • 2 Overview
  • 3 Complexity Analysis based on Squeezers
  • 3.1 Time complexity as a function of rank
  • 3.2 Complexity decomposition by partitioned simulation
  • 3.3 Extraction of recurrence relations over ranks
  • 3.4 Establishing the requirements of the recurrence relations extraction
  • 3.5 Trace-length vs. state-size recurrences with squeezers
  • 4 Synthesis
  • 4.1 SyGuS
  • 4.2 Verification
  • 5 Empirical Evaluation
  • 5.1 Experiments
  • 5.2 Case study: Subsets example
  • 6 Related Work
  • 7 Conclusion
  • Acknowledgements.
  • References
  • Complete trace models of state and control
  • 1 Introduction
  • 2 HOSC
  • 3 HOSC[HOSC]
  • 3.1 Names and abstract values
  • 3.2 Actions and traces
  • 3.3 Extended syntax and reduction
  • 3.4 Configurations
  • 3.5 Transitions
  • 3.6 Correctness and full abstraction
  • 4 GOSC[HOSC]
  • 5 HOS[HOSC]
  • 6 GOS[HOSC]
  • 7 Concluding remarks
  • 8 Related Work
  • References
  • Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols
  • 1 Introduction
  • 2 Session Types
  • 3 Session Coalgebra
  • 3.1 Alternative Presentation of Session Coalgebras
  • 3.2 Coalgebra of Session Types
  • 4 Type Equivalence, Duality and Subtyping
  • 4.1 Bisimulation
  • 4.2 Duality
  • 4.3 Parallelizability
  • 4.4 Simulation and Subtyping
  • 4.5 Decidability
  • 5 Typing Rules
  • 5.1 A Session π-calculus
  • 5.2 Typing Rules
  • 6 Algorithmic Type Checking
  • 7 Concluding Remarks
  • References
  • Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages
  • 1 Introduction
  • 2 A Motivating Example from Phylogenetics
  • 3 A Calculus for Probabilistic Programming Languages
  • 3.1 Syntax
  • 3.2 Semantics
  • 3.3 Resampling Semantics
  • 4 The Target Measure of a Program
  • 4.1 A Measure Space over Traces.
  • 4.2 A Measurable Space over Terms.

Similar Items