Tests and Proofs: 16th International Conference, TAP 2022, Held as Part of STAF 2022, Nantes, France, July 5, 2022, Proceedings (Lecture Notes in Computer Science)

This book constitutes the proceedings of the 16th International Conference on Tests and Proofs, TAP 2022, which was held as part of Software Technologies: Applications and Foundations, STAF 2022, and took place in Nantes, France in July 2022. The 6 full papers together with 1 invited extended abstract included in this volume were carefully reviewed and selected from 11 submissions. They were organized in topical sections on formal analysis, and proofs, and effective testing. Preface Organization Contents Invited Talk Automatic Test-Case Generation with CoVeriTest (Extended Abstract) 1 The CoVeriTest Framework 1.1 Cooperation 1.2 Adjusting Individual Analysis Time Limits 2 CoVeriTest Implementation and Evaluation References Formal Analysis and Proofs Reach on Register Automata via History Independence 1 Introduction 2 Preliminaries 2.1 Logical Operations 2.2 Register Automata 3 History Independence 4 Backwards-Propagation Algorithm 4.1 Well-Constrained Transitions 4.2 Iterative History Independence Transformation 5 Evaluation 5.1 Automata Wiki Benchmarks 5.2 Random Automata 5.3 Threats to Validity 6 Conclusion References Bddl: A Type System for Binary Decision Diagrams 1 Introduction 2 Background: Binary Decision Diagrams 2.1 Binary Decision Diagrams 2.2 Canonical Binary Decision Diagrams 2.3 Encoding Sets and Relations with BDDs 3 Motivation 4 The Bddl Language 5 Typing, Semantics, and Soundness 5.1 Types 5.2 Typing Rules 5.3 Subtyping 5.4 Semantics and Soundness 6 Related Work 7 Conclusion References Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction 1 Introduction 1.1 Motivating Example 1.2 Background 2 Proof by Induction in Isabelle/HOL 3 Overview of SeLFiE 4 Syntactic Reasoning in LiFtEr 4.1 LiFtEr: Logical Feature Extraction 4.2 Naive Generalization Heuristic in LiFtEr 5 Semantic Reasoning in SeLFiE 5.1 Semantics-Aware Logical Feature Extraction 5.2 Semantics-Aware Generalization Heuristic 6 Case Studies and Evaluations 6.1 Interactive Recommendation System 6.2 Automatic Proof Search Using SeLFiE 7 Conclusion 8 Related Work References Effective Testing Fuzzing and Delta Debugging And-Inverter Graph Verification Tools 1 Introduction 2 Fuzzing, Delta Debugging and AIGs 3 Generation-based Fuzzing for Multipliers 4 Mutation-based Fuzzing for AIGs 5 Delta Debugging with Slices 6 Fuzzing, Tests and Proofs 7 Experiments 7.1 MultAIGenFuzzer Generates Multipliers 7.2 Using AIGoFuzzing to Mutate AIGs 7.3 Combining Generation- and Mutation-Based Fuzzing 7.4 Using AIGdd2 Minimize Failure-Inducing Inputs 7.5 Summary 8 Conclusion References A Unit-Based Symbolic Execution Method for Detecting Heap Overflow Vulnerability in Executable Codes 1 Introduction 2 Method Overview 2.1 Static Analysis 2.2 Processing the Test Units 2.3 Learning and Simulation Process 2.4 Test Data Generation 3 Evaluation 3.1 Experiment 1 3.2 Experiment 2 4 Conclusion and Future Works References Conformance Testing of Formal Semantics Using Grammar-Based Fuzzing 1 Introduction 2 Approach 2.1 Deriving a Test Oracle from a Formal Semantics 2.2 Generate Random Solidity Code 2.3 Testing Algorithm 2.4 Example Smart Contract 3 Evaluation 3.1 Examples of Detected Issues 3.2 Statistics 4 Related Work 5 Discussion 6 Conclusion References Author Index