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, Part I.

• Superior document: Lecture Notes in Computer Science Series ; v.12651
• Author: Groote, Jan Friso.
• TeilnehmendeR: Larsen, Kim Guldstrand.
• Place / Publishing House: Cham : : Springer International Publishing AG,, 2021.; ©2021.
• Year of Publication: 2021
• Edition: 1st ed.
• Language: English
• Series: Lecture Notes in Computer Science Series
• Physical Description: 1 online resource (483 pages)

Table of Contents

Intro -- 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.