Cover Image

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

Bibliographic Details
Main Author: Fisman, Dana.
Other Authors: Rosu, Grigore.
Format: eBook
Language:English
Published: Cham : Springer International Publishing AG, 2022.
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 II
  • Contents - Part I
  • Probabilistic Systems
  • A Probabilistic Logic for Verifying Continuous-time Markov Chains
  • 1 Introduction
  • 2 Preliminaries
  • 3 Continuous-time Markov Chains as Distributions Transformers
  • 4 Symbolic Dynamics of CTMCs
  • 5 Continuous Linear-time Logic
  • 6 CLL Model Checking
  • 7 Numerical Implementation
  • 8 Related Works
  • 9 Conclusion
  • Acknowledgments
  • References
  • Under-Approximating Expected Total Rewards in POMDPs
  • 1 Introduction
  • 2 Preliminaries and Problem Statement
  • 3 Finite Exploration Under-Approximation
  • 4 Experimental Evaluation
  • 5 Conclusion
  • References
  • Correct Probabilistic Model Checkingwith Floating-Point Arithmetic
  • 1 Introduction
  • 2 Probabilistic Model Checking
  • 3 Floating-Point Arithmetic
  • 4 Correctly Rounding Interval Iteration
  • 5 Experiments
  • 6 Conclusion
  • References
  • Correlated Equilibria and Fairness in Concurrent Stochastic Games
  • 1 Introduction
  • 2 Normal Form Games
  • 3 Concurrent Stochastic Games
  • 4 Case Studies and Experimental Results
  • 5 Conclusions
  • References
  • Omega Automata
  • A Direct Symbolic Algorithm for Solving Stochastic Rabin Games
  • 1 Introduction
  • 2 Preliminaries
  • 3 Problem Statement and Outline
  • 4 From Randomness to Extreme Fairness
  • 5 Extremely Fair Adversarial Rabin Games
  • 5.1 Preliminaries on Symbolic Computations over Game Graphs
  • 5.2 The Symbolic Algorithm
  • 5.3 Proof Outline
  • 6 Experimental Evaluation
  • 6.1 The VLTS Benchmark Experiments
  • 6.2 Synthesis for Stochastically Perturbed Dynamical Systems
  • References
  • Practical Applications of theAlternating Cycle Decomposition
  • 1 Introduction
  • 2 Preliminaries
  • 3 The Alternating Cycle Decomposition
  • 4 An Efficient Computation of the ACD.
  • 5 From Emerson-Lei to Parity Automata
  • 6 Degeneralization of Generalized Büchi Automata
  • 7 Deciding Typeness
  • 8 Availability
  • 9 Conclusion
  • References
  • Sky Is Not the Limit
  • 1 Introduction
  • 2 Preliminaries
  • 3 Complementing Büchi automata
  • 4 Elevator Automata
  • 5 Rank Propagation
  • 6 Experimental Evaluation
  • 7 Related Work
  • References
  • On-The-Fly Solving for Symbolic Parity Games
  • 1 Introduction
  • 2 Preliminaries
  • 3 Incomplete Parity Games
  • 4 On-the-fly Solving
  • 5 Experimental Results
  • 6 Conclusion
  • References
  • Equivalence Checking
  • Distributed Coalgebraic Partition Refinement
  • 1 Introduction
  • 2 Preliminaries
  • 3 Coalgebraic Partition Refinement
  • 4 The Distributed Algorithm
  • 5 Evaluation
  • 6 Conclusions and Future Work
  • References
  • From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques
  • 1 Introduction
  • 2 High-Level Intuitions
  • 3 Language and Semantics
  • 4 LTS with Symbolic Higher-Order Transitions
  • 5 Up-to Techniques
  • 6 Symbolic First-Order Transitions
  • 7 Up to State Invariants
  • 8 Implementation and Evaluation
  • 9 Comparison with Existing Tools
  • 10 Conclusion
  • References
  • Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time
  • 1 Introduction
  • 2 Preliminaries
  • 2.1 Lattices and Bisemilattices
  • 2.2 Term Rewriting Systems
  • 3 Directed Acyclic Graph Equivalence
  • 4 Word Problem on Orthocomplemented Bisemilattices
  • 4.1 Confluence of the Rewriting System
  • 4.2 Complete Terminating Confluent Rewrite System
  • 5 Algorithm and Complexity
  • 5.1 Combining Rewrite Rules and Tree Isomorphism
  • 5.2 Case of Quadratic Runtime for the Basic Algorithm
  • 5.3 Final Log-Linear Time Algorithm
  • 6 Conclusion
  • References
  • Monitoring and Analysis
  • A Theoretical Analysis of Random Regression Test Prioritization.
  • 1 Introduction
  • 2 Preliminaries
  • 3 PMF of α
  • 4 Expected Values for All Orders Ωa(T )
  • 5 Expected Values for Compatible Orders Ωc(T )
  • 6 Properties of Metrics and Checking Prior RTP Work
  • 7 Related Work
  • 8 Conclusion
  • References
  • Verified First-Order Monitoring with Recursive Rules
  • 1 Introduction
  • 2 Metric First-Order Temporal Logic
  • 3 Non-Recursive Let Operator
  • 4 Past-Recursive Let Operator
  • 5 Evaluation
  • 6 Conclusion
  • References
  • Maximizing Branch Coverage withConstrained Horn Clauses
  • 1 Introduction
  • 2 Related Work
  • 3 Motivating Example
  • 4 Background
  • 5 Test-case Generation for Branch Coverage
  • 6 Solving the MBC problem
  • 7 Evaluation
  • 8 Conclusion
  • References
  • Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation
  • 1 Introduction
  • 2 Preliminaries
  • 3 Cyclic Redundancy Architectures
  • 4 Reducing Redundancy UF+V TS to Fault Propagation Graphs
  • 5 Related Work
  • 6 Experimental Evaluation
  • 7 Conclusions and Future Work
  • References
  • Tools | Optimizations, Repair and Explainability
  • Adiar
  • 1 Introduction
  • 2 Preliminaries
  • 3 BDD Manipulation by Time-forward Processing
  • 4 Adiar: An Implementation
  • 5 Experimental Evalua
  • 6 Conclusions and Future Work
  • References
  • Forest GUMP: A Tool for Explanation
  • 1 Introduction
  • 2 Random Forests
  • 3 Class Vector Aggregation
  • 4 Infeasible Path Elimination
  • 5 Majority Vote at Compile Time
  • 6 Forest GUMP and Three Problems of Explanability
  • 7 Lessons Learned
  • 8 Conclusion and Perspectives
  • References
  • Alpinist: an Annotation-Aware GPU Program Optimizer
  • 1 Introduction
  • 2 Annotation-Aware Optimization using Alpinist
  • 3 The Design of Alpinist
  • 4 GPU Optimizations
  • 5 Evaluation
  • 6 Related Work
  • 7 Conclusion
  • References
  • Automatic Repair for Network Programs
  • 1 Introduction.
  • 2 Overview
  • 3 Preliminaries
  • 4 Modular Program Repair
  • 5 Implementation
  • 6 Evaluation
  • 7 Related Work
  • 8 Limitations and Future Work
  • 9 Conclusion
  • References
  • 11th Competition on Software Verification|SV-COMP 2022
  • Progress on Software Verification: SV-COMP 2022
  • 1 Introduction
  • 2 Organization, Definitions, Formats, and Rules
  • 3 Reproducing a Verification Run and Trouble-Shooting Guide
  • 4 Participating Verifiers
  • 5 Results and Discussion
  • 6 Conclusion
  • References
  • AProVE: Non-Termination Witnesses for C Programs
  • 1 Verification Approach and Software Architecture
  • 2 Discussion of Strengths and Weaknesses
  • 3 Setup and Configuration
  • References
  • BRICK: Path Enumeration Based Bounded Reachability Checking of C Program(Competition Contribution)
  • 1 Verification Approach
  • 2 Software Architecture
  • 3 Strengths and Weaknesses
  • 4 Tool Setup and Configuration
  • 5 Software Project and Contributors
  • References
  • A Prototype for Data Race Detection in CSeq 3 (Competition Contribution)
  • 1 Verification Approach
  • 2 Software Architecture
  • 3 Strengths and Weaknesses
  • 4 Setup and Configuration
  • References
  • Dartagnan: SMT-based Violation Witness Validation (Competition Contribution)
  • 1 Introduction
  • 2 Validation Approach
  • 3 Strengths and Weaknesses
  • 4 Validation Results
  • 5 Software Project and Configuration
  • References
  • Deagle: An SMT-based Verifier for Multi-threaded Programs (Competition Contribution)
  • 1 Verification Approach
  • 2 Software Architecture
  • 3 Strengths and Weaknesses
  • 4 Tool Setup and Configuration
  • 5 Software Project
  • 6 Acknowledgement
  • References
  • The Static Analyzer Frama-C in SV-COMP (Competition Contribution)
  • 1 Approach
  • 2 Architecture
  • 3 Strengths and Weaknesses
  • 4 Software Project and Contributors
  • References.
  • GDart: An Ensemble of Tools for Dynamic Symbolic Execution on the Java Virtual Machine (Competition Contribution)
  • 1 Verification Approach
  • 2 Software Architecture
  • 3 Strengths and Weaknesses
  • 4 Tool Setup
  • 5 Software Project
  • 6 Data Availability Statement
  • References
  • Graves-CPA: A Graph-Attention Verifier Selector (Competition Contribution)
  • 1 Verification Approach
  • 2 System Architecture
  • 3 Strengths and Weaknesses
  • 4 Tool Setup and Configuration
  • 5 Software Project and Contributions
  • Acknowledgements
  • References
  • GWIT: A Witness Validator for Java based on GraalVM (Competition Contribution)
  • 1 Introduction
  • 2 Witness Validation in GWIT
  • 3 Performance and Limitations
  • 4 Tool Setup
  • 5 Software Project
  • 6 Data Availability Statement
  • References
  • The Static Analyzer Infer in SV-COMP(Competition Contribution)
  • 1 Facebook Infer
  • 2 Infer in SV-COMP
  • 3 Usage
  • 4 Conclusion
  • References
  • LART: Compiled Abstract Execution
  • 1 Verification Approach and Software Architecture
  • 2 Strengths and Weaknesses
  • 3 Tool Setup and Configuration
  • 4 Software Project and Contributors
  • References
  • Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding
  • 1 Verification Approach
  • 2 Strengths and Weaknesses
  • 3 Software Project and Contributors
  • References
  • Symbiotic-Witch: A Klee-Based Violation Witness Checker
  • 1 Verification Approach
  • 2 Software Architecture
  • 3 Strengths and Weaknesses
  • 4 Tool Setup and Configuration
  • 5 Software Project and Contributors
  • References
  • Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution)
  • 1 Verification Approach and Software Architecture
  • 2 Strengths and Weaknesses
  • 3 Tool Setup and Configuration
  • 4 Software Project
  • References.
  • Ultimate GemCutter and the Axes of Generalization (Competition Contribution).

Similar Items