فهرست مطالب
Preface
Organization
On-The-Fly Verification via Incremental, Interactive Abstract Interpretation with CiaoPP and VeriFly (Invited Talk)
Contents
Keynote
Unification Modulo Equational Theories in Languages with Binding Operators (Invited Talk)
References
Horn Clauses Analysis, Transformation and Synthesis
Design Datalog Templates for Synthesizing Bidirectional Programs from Tabular Examples
1 Introduction
2 Background
2.1 Relational Databases and NR-Datalog
2.2 Bidirectional Program
2.3 Functional Dependencies: Constraints and Effects
2.4 ProSynth
3 Overview
4 Forward-Propagating FDs
5 Templatizing Minimal-Effect View Update Strategies
6 Templatizing Constraints and Effects of FDs
6.1 Templatizing the Constraints of FDs
6.2 Templatizing the Effects of FDs
7 Implementation
8 Related Work
9 Conclusion
References
Transforming Big-Step to Small-Step Semantics Using Interpreter Specialisation
1 Introduction
2 Background
3 A Small-Step Interpreter for Big-Step Semantics
4 Examples
5 Related Work
References
Constrained Horn Clauses Satisfiability via Catamorphic Abstractions
1 Introduction
2 Basic Notions
3 An Introductory Example
4 CHC Transformation via Catamorphic Abstractions
4.1 Catamorphic Abstractions and Catamorphic Abstraction Specifications
4.2 Transformation Rules
4.3 The Transformation Algorithm Tabs
5 Implementation and Experimental Evaluation
6 Conclusions and Related Work
References
Static Analysis and Type Systems
A Reusable Machine-Calculus for Automated Resource Analyses
1 Introduction
2 Context and State of the Art
2.1 Amortized Analysis
2.2 Automated Amortized Resource Analysis and RAML
2.3 dlPCF and lambda-amor
2.4 Abstract Interpretation for Resource Analysis
2.5 Our Technical Setup
3 The ILL-Calculus
3.1 Generalities
3.2 Linear Fragment
3.3 Call-By-Value Semantics
3.4 Non-linear Fragment
4 Type System
4.1 Generalities
4.2 Datatypes with Parameters
4.3 Implementing Polymorphism
4.4 An Example of Encoding: append
4.5 Soundness
5 Embedding AARA as an Effect
5.1 An Effect for Parameters
5.2 Polymorphic State-Passing Effect
5.3 Token Encoding
5.4 Potential in Shared Values
6 Implementation for ML-Like Languages
7 Conclusion
References
A Rule-Based Approach for Designing and Composing Abstract Domains
1 Introduction
2 Preliminaries
3 The Approach
4 Inferring Program Properties Using Rule-Based Combined Domains
5 Conclusions
References
A Logical Interpretation of Asynchronous Multiparty Compatibility
1 Introduction
2 CP and Classical Linear Logic
3 Multiparty Compatibility
4 Asynchronous Forwarders
5 Composing Processes with Asynchronous Forwarders
6 Related Work
7 Conclusions and Future Work
References
Relational Solver for Java Generics Type System
1 Introduction
2 Relational Programming, Verifiers, and Solvers
3 Java Generics
4 Relational Subtyping Solver
5 Evaluation
6 Conclusion
References
Unification and Substitution in (C)LP
Predicate Anti-unification in (Constraint) Logic Programming
1 Introduction
2 Preliminaries
3 Predicate Anti-unification
4 Computing Common Generalizations
4.1 Terms and Literals
4.2 Predicates
5 Conclusions and Future Work
References
A Term Matching Algorithm and Substitution Generality
1 Introduction
2 Preliminaries
2.1 Term
2.2 Variable Substitution
2.3 Generality
2.4 Unification
2.5 Relaxed Core Representation
2.6 Partial Renaming
3 Term Matching (Subsumption)
4 The Term Matching Algorithm TMAT
5 Applications
5.1 Deciding Substitution Generality
5.2 Illustration: Subtleties of ``\'\'
5.3 Deciding Substitution Equigenerality
5.4 Most General Unifiers and Their Possible Relevance
6 Summary
References
Knowledge Representation and AI-Based Learning
A Novel EGs-Based Framework for Systematic Propositional-Formula Simplification
1 Introduction
2 Background and Notation
3 Preprocessing Framework
3.1 Simplification Rules
3.2 Rules Properties
4 Discussion and Future Work
5 Conclusion
References
From Static to Dynamic Access Control Policies via Attribute-Based Category Mining
1 Introduction
2 Preliminaries
2.1 The Category-Based Metamodel
2.2 Policy Mining
3 Policy Mining Algorithm Overview
4 Category Mining Proof of Concept - Use Cases
5 Related Work
6 Conclusions and Future Work
References
Towards a Certified Proof Checker for Deep Neural Network Verification
1 Introduction
2 Background
2.1 DNN Verification
2.2 Proof Production for DNN Verification
3 The Imandra Proof Checker
4 Specification of the Proof Checker\'s Correctness
5 Discussion and Future Work
References
Author Index
Organization
On-The-Fly Verification via Incremental, Interactive Abstract Interpretation with CiaoPP and VeriFly (Invited Talk)
Contents
Keynote
Unification Modulo Equational Theories in Languages with Binding Operators (Invited Talk)
References
Horn Clauses Analysis, Transformation and Synthesis
Design Datalog Templates for Synthesizing Bidirectional Programs from Tabular Examples
1 Introduction
2 Background
2.1 Relational Databases and NR-Datalog
2.2 Bidirectional Program
2.3 Functional Dependencies: Constraints and Effects
2.4 ProSynth
3 Overview
4 Forward-Propagating FDs
5 Templatizing Minimal-Effect View Update Strategies
6 Templatizing Constraints and Effects of FDs
6.1 Templatizing the Constraints of FDs
6.2 Templatizing the Effects of FDs
7 Implementation
8 Related Work
9 Conclusion
References
Transforming Big-Step to Small-Step Semantics Using Interpreter Specialisation
1 Introduction
2 Background
3 A Small-Step Interpreter for Big-Step Semantics
4 Examples
5 Related Work
References
Constrained Horn Clauses Satisfiability via Catamorphic Abstractions
1 Introduction
2 Basic Notions
3 An Introductory Example
4 CHC Transformation via Catamorphic Abstractions
4.1 Catamorphic Abstractions and Catamorphic Abstraction Specifications
4.2 Transformation Rules
4.3 The Transformation Algorithm Tabs
5 Implementation and Experimental Evaluation
6 Conclusions and Related Work
References
Static Analysis and Type Systems
A Reusable Machine-Calculus for Automated Resource Analyses
1 Introduction
2 Context and State of the Art
2.1 Amortized Analysis
2.2 Automated Amortized Resource Analysis and RAML
2.3 dlPCF and lambda-amor
2.4 Abstract Interpretation for Resource Analysis
2.5 Our Technical Setup
3 The ILL-Calculus
3.1 Generalities
3.2 Linear Fragment
3.3 Call-By-Value Semantics
3.4 Non-linear Fragment
4 Type System
4.1 Generalities
4.2 Datatypes with Parameters
4.3 Implementing Polymorphism
4.4 An Example of Encoding: append
4.5 Soundness
5 Embedding AARA as an Effect
5.1 An Effect for Parameters
5.2 Polymorphic State-Passing Effect
5.3 Token Encoding
5.4 Potential in Shared Values
6 Implementation for ML-Like Languages
7 Conclusion
References
A Rule-Based Approach for Designing and Composing Abstract Domains
1 Introduction
2 Preliminaries
3 The Approach
4 Inferring Program Properties Using Rule-Based Combined Domains
5 Conclusions
References
A Logical Interpretation of Asynchronous Multiparty Compatibility
1 Introduction
2 CP and Classical Linear Logic
3 Multiparty Compatibility
4 Asynchronous Forwarders
5 Composing Processes with Asynchronous Forwarders
6 Related Work
7 Conclusions and Future Work
References
Relational Solver for Java Generics Type System
1 Introduction
2 Relational Programming, Verifiers, and Solvers
3 Java Generics
4 Relational Subtyping Solver
5 Evaluation
6 Conclusion
References
Unification and Substitution in (C)LP
Predicate Anti-unification in (Constraint) Logic Programming
1 Introduction
2 Preliminaries
3 Predicate Anti-unification
4 Computing Common Generalizations
4.1 Terms and Literals
4.2 Predicates
5 Conclusions and Future Work
References
A Term Matching Algorithm and Substitution Generality
1 Introduction
2 Preliminaries
2.1 Term
2.2 Variable Substitution
2.3 Generality
2.4 Unification
2.5 Relaxed Core Representation
2.6 Partial Renaming
3 Term Matching (Subsumption)
4 The Term Matching Algorithm TMAT
5 Applications
5.1 Deciding Substitution Generality
5.2 Illustration: Subtleties of ``\'\'
5.3 Deciding Substitution Equigenerality
5.4 Most General Unifiers and Their Possible Relevance
6 Summary
References
Knowledge Representation and AI-Based Learning
A Novel EGs-Based Framework for Systematic Propositional-Formula Simplification
1 Introduction
2 Background and Notation
3 Preprocessing Framework
3.1 Simplification Rules
3.2 Rules Properties
4 Discussion and Future Work
5 Conclusion
References
From Static to Dynamic Access Control Policies via Attribute-Based Category Mining
1 Introduction
2 Preliminaries
2.1 The Category-Based Metamodel
2.2 Policy Mining
3 Policy Mining Algorithm Overview
4 Category Mining Proof of Concept - Use Cases
5 Related Work
6 Conclusions and Future Work
References
Towards a Certified Proof Checker for Deep Neural Network Verification
1 Introduction
2 Background
2.1 DNN Verification
2.2 Proof Production for DNN Verification
3 The Imandra Proof Checker
4 Specification of the Proof Checker\'s Correctness
5 Discussion and Future Work
References
Author Index
