Automated Technology for Verification and Analysis: 21st International Symposium, ATVA 2023, Singapore, October 24–27, 2023, Proceedings 1

This book constitutes the refereed proceedings of the 21st International Symposium on Automated Technology for Verification and Analysis, ATVA 2023, held in Singapore, in October 2023. The symposium intends to promote research in theoretical and practical aspects of automated analysis, verification and synthesis by providing a forum for interaction between regional and international research communities and industry in related areas. The 30 regular papers presented together with 7 tool papers were carefully reviewed and selected from 150 submissions.The papers are divided into the following topical sub-headings: Temporal logics, Data structures and heuristics, Verification of programs and hardware. Preface Organization Contents – Part I Contents – Part II Invited Talk Correct and Efficient Policy Monitoring, a Retrospective • David Basin, Srd-an Krstic ́, Joshua Schneider, and Dmitriy Traytel 1 Introduction 2 The Logic 3 Monitoring Setting 4 Restrictions and Algorithms 4.1 Relational Algebra Normal Form 4.2 Translation to RANF 4.3 Automatic Structures 4.4 Propositional Monitoring 5 Parallelization 5.1 Scalable Offline Monitoring 5.2 Scalable Online Monitoring 5.3 Monitoring Distributed Systems 6 Verification 7 Applications 7.1 Security and Anomaly Detection 7.2 Privacy and Data Protection 7.3 Distributed Systems 8 Conclusions and Open Problems References Automata Learning Nonlinear Hybrid Automata from Input–Output Time-Series Data • Amit Gurung, Masaki Waga, and Kohei Suenaga 1 Introduction 2 Preliminaries 2.1 Trajectories and Hybrid Automata 2.2 Linear Multistep Method 2.3 Dynamic Time Warping (DTW) 3 HA Learning from Input–Output Trajectories 3.1 Identification of Locations 3.2 Identification of Transitions 3.3 Impact of Parameter Selection on Model Accuracy 4 Experiments 4.1 Benchmark Description 4.2 Results and Discussion 4.3 Comparison with Other Methods 5 Conclusion References A Novel Family of Finite Automata for Recognizing and Learning ω-Regular Languages • Yong Li, Sven Schewe, and Qiyi Tang 1 Introduction 2 Preliminaries 3 Limit FDFAs for Recognizing -Regular Languages 3.1 Limit FDFAs and Other Canonical FDFAs 3.2 Size Comparison with Other Canonical FDFAs 4 Limit FDFAs for Identifying DBA-Recognizable Languages 4.1 Limit FDFA for DBA-Recognizable Languages 4.2 Deciding DBA-Recognizable Languages 5 Underspecifying Progress Right Congruences 6 Discussion and Future Work References On the Containment Problem for Deterministic Multicounter Machine Models • Oscar H. Ibarra and Ian McQuillan 1 Introduction 2 Preliminaries 3 Properties of Deterministic Partially-Blind Machines 4 Finite-Testable Counter Machines 5 Bounded Languages in DTCM and NTCM 6 Complement and Containment of Deterministic Finite-Testable Machines 7 Future Directions References Parallel and Incremental Verification of Hybrid Automata with Ray and Verse • Haoqing Zhu, Yangge Li, Keyi Shen, and Sayan Mitra 1 Introduction 2 Related Work 3 Preliminaries: Hybrid Multi-agent Scenarios 3.1 Agents in Hybrid Scenarios 3.2 Scenario to Hybrid Verification 3.3 Bounded Reach Sets 4 Parallel and Incremental Verification Algorithms 4.1 Reachability Analysis 4.2 Parallel Reachability with Ray 4.3 Incremental Verification 5 Experimental Evaluation 5.1 Parallel Reachability Speeds up with Cores and Branching 5.2 Incremental Verification Can Speed up Reachability Across Model Updates 6 Conclusions and Future Directions References An Automata Theoretic Characterization of Weighted First-Order Logic • Dhruv Nevatia and Benjamin Monmege 1 Introduction 2 Weighted First-Order Logic 3 Nested Two-Way Weighted Automata 4 From the Logic to Automata 5 From Nested Sweeping Weighted Automata to the Logic 6 From Nested Two-Way Weighted Automata to Nested Sweeping Weighted Automata 7 Conclusion References Probabilistic Systems Graph-Based Reductions for Parametric and Weighted MDPs • Kasper Engelen, Guillermo A. Pérez, and Shrisha Rao 1 Introduction 2 Preliminaries 2.1 Stochastic Models 2.2 The Graph of a WpMDP 2.3 The Never-Worse Relation 3 From Weighted to Non-Weighted MDPs 3.1 Removing Weights from Parametric MDPs 3.2 Removing Weights from Trivially Parametric MDPs 4 The Complexity of Deciding the NWR 4.1 The Complexity of Deciding NWR Equivalences 5 Action Pruning via the NWR 5.1 The Under-Approximation Graph 5.2 End Components and Quotienting 5.3 Pruning Actions and Inferring the NWR 6 Experiments 6.1 Benchmarks and Protocol 6.2 Different Setups 6.3 Results, Tables and Graphs 7 Conclusions References Scenario Approach for Parametric Markov Models • Ying Liu, Andrea Turrini, Ernst Moritz Hahn, Bai Xue, and Lijun Zhang 1 Introduction 2 Preliminaries 2.1 Probabilistic Models 2.2 Probabilistic Reward Logic PRCTL 2.3 Parametric Models 3 Probably Approximately Correct Function Synthesis 3.1 Probably Approximately Correct Models 3.2 The Scenario Approach 3.3 Synthesizing Parametric Functions 3.4 PRCTL Property Analysis 4 Experimental Evaluation 4.1 Overall Evaluation 4.2 Relation of the Polynomial Degree d and the Number of Samples with the Margin and the Distance [2]f - 4.3 Relation of the Statistical Parameters and with the Distances [2]f - and UB(, X, ) 4.4 Comparison with the Taylor Expansion 4.5 Extension to Reward Models 5 Conclusion References Fast Verified SCCs for Probabilistic Model Checking 1 Introduction 2 Preliminaries 2.1 Markov Decision Processes 2.2 Program Verification Based on Refinement in Isabelle/HOL 2.3 Existing Formalisation of Gabow's Algorithm 3 Abstract Path-Based Algorithm 3.1 The Skeleton Algorithm 3.2 Abstract SCC-Finding Algorithm 4 Formalizing Gabow's Algorithm 4.1 The Skeleton of Gabow's Algorithm 4.2 Gabow's SCC-Finding Algorithm 5 Refinement to LLVM 5.1 Node State 5.2 MDP Graph Data Structure 5.3 Main Algorithm 6 Implementation in the Modest Toolset 7 Benchmarks 7.1 Benchmark Selection 7.2 Benchmarking Setup 7.3 Benchmarking Results 8 Conclusion References Bi-objective Lexicographic Optimization in Markov Decision Processes with Related Objectives Damien Busatto-Gaston, Debraj Chakraborty, Anirban Majumdar, Sayan Mukherjee, Guillermo A. Pérez, and Jean-François Raskin 1 Introduction 2 Preliminaries 2.1 Markov Chain 2.2 Markov Decision Process 3 Length-Optimal Strategy for Reachability 3.1 Maximizing Probability to Reach a Target 3.2 Minimizing Expected Conditional Length to Target 4 Experimental Results 5 Safety and Expected Mean Payoff 5.1 Maximizing Probability of Staying Safe 5.2 Maximizing Expected Conditional Mean Payoff 6 Discussion References Synthesis Model Checking Strategies from Synthesis over Finite Traces • Suguman Bansal, Yong Li, Lucas M. Tabajara, Moshe Y. Vardi, and Andrew Wells 1 Introduction 2 Preliminaries and Notations 2.1 Linear Temporal Logic over Finite Traces (LTLf) 2.2 LTLf Synthesis and Transducers 3 LTLf Model Checking 4 Prefix Language of LTLf Formulas 4.1 Prefix Automata for LTLf 4.2 Prefix Automata for LTLf Fragment 5 Complexity of LTLf Model Checking 5.1 EXPSPACE Lower Bound for Non-terminating Systems 5.2 Final Complexity Results 6 Concluding Remarks References Reactive Synthesis of Smart Contract Control Flows • Bernd Finkbeiner, Jana Hofmann, Florian Kohn, and Noemi Passing 1 Introduction 2 Preliminaries 2.1 State Machines, Safety Properties and Reactive Synthesis 2.2 Past-Time Temporal Stream Logic 3 Parameterized TSL for Smart Contract Specifications 3.1 Parameterized TSL 3.2 Example: ERC20 Contract 4 Synthesis Approach 4.1 Problem Statement 4.2 High-Level Description of the Approach 5 PastTSL Synthesis 5.1 PastTSL Synthesis via PastLTL Approximation 6 Splitting Algorithm 6.1 Idea of the Algorithm 6.2 Construction 6.3 Check for Independence 6.4 Interpretation as Infinite-State Machine 6.5 Correctness 6.6 Extension to Existential Quantifiers 7 Implementation and Evaluation 7.1 Implementation 7.2 Evaluation 8 Conclusion References Synthesis of Distributed Protocols by Enumeration Modulo Isomorphisms • Derek Egolf and Stavros Tripakis 1 Introduction 2 Preliminaries 3 The Guess-Check-Generalize Paradigm 3.1 A Generic GCG Algorithm and Its Correctness 3.2 A Concrete Instance of GCG for LTS 4 Synthesis Modulo Isomorphisms 4.1 LTS Isomorphisms 4.2 Completion Enumeration Modulo Isomorphisms 4.3 Properties of an Efficient GCG Algorithm 4.4 Optimized Generalization 5 Implementation and Evaluation 6 Related Work 7 Conclusions References Controller Synthesis for Reactive Systems with Communication Delay by Formula Translation • J. S. Sajiv Kumar and Raghavan Komondoor 1 Introduction 2 Background 3 Fixed Delay 3.1 Definitions 3.2 Results on Control Under Delay 3.3 Controller Synthesis 3.4 Soundness and Completeness 4 Variable Delay 4.1 Definitions 4.2 Results on Control Under Variable Delay 4.3 Controller Synthesis 4.4 Properties of Our Approach 5 Unrealizability Filter 6 Empirical Evaluation 6.1 Our Results 6.2 Comparison with Chen et al.'s Tool 7 Related Work 8 Conclusions and Future Work References Statistical Approach to Efficient and Deterministic Schedule Synthesis for Cyber-Physical Systems • Shengjie Xu, Bineet Ghosh, Clara Hobbs, Enrico Fraccaroli, Parasara Sridhar Duggirala, and Samarjit Chakraborty 1 Introduction 1.1 Related Work 2 Background 2.1 System Formulation 2.2 System Behavior Under Deadline Misses 2.3 Characterizing Deadline Miss Patterns 3 Statistical Hypothesis Testing 3.1 Example of Statistical Hypothesis Testing 4 Proposed Schedule Synthesis 4.1 Comparison with Deterministic Method Proposed in ch15xuspssafetyspsawaresps2023 5 Evaluation 5.1 Benchmarks 5.2 Experiments 5.3 RQ1: Effectiveness of the Proposed Approach to Synthesize Safe Schedules 5.4 RQ2: Reduction of Execution Time Using the Proposed Approach 6 Concluding Remarks References Compositional High-Quality Synthesis • Rafael Dewes and Rayna Dimitrova 1 Introduction 2 Preliminaries 2.1 Languages and Automata over Infinite Words 2.2 The Temporal Logic LTL[F] 3 Good-Enough Assume-Guarantee Decomposition 3.1 Multi-component Reactive Systems 3.2 Good-Enough Realizability and Synthesis from LTL[F] 3.3 Good-Enough Decomposition 4 Compositional Good-Enough Synthesis 4.1 Automata Constructions 4.2 Synthesis with a Given Assume-Guarantee Contract 4.3 Synthesis with Iterative Assumption Generation 5 Experimental Evaluation 6 Conclusion References Neural Networks Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems • Matin Ansaripour, Krishnendu Chatterjee, Thomas A. Henzinger, Mathias Lechner, and Đorđe Žikelić 1 Introduction 2 Preliminaries 3 Theoretical Results 4 Learning Stabilizing Policies and sRSMs on Compact State Spaces 4.1 Initialization 4.2 Learner 4.3 Verifier 4.4 Adaptation into a Formal Verification Procedure 5 Experimental Results 6 Related Work 7 Conclusion References An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks • Ye Tao, Wanwei Liu, Fu Song, Zhen Liang, Ji Wang, and Hongxu Zhu 1 Introduction 2 Preliminaries 3 The Temporal Logic BLTL 3.1 Syntax and Semantics of BLTL 3.2 Illustrating Properties Expressed by BLTL 4 From BLTL to Automata 4.1 Eliminating Placeholders 4.2 Automata Construction 4.3 Tableau-Based Construction 5 BNN Synthesis 5.1 The Threshold 5.2 Encoding with IDL Problem 5.3 Utilize the Synthesis 6 Experimental Evaluation 6.1 Local Robustness 6.2 Individual Fairness 7 Conclusion References Syntactic vs Semantic Linear Abstraction and Refinement of Neural Networks 1 Introduction 2 Preliminaries 2.1 Syntactic and Semantic Abstractions 3 Linear Abstraction 3.1 Finding the Basis 3.2 Finding the Coefficients 3.3 Replacement 4 Refinement 5 Experimental Results 5.1 Abstraction 5.2 Comparison to Existing Work 5.3 Semantic vs Syntactic 5.4 Refining the Network 5.5 Error Calculation 6 Conclusions References Using Counterexamples to Improve Robustness Verification in Neural Networks • Mohammad Afzal, Ashutosh Gupta, and S. Akshay 1 Introduction 2 A Motivating Example 3 Preliminaries 3.1 DeepPoly 3.2 Solver 4 Algorithm 4.1 The Top Level Algorithm 4.2 Verifying Query Under Marked Neurons 4.3 Maxsat Based Approach to Find the Marked Neurons 4.4 Proofs of Progress and Termination 5 Experiments 5.1 Results 6 Conclusion References Author Index