Tools and Algorithms for the Construction and Analysis of Systems. 27th International Conference, TACAS 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021 Luxembourg City, Luxembourg, March 27 – April 1, 2021 Proceedings

ETAPS Foreword
Preface
Organization
Contents – Part I
Contents – Part II
Game Theory
	A Game for Linear-time–Branching-time Spectroscopy
		1 Introduction
		2 Preliminaries: HML, Games, and the Spectrum
			2.1 Transition Systems and Hennessy–Milner Logic
			2.2 Games Semantics of HML
			2.3 The Spectrum of Behavioral Equivalences
		3 Distinguishing Formula Games
			3.1 The Formula Preorder Game
			3.2 The Spectroscopy Game
			3.3 Building Distinguishing Formulas from Attacker Strategies
			3.4 Retrieving Cheapest Distinguishing Formulas
		4 A Webtool for Equivalence Spectroscopy
		5 Related Work and Alternatives
		6 Conclusion
		References
	On Satisficing in Quantitative Games
		1 Introduction
		2 Preliminaries
			2.1 Two-player graph games
			2.2 Automata and formal languages
		3 Satisficing via Optimization
			3.1 Satisficing and Optimization
			3.2 VI: Number of iterations
			3.3 Worst-case complexity analysis of VI for optimization
			3.4 Satisficing via value-iteration
		4 Satisficing via Comparators
			4.1 Foundations of comparator automata with threshold v ∈ Q
			4.2 Satisficing via safety and reachability games
			4.3 Implementation and Empirical Evaluation
		5 Adding Temporally Extended Goals
		6 Concluding remarks
		References
	Quasipolynomial Computation of Nested Fixpoints
		1 Introduction
		2 Notation and Preliminaries
		3 Systems of Fixpoint Equations
		4 Fixpoint Games and History-free Witnesses
		5 Solving Equation Systems using Universal Graphs
		6 A Progress Measure Algorithm
		7 Conclusion
		References
SMT Verification
	A Flexible Proof Format for SAT Solver-Elaborator Communication
		1 Introduction
		2 The FRAT format
			2.1 Flexibility and extensibility
		3 FRAT-producing solvers
		4 Elaboration
		5 Test results
		6 Related works
		7 Conclusion
		References
	Generating Extended Resolution Proofs with a BDD-Based SAT Solver
		1 Introduction
		2 Preliminaries
			2.1 (Extended) Resolution Proofs
			2.2 Binary Decision Diagrams
		3 Proof Generation During BDD Construction
			3.1 Generating BDD Representations of Clauses
			3.2 The APPLYAND Operation
			3.3 Testing Implication
		4 Experimental Results
			4.1 Mutilated Chessboard
			4.2 Pigeonhole Problem
			4.3 Evaluation
		5 Conclusion
		References
	Bounded Model Checking for Hyperproperties
		1 Introduction
		2 Preliminaries
			2.1 Kripke Structures
			2.2 The Temporal Logic HyperLTL
		3 Bounded Semantics for HyperLTL
			3.1 Bounded Semantics
			3.2 The Logical Relation between Different Semantics
		4 Reducing BMC to QBF Solving
		5 Evaluation and Case Studies
		6 Related Work
		7 Conclusion and Future Work
		References
	Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
		1 Introduction
		2 Background
		3 Using Auxiliary Variables to Assist Induction
		4 Abstraction Refinement for Arrays
		5 Expressiveness and Limitations
		6 Experiments
		7 Related Work
		8 Conclusion
		References
	SAT Solving with GPU Accelerated Inprocessing
		1 Introduction
		2 Preliminaries
		3 GPU Memory and Data Structures
		4 Parallel Garbage Collection
		5 Parallel Inprocessing Procedure
		6 Three-Phase Parallel Variable Elimination
		7 Eager Redundancy Elimination
		8 Experiments
		9 Related Work
		10 Conclusion
		References
	FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions
		1 Introduction
		2 Synthesis Algorithm Overview
		3 Regular Expressions Synthesis
			3.1 Regular Expressions DSL
			3.2 Regex Enumeration
			3.3 Regex Disambiguation
		4 Capturing Groups Synthesis
			4.1 Capturing Groups Enumeration
			4.2 Capture Conditions Synthesis
			4.3 Capture Conditions Disambiguation
		5 Related Work
		6 Experimental Results
			6.1 Comparison with Regel
			6.2 Impact of pruning the search space and splitting examples
			6.3 Multi-tree versus k-tree and line-based encodings
			6.4 Impact of fewer examples
		7 Conclusions and Future Work
		References
