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

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