Tools and Algorithms for the Construction and Analysis of Systems. 28th International Conference, TACAS 2022 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022 Munich, Germany, April 2–7, 2022 Proceedings

Description

ETAPS Foreword Preface Organization Contents – Part I Contents – Part II Synthesis HOLL: Program Synthesis for Higher Order Logic Locking 1 Introduction 2 HOLL Overview 2.1 Threat Model: the Untrusted Foundry 2.2 Defending with HOLL 2.3 Attacking with SynthAttack 3 Program Synthesis to Infer Key Relations 3.1 Lock and Key Inference 3.2 Expression Selection 4 HOLL: Implementation and Optimization 5 SynthAttack: Attacking HOLL with Program Synthesis 5.1 The SynthAttack Algorithm 6 Experimental Evaluation 6.1 Attack Resilience 6.2 Impact of Expression Selection on Attack Resilience 6.3 Hardware cost 7 Related Work 8 Discussion References The Complexity of LTL Rational Synthesis 1 Introduction 2 Preliminaries 2.1 LTL, trees, and automata 2.2 Concurrent multiplayer games 3 Rational Synthesis 4 The Complexity of Cooperative Rational Synthesis 5 The Complexity of Non-Cooperative Rational Synthesis 5.1 Turn-based games 5.2 Concurrent games 5.3 General rational synthesis References Synthesis of Compact Strategies for Coordination Programs 1 Introduction 2 Background 3 Compactness 3.1 Effective Minimality Constructions for LTL 3.2 Relationship to Quantitative Synthesis 3.3 Approximating Compactness 4 Evaluation 4.1 Multi-Robot Coordination 4.2 Compactness for LTL 5 Related Work References ZDD Boolean Synthesis 1 Introduction 2 Preliminaries 3 Realizability Using ZDDs 3.1 Realizable Set R 3.2 Full and Partial Realizability 4 Synthesis Using ZDDs 4.1 Witnesses for Single-Dimension Output Variable 4.2 Preserve CNF by Equivalent Witnesses 4.3 Algorithm for Constructing Witnesses 5 Experimental Evaluations 5.1 Experimental Methodology and and Setting 5.2 Compilation Time and Size of Diagram Representing Original Formula 5.3 Realizability Time 5.4 End-to-End Time and Peak Memory 5.5 Scalable Benchmarks Show ZDD has Slower Growing Demands of Time and Space 5.6 Overall Comparison 6 Conclusion References Verification Comparative Verification of the Digital Library of Mathematical Functions and Computer Algebra Systems 1 Introduction 1.1 Related Work 2 The DLMF dataset 3 Semantic LATEX to CAS translation 3.1 Parse sums, products, integrals, and limits 3.2 Lagrange’s notation for differentiation and derivatives 4 Evaluation of the DLMF using CAS 4.1 Symbolic Evaluation 4.2 Numerical Evaluation 5 Results 5.1 Error Analysis 6 Conclusion 6.1 Future Work References Verifying Fortran Programs with CIVL 1 Introduction 2 Overview of CIVL Extension 3 Defect-Preserving Translation 3.1 Translation from Source to Source 3.2 Translation for Compilation 3.3 Translation for Verification 4 Fortran Array Modeling 4.1 Fortran Array Semantics 4.2 Modeling Fortran Arrays for Verification 5 Evaluation 5.1 Compute Environment and Experimental Artifacts 5.2 Specification and Verification Approach 5.3 Fortran Verification Benchmark Suites 5.4 Verifying Nek5000 Components 6 Related Work 7 Conclusion and Future Work References NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems 1 Introduction 2 Relay-based Railway Interlocking Systems 3 Norma: overview 4 Graphical modeling of RRIS 5 Compilation in Timed SMV 6 Simplification of RRIS models 6.1 Equivalence propagation 6.2 Abstracting electrical variables 7 Software architecture 8 Experimental Evaluation 9 Conclusions References Efficient Neural Network Analysis with Sum-of-Infeasibilities 1 Introduction 2 Related Work 3 Preliminaries 4 Sum of Infeasibilities in Neural Network Analysis 4.1 The Sum of Infeasibilities 4.2 Stochastically Minimizing the SoI with MCMC Sampling 5 The DeepSoI Algorithm 5.1 DeepSoI 5.2 Complete Analysis and Pseudo-impact Branching 6 Experimental Evaluation 6.1 Implementation. 6.2 Benchmarks. 6.3 Experimental Setup. 6.4 Ablation study of the proposed techniques. 6.5 Comparison with other complete analyzers. 6.6 Incremental Solving and the Rejection Threshold T 6.7 Improving the perturbation bounds found by AutoAttack 7 Conclusions and Future Work References Blockchain Formal Verification of the Ethereum 2.0 Beacon Chain 1 Introduction 2 The Beacon Chain Reference Implementation 2.1 System Description and Scope of the Study 2.2 The Beacon Chain Reference Implementation 2.3 Motivation for Formal Verification 2.4 Objectives of the Study 3 Formal Specification and Verification 3.1 Challenges 3.2 Methodologies 3.3 Results 4 Findings and Lessons Learned 4.1 Array-out-of-bounds Runtime Error 4.2 Beyond Runtime Errors 4.3 Finalisation and Justification 4.4 Reection 5 Conclusion References Fast and Reliable Formal Verification of Smart Contracts with the Move Prover 1 Introduction 2 Move and the Prover 3 Move Prover Design 3.1 Reference Elimination 3.2 Global Invariant Injection 3.3 Monomorphization 4 Analysis 5 Conclusion References A Max-SMT Superoptimizer for EVM handling Memory and Storage 1 Introduction and Related Work 2 The Architecture of GASOL 3 Synthesis of Stack and Memory Specifications 3.1 Initial Stack and Memory/Storage Specification 3.2 Memory/Storage Simplifications 3.4 Bounding the Operations Position 4 Max-SMT Superoptimization 4.1 Stack Representation in the SMT Encoding 4.2 Encoding the Pre-order Relation 4.3 Optimization using Max-SMT 5 Implementation and Experiments 6 Conclusions and Future Work References Grammatical Inference A New Approach for Active Automata Learning Based on Apartness 1 Introduction 2 Partial Mealy Machines and Apartness 3 Learning Algorithm 3.1 Hypothesis construction 3.2 Main loop of the algorithm 3.3 Consistency checking 3.4 Counterexample processing 3.5 Adaptive distinguishing sequences 3.6 Complexity 4 Experimental Evaluation 5 Conclusions and Future Work References Learning Realtime One-Counter Automata 1 Introduction 2 Preliminaries 3 Learning ROCAs 4 Experiments 4.1 Random ROCAs 4.2 JSON Documents and JSON Schemas 5 Future Work References Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic 1 Introduction 2 Preliminaries 3 High-level view of the algorithm 4 Searching for directed formulas 5 Boolean combinations of formulas 6 Theoretical guarantees 7 Experimental evaluation 7.1 RQ1: Performance Comparison 7.2 RQ2: Scalability 7.3 RQ3: Anytime Property 8 Conclusion References Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes 1 Introduction 1.1 Related Work 2 Background 2.1 Signal Temporal Logic 2.2 Kernel Crash Course 3 Overview of Our Approach and Results 4 A Kernel for Signal Temporal Logic 4.1 Definition of STL Kernel 4.2 The Base Measure 0 4.3 Normalized Robustness 4.4 PAC Bounds for the STL Kernel 5 Experiments 5.1 Setting 5.2 Robustness and Satisfaction on Single Trajectories 5.3 Expected Robustness and Satisfaction Probability 5.4 Kernel Regression on Other Stochastic Processes 6 Conclusions References Verification Inference Inferring Interval-Valued Floating-Point Preconditions 1 Introduction 2 Overview 3 Precondition Inference by Subdivision 3.1 Extracting a Verified Precondition from Subdivisions 3.2 Precondition Optimization 4 Precondition Inference by Decision Tree Learning 4.1 Extracting Candidates from a Classification Tree 4.2 Refining Candidates by Growing Regions 4.3 Refining Candidates by Recursive Subdivision 5 Evaluation 6 Related Work 7 Conclusion References NeuReach: Learning Reachability Functions from Simulations 1 Introduction 2 Related work 3 Problem setup and an overview of the tool 4 Design of NeuReach: Learning reachability functions 4.1 Reachability with Empirical Risk Minimization 4.2 Probabilistic Correctness of NeuReach 5 Experimental evaluation 5.1 Benchmark systems 5.2 Experimental results 6 Conclusion References Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion 1 Introduction 2 Background 3 Breadth-First Inductive Generalization with Separation 3.1 Naive Inductive Generalization with Separation 3.2 Prefix Search at the Inductive Generalization Level 3.3 Algorithm for Inductive Generalization 4 k-Term Pseudo-DNF 5 An Algorithm for Invariant Inference 5.1 May-proof-obligations 5.2 Multi-block Generalization 5.3 Enforcing EPR 5.4 SMT Robustness 5.5 Complete Algorithm 6 Evaluation 6.1 Invariant Inference Benchmark 6.2 Experimental Setup 6.3 Results and Discussion 6.4 Ablation Study 7 Related Work 8 Conclusion References LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions 1 Introduction 2 Preliminaries 2.1 Neural Networks 2.2 Neural Network Verification 2.3 Existing Methods 2.4 Limitations of Existing Methods 3 Synthesizing the Candidate Linear Bounds 3.1 Problem Statement and Challenges 3.2 Synthesizing Candidate Bounds 4 Making the Bound Sound 4.1 Problem Statement and Challenges 4.2 Verifying the Bound 4.3 Computing υl 4.4 On the Correctness and Generality of LinSyn 5 Evaluation 5.1 Benchmarks 5.2 Experimental Results 6 Related Work 7 Conclusions References Short papers Kmclib: Automated Inference and Verification of Session Types from OCaml Programs 1 Introduction 2 Safe Concurrent Programming in Multicore OCaml 3 Inference of Session Types in kmclib 4 Conclusion References Automated Translation of Natural Language Requirements to Runtime Monitors 1 Introduction 2 Step-by-step Framework Workflow 3 FRET Steps 4 Ogma Steps 5 Copilot Steps 6 Preliminary Results 7 Conclusion References MaskD: A Tool for Measuring Masking Fault-Tolerance 1 Introduction 2 The MaskD Tool 2.1 Architecture 2.2 Usage 3 Experiments References Better Counterexamples for Dafny 1 Introduction 2 Motivation 3 Design and Implementation 4 Conclusions and Future Work References Constraint Solving cvc5: A Versatile and Industrial-Strength SMT Solver 1 Introduction 2 Architecture and Core Components 2.1 The SMT Solver Module 2.2 Proof Module 2.3 Node Manager 2.4 Context-Dependent Data Structures 3 Highlighted Features 4 Evaluation 5 Future Work References Clausal Proofs for Pseudo-Boolean Reasoning 1 Introduction 2 Pseudo-Boolean Constraints 2.1 BDD Representations 2.2 Solving Systems of Equations with Gaussian Elimination 2.3 Solving Systems of Ordering Constraints with Fourier-Motzkin Elimination 3 Overall Operation 3.1 Constraint Extraction 3.2 Solver Operation 4 Experimental Results 4.1 Urquhart Parity Formulas 4.2 Other Parity Constraint Benchmarks 4.3 Variants of the Mutilated Chessboard 4.4 Pigeonhole Problem 4.5 Other Cardinality Constraint Problems 5 Conclusions References Moving Definition Variables in Quantified Boolean Formulas 1 Introduction 2 Preliminaries 2.1 Quantified Boolean Formulas 2.2 Inference Techniques in QBF 2.3 Definitions 3 Definition Detection 3.1 Hierarchical Definition Detection in CNFTOOLS 3.2 Independent Definition Detection in KISSAT 4 Moving Variables 4.1 Moving in Order 4.2 XOR Processing 4.3 Proving Variable Movement 5 Evaluation 5.1 Evaluating Definition Detection 5.2 Evaluating Solvers 6 PGBDDQ Case Study 7 Conclusion and Future Work 8 Acknowledgements References A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic 1 Introduction 2 Preliminaries 3 The Sorted Datalog Hammer 4 Implementation and Experiments 5 Conclusion References Model Checking and Verification Property Directed Reachability for Generalized Petri Nets 1 Introduction 2 Petri Nets and Linear Reachability Constraints 3 Property Directed Reachability 4 Experimental Results 5 Conclusion and Related Works References Transition Power Abstractions for Deep Counterexample Detection 1 Introduction 2 Background 3 Motivating example 4 Finding deep counterexamples with transition power abstractions 4.1 TPA sequence for bounded reachability queries 4.2 Algorithm for bounded reachability checks 4.3 Correctness and termination 4.4 Under-approximating QE with model-based projection 4.5 Proving safety 5 Experiments 6 Related work 7 Conclusion and Future Work References Searching for Ribbon-Shaped Paths in Fair Transition Systems 1 Introduction 2 Related Work 3 Background 3.1 Symbolic Fair Transition Systems 3.2 Liveness to Safety (L2S). 4 The Problem of Ribbon-Shaped Paths 4.1 The Diagnosability Problem 4.2 Ribbon-Shaped Critical Pairs 4.3 Fixpoint-based Algorithm 5 Extended Liveness to Safety 5.1 Definition of the L2S Extension 5.2 Correctness 6 Experimental Evaluation 6.1 Implementation 6.2 Benchmarks 6.3 Results 7 Conclusions and Future Work References CoVeriTeam: On-Demand Composition of Cooperative Verification Systems 1 Introduction 2 Running Example 3 Design and Implementation of CoVeriTeam 3.1 Concepts 3.2 Execution Concerns 3.3 CoVeriTeam 3.4 API 4 Evaluation 4.1 Case Studies 4.2 Performance 5 Related Work 6 Conclusion References Author Index