Probabilities
	Finding Provably Optimal Markov Chains
		1 Introduction
		2 Problem Statement
		3 Main Ingredients in a Nutshell
			3.1 The Monotonicity Checker
			3.2 The Parameter Lifter
			3.3 Divide and Conquer
		4 A New Rule for Sufficient Monotonicity
		5 Parameter Lifting with Monotonicity Information
		6 Lifting and Monotonocity, Together
		7 Empirical Evaluation
		8 Conclusion and Future Work
		References
	Inductive Synthesis for Probabilistic Programs Reaches New Horizons-0.5em
		1 Introduction
		2 Problem Statement
		3 Counterexample-Guided Inductive Synthesis
		4 A Smart Oracle with Counterexamples and Abstraction
		5 Hybrid Dual-Oracle Synthesis
		6 Experimental evaluation
		7 Conclusion
		References
	Analysis of Markov Jump Processes under Terminal Constraints
		1 Introduction
		2 Related Work
		3 Preliminaries
			3.1 Markov Jump Processes with Population Structure
			3.2 Bridging Distribution
		4 Bridge Truncation via Lumping Approximations
			4.1 Finite State Projection
			4.2 State-Space Lumping
			4.3 Iterative Refinement Algorithm
		5 Results
			5.1 Bounding Rare Event Probabilities
			5.2 Mode Switching
			5.3 Recursive Bayesian Estimation
		6 Conclusion
		References
	Multi-objective Optimization of Long-run Average and Total Rewards
		1 Introduction
		2 Preliminaries
			2.1 Markov Automata
			2.2 Reward-based Objectives
			2.3 Markov Decision Processes
		3 Efficient Multi-objective Model Checking
			3.1 Multi-objective Model Checking Queries
			3.2 Approximation of Achievable Points
		4 Optimizing Weighted Combinations of Objectives
			4.1 Pure Long-run Average Queries
			4.2 A Two-phase Approach for Single-objective LRA
			4.3 Combining Long-run Average and Total Rewards
		5 Experimental Evaluation
		6 Conclusion
		References
	Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes
		1 Introduction
		2 Probabilistic Integer Programs
		3 Complexity Bounds
			3.1 Runtime and Size Bounds
			3.2 Expected Runtime and Size Bounds
		4 Computing Expected Runtime Bounds
			4.1 Probabilistic Linear Ranking Functions
			4.2 Inferring Expected Runtime Bounds
		5 Computing Expected Size Bounds
			5.1 Local Change Bounds and General Result Variable Graph
			5.2 Inferring Expected Size Bounds
		6 Related Work, Implementation, and Conclusion
		References
	Probabilistic and Systematic Coverage of Consecutive Test-Method Pairs forDetecting Order-Dependent Flaky Tests
		1 Introduction
		2 Background and Example
		3 Preliminaries
			3.1 Dataset for Evaluation
		4 Analysis of Flake Rate and Simple Algorithm Change
			4.1 Determining Test Outcome without Running a Test Order
			4.2 Computing Flake Rate
			4.3 Comparing Flake Rate for Different Sets of Test Orders
			4.4 Simple Change to Increase Probability of Detecting OD Tests
		5 Generating Test Orders to Cover Test Pairs
			5.1 Special Case: All Orders are Class-Compatible
			5.2 General Case
		6 Conclusion
		Acknowledgments
		References
