Kooperativer Bibliotheksverbund

UID:

Format: 1 Online-Ressource

ISBN: 9783030720193

Series Statement: Lecture notes in computer science 12648

Additional Edition: Erscheint auch als Druck-Ausgabe, Paperback ISBN 978-3-030-72018-6

Language: English

Subjects: Computer Science

Keywords: Programmverifikation ; Programmanalyse ; Nebenläufigkeit ; Programmiersprache ; Typsystem ; Formale Methode ; Konferenzschrift

DOI: 10.1007/978-3-030-72019-3

URL: Volltext  (kostenfrei)

URL: Volltext  (kostenfrei)

UID:

Format: 1 online resource (705 pages)

ISBN: 9783030720193

Series Statement: Lecture Notes in Computer Science Ser. ; v.12648

Note: 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.

Additional Edition: Print version: Yoshida, Nobuko Programming Languages and Systems Cham : Springer International Publishing AG,c2021 ISBN 9783030720186

Language: English

Keywords: Electronic books. ; Electronic books

URL: Click to View

URL: Full-text  ((OIS Credentials Required))

URL: lizenzpflichtig

UID:

Format: 1 Online-Ressource (693 p.)

ISBN: 9783030720193

Series Statement: Lecture Notes in Computer Science; Theoretical Computer Science and General Issues

Content: This open access book constitutes the proceedings of the 30th European Symposium on Programming, ESOP 2021, which was held during March 27 until April 1, 2021, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021. The conference was planned to take place in Luxembourg and changed to an online format due to the COVID-19 pandemic. The 24 papers included in this volume were carefully reviewed and selected from 79 submissions. They deal with fundamental issues in the specification, design, analysis, and implementation of programming languages and systems

Note: English

Language: English

URL: kostenfrei

URL: https://av.tib.eu/series/1142/30th+european+symposium+on+programming+esop+2021

UID:

Format: 1 online resource (705 pages)

Edition: 1st ed. 2021.

ISBN: 3-030-72019-5

Series Statement: Theoretical Computer Science and General Issues, 12648

Content: This open access book constitutes the proceedings of the 30th European Symposium on Programming, ESOP 2021, which was held during March 27 until April 1, 2021, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021. The conference was planned to take place in Luxembourg and changed to an online format due to the COVID-19 pandemic. The 24 papers included in this volume were carefully reviewed and selected from 79 submissions. They deal with fundamental issues in the specification, design, analysis, and implementation of programming languages and systems.

Note: The Decidability of Verification under PS 2.0 -- Data Flow Analysis of Asynchronous Systems using Infinite Abstract Domains -- Types for Complexity of Parallel Computation in Pi-Calculus -- Checking Robustness Between Weak Transactional Consistency Models -- Verified Software Units -- An Automated Deductive Verication Framework for Circuit-building Quantum Programs -- Nested Session Types -- Coupled Relational Symbolic Execution for Differential Privacy -- Graded Hoare Logic and its Categorical Semantics -- Do Judge a Test by its Cover: Combining Combinatorial and Property-Based Testing -- For a Few Dollars More – Verified Fine-Grained Algorithm Analysis Down to LLVM -- Run-time Complexity Bounds Using Squeezers -- Complete trace models of state and control -- Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols -- Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages -- Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere -- Graded Modal Dependent Type Theory -- Automated Termination Analysis of Polynomial Probabilistic Programs -- Bayesian strategies: probabilistic programs as generalised graphical models -- Temporal Refinements for Guarded Recursive Types -- Query Lifting: Language-integrated query for heterogeneous nested collections -- Reverse AD at Higher Types: Pure, Principled and Denotationally Correct -- Sound and Complete Concolic Testing for Higher-order Functions -- Strong-Separation Logic. . , English

Additional Edition: ISBN 3-030-72018-7

Language: English

DOI: 10.1007/978-3-030-72019-3

UID:

Format: 1 online resource (xii, 693 pages) : , illustrations.

ISBN: 9783030720193 , 3030720195

Series Statement: Lecture notes in computer science ; 12648

Content: This open access book constitutes the proceedings of the 30th European Symposium on Programming, ESOP 2021, which was held during March 27 until April 1, 2021, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021. The conference was planned to take place in Luxembourg and changed to an online format due to the COVID-19 pandemic. The 24 papers included in this volume were carefully reviewed and selected from 79 submissions. They deal with fundamental issues in the specification, design, analysis, and implementation of programming languages and systems.

