.

0 (hodnocen0 x )

EB

ONLINE

Cham : Springer International Publishing AG, 2022

1 online resource (506 pages)

ISBN 9783030995270 (electronic bk.)

ISBN 9783030995263

Lecture Notes in Computer Science Ser. ; v.13244

Print version: Fisman, Dana Tools and Algorithms for the Construction and Analysis of Systems Cham : Springer International Publishing AG,c2022 ISBN 9783030995263

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.

1 Introduction -- 2 Preliminaries -- 3 PMF of a -- 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.

5 From Emerson-Lei to Parity Automata -- 6 Degeneralization of Generalized Buchi Automata -- 7 Deciding Typeness -- 8 Availability -- 9 Conclusion -- References -- Sky Is Not the Limit -- 1 Introduction -- 2 Preliminaries -- 3 Complementing Buchi 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.

Ultimate GemCutter and the Axes of Generalization (Competition Contribution).

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.

001896864

express

(Au-PeEL)EBL6942731

(MiAaPQ)EBC6942731

(OCoLC)1308973926