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.
Saved in:
Superior document: | Lecture Notes in Computer Science Series ; v.13990 |
---|---|
: | |
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
|
Online Access: | |
Physical Description: | 1 online resource (579 pages) |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
id |
5007239158 |
---|---|
ctrlnum |
(MiAaPQ)5007239158 (Au-PeEL)EBL7239158 (OCoLC)1376355114 |
collection |
bib_alma |
record_format |
marc |
spelling |
Wies, Thomas. 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. 1st ed. Cham : Springer International Publishing AG, 2023. Ã2023. 1 online resource (579 pages) text txt rdacontent computer c rdamedia online resource cr rdacarrier Lecture Notes in Computer Science Series ; v.13990 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. Description based on publisher supplied metadata and other sources. Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2024. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries. Electronic books. Print version: Wies, Thomas Programming Languages and Systems Cham : Springer International Publishing AG,c2023 9783031300431 ProQuest (Firm) Lecture Notes in Computer Science Series https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=7239158 Click to View |
language |
English |
format |
eBook |
author |
Wies, Thomas. |
spellingShingle |
Wies, Thomas. 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. Lecture Notes in Computer Science Series ; 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. |
author_facet |
Wies, Thomas. |
author_variant |
t w tw |
author_sort |
Wies, Thomas. |
title |
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. |
title_sub |
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. |
title_full |
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. |
title_fullStr |
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. |
title_full_unstemmed |
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. |
title_auth |
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. |
title_new |
Programming Languages and Systems : |
title_sort |
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. |
series |
Lecture Notes in Computer Science Series ; |
series2 |
Lecture Notes in Computer Science Series ; |
publisher |
Springer International Publishing AG, |
publishDate |
2023 |
physical |
1 online resource (579 pages) |
edition |
1st ed. |
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. |
isbn |
9783031300448 9783031300431 |
callnumber-first |
Q - Science |
callnumber-subject |
QA - Mathematics |
callnumber-label |
QA76 |
callnumber-sort |
QA 276.76 C65 |
genre |
Electronic books. |
genre_facet |
Electronic books. |
url |
https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=7239158 |
illustrated |
Not Illustrated |
oclc_num |
1376355114 |
work_keys_str_mv |
AT wiesthomas programminglanguagesandsystems32ndeuropeansymposiumonprogrammingesop2023heldaspartoftheeuropeanjointconferencesontheoryandpracticeofsoftwareetaps2023parisfranceapril22272023proceedings |
status_str |
n |
ids_txt_mv |
(MiAaPQ)5007239158 (Au-PeEL)EBL7239158 (OCoLC)1376355114 |
carrierType_str_mv |
cr |
hierarchy_parent_title |
Lecture Notes in Computer Science Series ; v.13990 |
is_hierarchy_title |
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. |
container_title |
Lecture Notes in Computer Science Series ; v.13990 |
marc_error |
Info : Unimarc and ISO-8859-1 translations identical, choosing ISO-8859-1. --- [ 856 : z ] |
_version_ |
1792331066020724736 |
fullrecord |
<?xml version="1.0" encoding="UTF-8"?><collection xmlns="http://www.loc.gov/MARC21/slim"><record><leader>06110nam a22004213i 4500</leader><controlfield tag="001">5007239158</controlfield><controlfield tag="003">MiAaPQ</controlfield><controlfield tag="005">20240229073848.0</controlfield><controlfield tag="006">m o d | </controlfield><controlfield tag="007">cr cnu||||||||</controlfield><controlfield tag="008">240229s2023 xx o ||||0 eng d</controlfield><datafield tag="020" ind1=" " ind2=" "><subfield code="a">9783031300448</subfield><subfield code="q">(electronic bk.)</subfield></datafield><datafield tag="020" ind1=" " ind2=" "><subfield code="z">9783031300431</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(MiAaPQ)5007239158</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(Au-PeEL)EBL7239158</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(OCoLC)1376355114</subfield></datafield><datafield tag="040" ind1=" " ind2=" "><subfield code="a">MiAaPQ</subfield><subfield code="b">eng</subfield><subfield code="e">rda</subfield><subfield code="e">pn</subfield><subfield code="c">MiAaPQ</subfield><subfield code="d">MiAaPQ</subfield></datafield><datafield tag="050" ind1=" " ind2="4"><subfield code="a">QA76.76.C65</subfield></datafield><datafield tag="100" ind1="1" ind2=" "><subfield code="a">Wies, Thomas.</subfield></datafield><datafield tag="245" ind1="1" ind2="0"><subfield code="a">Programming Languages and Systems :</subfield><subfield code="b">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.</subfield></datafield><datafield tag="250" ind1=" " ind2=" "><subfield code="a">1st ed.</subfield></datafield><datafield tag="264" ind1=" " ind2="1"><subfield code="a">Cham :</subfield><subfield code="b">Springer International Publishing AG,</subfield><subfield code="c">2023.</subfield></datafield><datafield tag="264" ind1=" " ind2="4"><subfield code="c">Ã2023.</subfield></datafield><datafield tag="300" ind1=" " ind2=" "><subfield code="a">1 online resource (579 pages)</subfield></datafield><datafield tag="336" ind1=" " ind2=" "><subfield code="a">text</subfield><subfield code="b">txt</subfield><subfield code="2">rdacontent</subfield></datafield><datafield tag="337" ind1=" " ind2=" "><subfield code="a">computer</subfield><subfield code="b">c</subfield><subfield code="2">rdamedia</subfield></datafield><datafield tag="338" ind1=" " ind2=" "><subfield code="a">online resource</subfield><subfield code="b">cr</subfield><subfield code="2">rdacarrier</subfield></datafield><datafield tag="490" ind1="1" ind2=" "><subfield code="a">Lecture Notes in Computer Science Series ;</subfield><subfield code="v">v.13990</subfield></datafield><datafield tag="505" ind1="0" ind2=" "><subfield code="a">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).</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">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.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">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.</subfield></datafield><datafield tag="588" ind1=" " ind2=" "><subfield code="a">Description based on publisher supplied metadata and other sources.</subfield></datafield><datafield tag="590" ind1=" " ind2=" "><subfield code="a">Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2024. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries. </subfield></datafield><datafield tag="655" ind1=" " ind2="4"><subfield code="a">Electronic books.</subfield></datafield><datafield tag="776" ind1="0" ind2="8"><subfield code="i">Print version:</subfield><subfield code="a">Wies, Thomas</subfield><subfield code="t">Programming Languages and Systems</subfield><subfield code="d">Cham : Springer International Publishing AG,c2023</subfield><subfield code="z">9783031300431</subfield></datafield><datafield tag="797" ind1="2" ind2=" "><subfield code="a">ProQuest (Firm)</subfield></datafield><datafield tag="830" ind1=" " ind2="0"><subfield code="a">Lecture Notes in Computer Science Series</subfield></datafield><datafield tag="856" ind1="4" ind2="0"><subfield code="u">https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=7239158</subfield><subfield code="z">Click to View</subfield></datafield></record></collection> |