Note: The Decidability of Verification under PS 2.0 -- Data Flow Analysis of Asynchronous Systems using Infinite Abstract Domains -- Types for Complexity of Parallel Computation in Pi-Calculus -- Checking Robustness Between Weak Transactional Consistency Models -- Verified Software Units -- An Automated Deductive Verication Framework for Circuit-building Quantum Programs -- Nested Session Types -- Coupled Relational Symbolic Execution for Differential Privacy -- Graded Hoare Logic and its Categorical Semantics -- Do Judge a Test by its Cover: Combining Combinatorial and Property-Based Testing -- For a Few Dollars More – Verified Fine-Grained Algorithm Analysis Down to LLVM -- Run-time Complexity Bounds Using Squeezers -- Complete trace models of state and control -- Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols -- Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages -- Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere -- Graded Modal Dependent Type Theory -- Automated Termination Analysis of Polynomial Probabilistic Programs -- Bayesian strategies: probabilistic programs as generalised graphical models -- Temporal Refinements for Guarded Recursive Types -- Query Lifting: Language-integrated query for heterogeneous nested collections -- Reverse AD at Higher Types: Pure, Principled and Denotationally Correct -- Sound and Complete Concolic Testing for Higher-order Functions -- Strong-Separation Logic.

In: Springer Nature eBook

Additional Edition: Print version: 9783030720186

Language: English

Keywords: Electronic books. ; Electronic books. ; Conference papers and proceedings.

DOI: 10.1007/978-3-030-72019-3

URL: SpringerLink

URL: Click here to view book

UID:

Format: XII, 693 p. 177 illus. , online resource.

Edition: 1st ed. 2021.

ISBN: 9783030720193

Series Statement: Theoretical Computer Science and General Issues ; 12648

Content: This open access book constitutes the proceedings of the 30th European Symposium on Programming, ESOP 2021, which was held during March 27 until April 1, 2021, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021. The conference was planned to take place in Luxembourg and changed to an online format due to the COVID-19 pandemic. The 24 papers included in this volume were carefully reviewed and selected from 79 submissions. They deal with fundamental issues in the specification, design, analysis, and implementation of programming languages and systems.

Note: The Decidability of Verification under PS 2.0 -- Data Flow Analysis of Asynchronous Systems using Infinite Abstract Domains -- Types for Complexity of Parallel Computation in Pi-Calculus -- Checking Robustness Between Weak Transactional Consistency Models -- Verified Software Units -- An Automated Deductive Verication Framework for Circuit-building Quantum Programs -- Nested Session Types -- Coupled Relational Symbolic Execution for Differential Privacy -- Graded Hoare Logic and its Categorical Semantics -- Do Judge a Test by its Cover: Combining Combinatorial and Property-Based Testing -- For a Few Dollars More - Verified Fine-Grained Algorithm Analysis Down to LLVM -- Run-time Complexity Bounds Using Squeezers -- Complete trace models of state and control -- Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols -- Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages -- Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere -- Graded Modal Dependent Type Theory -- Automated Termination Analysis of Polynomial Probabilistic Programs -- Bayesian strategies: probabilistic programs as generalised graphical models -- Temporal Refinements for Guarded Recursive Types -- Query Lifting: Language-integrated query for heterogeneous nested collections -- Reverse AD at Higher Types: Pure, Principled and Denotationally Correct -- Sound and Complete Concolic Testing for Higher-order Functions -- Strong-Separation Logic. .

In: Springer Nature eBook

Additional Edition: Printed edition: ISBN 9783030720186

Additional Edition: Printed edition: ISBN 9783030720209

Language: English

DOI: 10.1007/978-3-030-72019-3

URL: https://doi.org/10.1007/978-3-030-72019-3

URL: https://doi.org/10.1007/978-3-030-72019-3

UID:

Format: 1 Online-Ressource(XII, 693 p. 177 illus.)

Edition: 1st ed. 2021.

ISBN: 9783030720193

Series Statement: Theoretical Computer Science and General Issues 12648

Content: The Decidability of Verification under PS 2.0 -- Data Flow Analysis of Asynchronous Systems using Infinite Abstract Domains -- Types for Complexity of Parallel Computation in Pi-Calculus -- Checking Robustness Between Weak Transactional Consistency Models -- Verified Software Units -- An Automated Deductive Verication Framework for Circuit-building Quantum Programs -- Nested Session Types -- Coupled Relational Symbolic Execution for Differential Privacy -- Graded Hoare Logic and its Categorical Semantics -- Do Judge a Test by its Cover: Combining Combinatorial and Property-Based Testing -- For a Few Dollars More – Verified Fine-Grained Algorithm Analysis Down to LLVM -- Run-time Complexity Bounds Using Squeezers -- Complete trace models of state and control -- Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols -- Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages -- Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere -- Graded Modal Dependent Type Theory -- Automated Termination Analysis of Polynomial Probabilistic Programs -- Bayesian strategies: probabilistic programs as generalised graphical models -- Temporal Refinements for Guarded Recursive Types -- Query Lifting: Language-integrated query for heterogeneous nested collections -- Reverse AD at Higher Types: Pure, Principled and Denotationally Correct -- Sound and Complete Concolic Testing for Higher-order Functions -- Strong-Separation Logic. .

Content: This open access book constitutes the proceedings of the 30th European Symposium on Programming, ESOP 2021, which was held during March 27 until April 1, 2021, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021. The conference was planned to take place in Luxembourg and changed to an online format due to the COVID-19 pandemic. The 24 papers included in this volume were carefully reviewed and selected from 79 submissions. They deal with fundamental issues in the specification, design, analysis, and implementation of programming languages and systems.

