상세정보

Invited Contributions.- Programming by Examples: PL meets ML.- Synthesizing SystemC Code from Delay Hybrid CSP.- Security.- Taming Message-passing Communication in Compositional Reasoning about Confidentiality.- Capabilities for Java: Secure Access to Resources.- Enforcing Programming Guidelines with Region-Types and Effects.- Automatically generating secure wrappers for SGX enclaves from separation logic specifications.- Heap and Equivalence Reasoning.- Black-box equivalence checking across compiler optimizations.- Weakly Sensitive Analysis for Unbounded Iteration over JavaScript Objects.- Decision Procedure for Entailment of Symbolic Heaps with Arrays.- Bringing order to the separation logic jungle.- Concurrency and Verification.- Programming and proving with classical types.- Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-vous.- Verified Root-Balanced Trees.- Safety and Liveness of MCS Lock - Layer by Layer.- Domain-Specific Languages.- Palgol: A High-Level DSL for Vertex-Centric Graph Processing with Remote Data Access.- Efficient Functional Reactive Programming through Incremental Behaviors.- Implementing Algebraic Effects in C - Monads for Free in C.- Sound and Efficient Language-Integrated Query: Maintaining the ORDER.- Semantics.- A Computational Interpretation of Context-Free Expressions.- Partiality and container monads.- The Negligible and Yet Subtle Cost of Pattern Matching.- A lambda calculus for density matrices wth classical and probabilistic controls.- Numerical Reasoning.- Compact Difference Bound Matrices.- Sharper and Simpler Nonlinear Interpolants for Program Verification.- A Nonstandard Functional Programming Language.- Counterexample-Guided Bit-Precision Selection.

정보제공 :

Intro -- Preface -- Organization -- Abstracts of Invited Talks -- Relational Verification of Higher-Order Probabilistic Programs -- Programming by Examples: PL Meets ML -- Gradual Enforcement of Program Invariants -- Synthesizing SystemC Code from Delay Hybrid CSP -- Contents -- Invited Contributions -- Programming by Examples: PL Meets ML -- 1 Introduction -- 2 Applications -- 2.1 Data Wrangling -- 2.2 Code Transformations -- 3 PL Meets ML -- 3.1 A Perspective on PL Meets ML -- 3.2 Using ML to Improve PBE -- 4 Search Algorithm -- 4.1 Domain-Specific Language -- 4.2 Deductive Search Methodology -- 4.3 ML-Based Search Algorithm -- 5 Ranking -- 5.1 Ranking Based on Program Structure -- 5.2 Ranking Based on Test Inputs -- 5.3 ML-based Ranking Function -- 6 Interactivity -- 6.1 Clustering of Strings -- 7 Future Directions -- 8 Conclusion -- References -- Synthesizing SystemC Code from Delay Hybrid CSP -- 1 Introduction -- 1.1 Related Work -- 2 Preliminaries -- 2.1 Delay Dynamical Systems -- 2.2 SystemC -- 3 Delay Hybrid CSP (dHCSP) -- 3.1 Syntax of dHCSP -- 3.2 Semantics of dHCSP -- 3.3 Approximate Bisimulation on dHCSP -- 4 Discretization of dHCSP -- 4.1 Discretization of DDE (DDEs) in Bounded Time -- 4.2 Discretization of dHCSP in Bounded Time -- 4.3 Correctness of the Discretization -- 5 From Discretized dHCSP to SystemC -- 6 Case Study -- 7 Conclusion -- References -- Security -- Taming Message-Passing Communication in Compositional Reasoning About Confidentiality -- 1 Introduction -- 2 Motivation and Approach at a Glance -- 3 Model of Computation -- 4 Attacker Model and Baseline Security -- 5 Compositional Reasoning About Noninterference -- 5.1 Annotated Programs -- 5.2 Process-Local Security Condition -- 5.3 Compositional Reasoning About Information-Flow Security -- 5.4 Instrumented Semantics and Sound Use of Assumptions -- 5.5 Soundness of Compositional Reasoning -- 6 Security Type System and Evaluation -- 6.1 Judgment and Typing Rules -- 6.2 Soundness -- 6.3 Examples of Typable Programs -- 7 Related Work -- 8 Conclusion -- References -- Capabilities for Java: Secure Access to Resources -- 1 Introduction -- 1.1 Java Security -- 1.2 Java Security Issues -- 1.3 Contributions -- 2 Classes and Interfaces as Capabilities -- 3 Capabilities for Java -- 3.1 Securing Capabilities -- 3.2 Generating Capabilities -- 3.3 Heterogeneous Data Structures -- 3.4 Methods of Class Object -- 4 Semantics of Capabilities -- 5 Implementation of Capabilities -- 6 Related Work -- 7 Conclusions and Future Work -- References -- Enforcing Programming Guidelines with Region Types and Effects -- 1 Introduction -- 2 Formalizing Programming Guidelines -- 3 Featherweight Java with Updates, Casts, and Strings -- 3.1 Syntax -- 3.2 Semantics -- 4 Region-Based Type and Effect Systems -- 4.1 Refined Types, Effects, and Type System Parameters -- 4.2 Declarative Type System -- 4.3 Semi-declarative Type System -- 4.4 Algorithmic Type System -- 5 Experimental Evaluation -- 5.1 Implemen.