Automated technology for verification and analysis : 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18-21, 2021, proceedings

This book constitutes the refereed proceedings of the 19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021, held in Gold Coast, Australia in October 2021. The symposium is dedicated to promoting research in theoretical and practical aspects of automated analysis, verification and synthesis by providing an international venue for the researchers to present new results. The 19 regular papers presented together with 4 tool papers and 1 invited paper were carefully reviewed and selected from 75 submissions. The papers are divided into the following topical sub-headings: Automata Theory; Machine learning for Formal Methods; Theorem Proving and Tools; Model Checking; Probabilistic Analysis; Software and Hardware Verification; System Synthesis and Approximation; and Verification of Machine Learning. Preface Organization Geometric Theory for Program Testing (Abstract of a Keynote Talk) Contents Invited Paper Linear Temporal Logic – From Infinite to Finite Horizon 1 Reactive Systems and Reactive Synthesis 2 LTL Synthesis over Finite Traces 3 Synthesis Using Finite-Word Automata References Automata Theory Determinization and Limit-Determinization of Emerson-Lei Automata 1 Introduction 2 Preliminaries 3 From TELA to Generalized Büchi Automata 3.1 Operations on Emerson-Lei Automata 3.2 Construction of Generalized Büchi Automata 4 Determinization 5 Limit-Deterministic TELA 5.1 Limit-Determinization 5.2 Probabilistic Model Checking 6 Experimental Evaluation 7 Conclusion References Automatic Discovery of Fair Paths in Infinite-State Transition Systems 1 Introduction 2 Background 3 Funnels and Funnel Loops 4 Automated Synthesis of Funnel Loops 5 Related Work 6 Experimental Evaluation 7 Conclusions and Future Work References Certifying DFA Bounds for Recognition and Separation 1 Introduction 2 Preliminaries 3 Proving and Refuting Bounds on DFAs 4 Certifying Bounds on Recognizability 4.1 Certification with Offline Refuters 4.2 Certification with Online Refuters 5 Bounds on DFA Separation 5.1 Hardness of Separation 5.2 Certifying Bounds on Separation 6 Discussion and Directions for Future Research References Machine Learning for Formal Methods AALpy: An Active Automata Learning Library 1 Introduction 2 AALpy – Intuitive Automata Learning in Python 3 Experimental Evaluation 4 Conclusion References Learning Linear Temporal Properties from Noisy Data: A MaxSAT-Based Approach 1 Introduction 2 Preliminaries 3 Problem Formulation 4 Learning Minimal LTL Formulas 4.1 MaxSAT 4.2 The Learning Algorithm 5 Learning Decision Trees over LTL Formulas 5.1 Decision Trees over LTL Formulas 5.2 The Learning Algorithm 5.3 LTL Formulas for Decision Nodes 5.4 Stopping Criterion 6 Experimental Evaluation 7 Conclusion References Mining Interpretable Spatio-Temporal Logic Properties for Spatially Distributed Systems 1 Introduction 2 Background 2.1 Spatio-temporal Reach and Escape Logic (STREL) 3 Constructing a Spatial Model 4 Learning STREL Formulas from Data 5 Case Studies 6 Related Work and Conclusion References Theorem Proving and Tools A Formal Semantics of the GraalVM Intermediate Representation 1 Introduction 2 GraalVM IR 3 Graph Model in Isabelle/HOL 4 Data-Flow Semantics 5 Local Control-Flow Semantics 6 Global Control-Flow Semantics 7 Validation of Execution Semantics 8 Proving Optimizations 9 Related Work 10 Conclusions References A Verified Decision Procedure for Orders in Isabelle/HOL 1 Introduction 1.1 Related Work 1.2 Contributions 1.3 Notation 2 A Semantics for Orders 3 Deciding Partial Orders 4 Deciding Linear Orders 5 Certification with Proof Terms 5.1 Basic Proof System for Partial Orders 5.2 Dealing with Strict Literals Through Rewriting 6 Refinement to Executable Specification 7 From Exported Code to Integrated Proof Tactic 8 Conclusion References PJBDD: A BDD Library for Java and Multi-Threading 1 Introduction 2 Design and Implementation Details 3 Architecture of the Library 4 Experimental Evaluation 5 Conclusion References Model Checking Live Synthesis 1 Introduction 2 Running Example – Relay Station 3 Preliminaries 4 Live Updates 5 A Temporal Language for Live Updates 5.1 LiveLTL 5.2 Obligations 6 Model Checking and Synthesis 6.1 Model Checking Live Updates 6.2 Live Synthesis 7 Case Study 7.1 Benchmark Families 7.2 Observations 8 Related Work 9 Conclusion References Faster Pushdown Reachability Analysis with Applications in Network Verification 1 Introduction 2 Preliminaries 3 Formal Model of MPLS Networks 3.1 MPLS Network Verification 3.2 From Query Satisfiability to Pushdown Reachability 4 Improving Pushdown System Reachability Analysis 4.1 Early Termination of Reachability Algorithms 4.2 Combining Forward and Backward Search 4.3 Abstraction Refinement for Pushdown System Reachability 5 Implementation and Experiments 6 Conclusion References Verifying Verified Code 1 Introduction 2 Unit Proofs with Code-as-Specification 3 Case Study 3.1 RQ1: Does CaS Empower Multiple Tools? 3.2 Are There Bugs in Verified Code? 3.3 Can Specifications Be Improved While Maintaining the CaS Philosophy? 4 Related Work 5 Conclusion References Probabilistic Analysis Probabilistic Causes in Markov Chains 1 Introduction 2 Preliminaries 3 Causes 3.1 Types of p-causes and Induced Monitors 3.2 Comparison to Prima Facie Causes 4 Costs of p-causes 4.1 Expected Cost of a p-cause 4.2 Partial Expected Cost of a p-cause 4.3 Maximal Cost of a p-cause 4.4 Instantaneous Cost 5 Conclusion References TEMPEST - Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments 1 Introduction 2 Model and Property Specification 3 Tempest Synthesis of Strategies 4 Tempest in Action 5 Conclusion and Future Work References AQUA: Automated Quantized Inference for Probabilistic Programs 1 Introduction 2 Preliminaries 3 AQUA's Probabilistic Inference Using Density Cubes 3.1 Notations and Basic Definitions 3.2 Analysis 3.3 Formal Guarantee of Accuracy 4 AQUA Analysis Optimizations 5 Methodology 6 Evaluation 6.1 Runtime and Accuracy Comparison 6.2 Estimating the Tails of Posterior Distribution 7 Related Work 8 Conclusion References Software and Hardware Verification Proving SIFA Protection of Masked Redundant Circuits 1 Introduction 1.1 Related Work 1.2 Contribution 2 Preliminaries 3 Verification Method 3.1 Attack Model 3.2 Incompleteness 3.3 Hiding 3.4 Inferred Statistical Independence 3.5 Approximating Statistical Independence 3.6 Verification Algorithm 4 Case Studies 4.1 Masked Keccak 3 4.2 Masked AES S-Box 4.3 Performance Evaluation 5 Conclusion References Verification by Gambling on Program Slices 1 Introduction 2 Background 3 Qicc 3.1 Cyclic Region Identification 3.2 Gambling 4 Evaluation 4.1 Implementation 4.2 Experimental Design 4.3 RQ1: Bounded Model Checking Systematic Analysis 4.4 RQ2: Evaluation with Automata Verifier 4.5 RQ3: Case Study 4.6 Threats to Validity 5 Related Work 6 Conclusion References Runtime Enforcement of Hyperproperties 1 Introduction 2 Preliminaries 3 Hyperproperty Enforcement 3.1 Trace Input Models 3.2 Losing Prefixes for Hyperproperties 3.3 Enforcement Mechanisms 4 Enforcement Algorithms for HyperLTL Specifications 4.1 Parallel Trace Input Model 4.2 Sequential Trace Input Model 5 Experimental Evaluation 5.1 Enforcing Symmetry in Mutual Exclusion Algorithms 5.2 Enforcing Observational Determinism 6 Conclusion References System Synthesis and Approximation Compositional Synthesis of Modular Systems 1 Introduction 2 Running Example 3 Preliminaries 4 Compositional Synthesis with Certificates 5 Certifying Synthesis with Deterministic Certificates 6 Computing Relevant Processes 7 Synthesizing Certificates 8 Experimental Results 9 Conclusions References Event-B Refinement for Continuous Behaviours Approximation 1 Introduction 2 Event-B 3 Hybrid Systems in Event-B 3.1 Continuous Variables 3.2 Continuous Refinement 3.3 Embedding Continuous Features Using Theories 4 A Theory of Approximation 4.1 Foundational Constructs 4.2 Properties of Approximation 4.3 Encoding Approximation in Event-B Using Theories 5 Approximation and Refinement: Two Scenarios of Use 5.1 Approximate Gluing Invariant 5.2 Downward Approximation Scenario 5.3 Upward Approximation Scenario 6 Related Work and Assessment 7 Conclusion References Incorporating Monitors in Reactive Synthesis Without Paying the Price 1 Introduction 2 Preliminaries 2.1 Flagging Monitors 3 Monitors as Triggers for LTL Formulas 4 Synthesising Monitor-Triggered Controllers 4.1 Tight Synthesis for Co-safety Implication Formulas 4.2 Monitor-Triggered Synthesis 5 Tool Support 6 Case Studies 6.1 Event Counting 6.2 Sequences of Events 7 Discussion 8 Conclusions References Verification of Machine Learning pyNeVer: A Framework for Learning and Verification of Neural Networks 1 Summary 2 Abstraction Algorithms 3 Experimental Evaluation References Property-Directed Verification and Robustness Certification of Recurrent Neural Networks 1 Introduction 2 Preliminaries 3 Verification Approaches 4 Property-Directed Verification of RNNs 5 Adversarial Robustness Certification 6 Experimental Evaluation 6.1 Evaluation on Randomly Generated DFAs 6.2 Adversarial Robustness Certification 6.3 RNNs Identifying Contact Sequences 7 Conclusion References Author Index