Note: Open Access

Additional Edition: ISBN 9783030720186

Additional Edition: ISBN 9783030720209

Additional Edition: Erscheint auch als Druck-Ausgabe ISBN 9783030720186

Additional Edition: Erscheint auch als Druck-Ausgabe ISBN 9783030720209

Language: English

DOI: 10.1007/978-3-030-72019-3

URL: kostenfrei

UID:

Format: 1 online resource (705 pages)

Edition: 1st ed. 2021.

ISBN: 3-030-72019-5

Series Statement: Theoretical Computer Science and General Issues, 12648

Content: This open access book constitutes the proceedings of the 30th European Symposium on Programming, ESOP 2021, which was held during March 27 until April 1, 2021, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021. The conference was planned to take place in Luxembourg and changed to an online format due to the COVID-19 pandemic. The 24 papers included in this volume were carefully reviewed and selected from 79 submissions. They deal with fundamental issues in the specification, design, analysis, and implementation of programming languages and systems.

Note: The Decidability of Verification under PS 2.0 -- Data Flow Analysis of Asynchronous Systems using Infinite Abstract Domains -- Types for Complexity of Parallel Computation in Pi-Calculus -- Checking Robustness Between Weak Transactional Consistency Models -- Verified Software Units -- An Automated Deductive Verication Framework for Circuit-building Quantum Programs -- Nested Session Types -- Coupled Relational Symbolic Execution for Differential Privacy -- Graded Hoare Logic and its Categorical Semantics -- Do Judge a Test by its Cover: Combining Combinatorial and Property-Based Testing -- For a Few Dollars More – Verified Fine-Grained Algorithm Analysis Down to LLVM -- Run-time Complexity Bounds Using Squeezers -- Complete trace models of state and control -- Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols -- Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages -- Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere -- Graded Modal Dependent Type Theory -- Automated Termination Analysis of Polynomial Probabilistic Programs -- Bayesian strategies: probabilistic programs as generalised graphical models -- Temporal Refinements for Guarded Recursive Types -- Query Lifting: Language-integrated query for heterogeneous nested collections -- Reverse AD at Higher Types: Pure, Principled and Denotationally Correct -- Sound and Complete Concolic Testing for Higher-order Functions -- Strong-Separation Logic. . , English

Additional Edition: ISBN 3-030-72018-7

Language: English

DOI: 10.1007/978-3-030-72019-3

UID:

Format: 1 online resource (705 pages)

Edition: 1st ed. 2021.

ISBN: 3-030-72019-5

Series Statement: Theoretical Computer Science and General Issues, 12648

Content: This open access book constitutes the proceedings of the 30th European Symposium on Programming, ESOP 2021, which was held during March 27 until April 1, 2021, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021. The conference was planned to take place in Luxembourg and changed to an online format due to the COVID-19 pandemic. The 24 papers included in this volume were carefully reviewed and selected from 79 submissions. They deal with fundamental issues in the specification, design, analysis, and implementation of programming languages and systems.

Note: The Decidability of Verification under PS 2.0 -- Data Flow Analysis of Asynchronous Systems using Infinite Abstract Domains -- Types for Complexity of Parallel Computation in Pi-Calculus -- Checking Robustness Between Weak Transactional Consistency Models -- Verified Software Units -- An Automated Deductive Verication Framework for Circuit-building Quantum Programs -- Nested Session Types -- Coupled Relational Symbolic Execution for Differential Privacy -- Graded Hoare Logic and its Categorical Semantics -- Do Judge a Test by its Cover: Combining Combinatorial and Property-Based Testing -- For a Few Dollars More – Verified Fine-Grained Algorithm Analysis Down to LLVM -- Run-time Complexity Bounds Using Squeezers -- Complete trace models of state and control -- Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols -- Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages -- Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere -- Graded Modal Dependent Type Theory -- Automated Termination Analysis of Polynomial Probabilistic Programs -- Bayesian strategies: probabilistic programs as generalised graphical models -- Temporal Refinements for Guarded Recursive Types -- Query Lifting: Language-integrated query for heterogeneous nested collections -- Reverse AD at Higher Types: Pure, Principled and Denotationally Correct -- Sound and Complete Concolic Testing for Higher-order Functions -- Strong-Separation Logic. . , English

Additional Edition: ISBN 3-030-72018-7

Language: English

DOI: 10.1007/978-3-030-72019-3

UID:

Format: 1 Online-Ressource.

ISBN: 978-3-030-72019-3

Series Statement: Lecture notes in computer science 12648

Additional Edition: Erscheint auch als Druck-Ausgabe, Paperback ISBN 978-3-030-72018-6

Language: English

Subjects: Computer Science

Keywords: Programmverifikation ; Programmanalyse ; Nebenläufigkeit ; Programmiersprache ; Typsystem ; Formale Methode ; Konferenzschrift

DOI: 10.1007/978-3-030-72019-3

URL: Volltext  (kostenfrei)

URL: Volltext  (kostenfrei)