Timed Systems
	Timed Automata Relaxation for Reachability
		1 Introduction
		2 Preliminaries and Problem Formulation
			2.1 Timed Automata
			2.2 Timed Automata Relaxations and Reductions
			2.3 Problem Statement
		3 Minimal Sufficient (D,I)-Reductions
			3.1 Base Scheme For Computing a Minimum MSR
			3.2 Shrinking a Seed
			3.3 Finding a Seed
			3.4 Representation of I and C
		4 Synthesis of Relaxation Parameters
		5 Case Study
		References
	Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata
		1 Introduction
		2 PTA, Parametric Zone Graphs and Accepted Runs
		3 Sound and Complete Liveness Parameter Synthesis
			3.1 Soundness and Completeness
		4 Semi-Algorithms for Liveness Parameter Synthesis
			4.1 Nested Depth-First Search with Enhancements
			4.2 Breadth-First Search
			4.3 Bounded Synthesis with Iterative Deepening
		5 Experimental Evaluation
		6 Case Study: the Bounded Retransmission Protocol
			6.1 Synthesis for Reachability Properties: deriving sharper bounds
			6.2 Liveness: approximations by bounded synthesis
			6.3 Proper Liveness Properties
		7 Conclusion
		References
	Algebraic Quantitative Semantics for Efficient Online Temporal Monitoring
		1 Introduction
		2 Algebraic Semantics using Semirings
		3 Symbolic Quantitative Traces and Languages
		4 Relationship with robust semantics
		5 Online Monitoring
		6 Experimental Evaluation
		7 Related Work
		8 Conclusion
		References
Neural Networks
	Synthesizing Context-free Grammars from Recurrent Neural Networks
		1 Introduction
		2 Definitions and Notations
			2.1 Deterministic Finite Automata
			2.2 Dyck Languages
		3 Patterns
			3.1 Pattern Composition
		4 Pattern Rule Sets
			4.1 Examples
		5 PRS Inference Algorithm
			5.1 Deviations from the PRS framework
		6 Converting a PRS to a CFG
		7 Experimental results
			7.1 Methodology
			7.2 Generating a sequence of DFAs
			7.3 Languages
			7.4 Results
		8 Related work
		9 Future Directions
		References
	Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models
		1 Introduction
		2 Safety Analysis with Barrier Certificates
		3 Synthesis of Neural Barrier Certificates via Learning and Verification
			3.1 Training of the Barrier Neural Network
			3.2 Certification of the Barrier Neural Network, or Falsification via Counter-examples
		4 Case Studies and Experimental Results
		5 Conclusions and Future Work
		References
	Improving Neural Network Verification through Spurious Region Guided Refinement
		1 Introduction
		2 Preliminaries
			2.1 Robustness verification of deep neural networks
			2.2 Abstract interpretation for DNN verification
		3 A Brief Introduction to DeepPoly
		4 Spurious Region Guided Refinement
			4.1 Main algorithm
			4.2 Iterative refinement of the spurious region
			4.3 Optimizations
		5 Quantitative Robustness Verification
		6 Experimental Evaluation
			6.1 Improvement in precision
			6.2 Robustness verification performance
			6.3 Quantitative robustness verification on ACAS Xu networks
		7 Related Works and Conclusion
		Acknowledgement
		References
Analysis of Network Communication
	Resilient Capacity-Aware Routing
		1 Introduction
		2 Network with Capacities and Demands
		3 Analysis of Algorithmic Complexity
		4 A Fast Strategic Search Algorithm
		5 Experiments
		6 Conclusion
		References
	Network Traffic Classification by Program Synthesis
		1 Introduction
		2 Overview
		3 Background on NetQRE
		4 Synthesis Algorithm
			4.1 Overview
			4.2 Partial Execution
			4.3 Merge Search
		5 Evaluation
			5.1 Data Preparation
			5.2 Learning Accuracy
			5.3 Post-processing and Interpretation
			5.4 Deployment Scenarios
			5.5 Program Synthesis Performance
		6 Related Work
		7 Conclusion
		Acknowledgements
		References
	General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
		1 Introduction
		2 Preliminaries
		3 Decision Problems on Asynchronous Programs
		4 General Decidability Results
			4.1 Safety and termination
			4.2 Boundedness
			4.3 Configuration reachability and liveness properties
		5 Higher-Order Asynchronous Programs
		References
Author Index