Cover Image

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.

Bibliographic Details
Main Author: Groote, Jan Friso.
Other Authors: Larsen, Kim Guldstrand.
Format: eBook
Language:English
Published: Cham : Springer International Publishing AG, 2021.
Edition:1st ed.
Series:Lecture Notes in Computer Science Series
Subjects:
Electronic books.
Online Access:Click to View
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.

Similar Items