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.