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
LEADER 11316nam a22004693i 4500
001 EBC6942731
003 MiAaPQ
005 20231204023222.0
006 m o d |
007 cr cnu||||||||
008 231204s2022 xx o ||||0 eng d
020 |a 9783030995270  |q (electronic bk.) 
020 |z 9783030995263 
035 |a (MiAaPQ)EBC6942731 
035 |a (Au-PeEL)EBL6942731 
035 |a (OCoLC)1308973926 
040 |a MiAaPQ  |b eng  |e rda  |e pn  |c MiAaPQ  |d MiAaPQ 
050 4 |a QA75.5-76.95 
100 1 |a Fisman, Dana. 
245 1 0 |a Tools and Algorithms for the Construction and Analysis of Systems :  |b 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. 
250 |a 1st ed. 
264 1 |a Cham :  |b Springer International Publishing AG,  |c 2022. 
264 4 |c ©2022. 
300 |a 1 online resource (506 pages) 
336 |a text  |b txt  |2 rdacontent 
337 |a computer  |b c  |2 rdamedia 
338 |a online resource  |b cr  |2 rdacarrier 
490 1 |a Lecture Notes in Computer Science Series ;  |v v.13244 
505 0 |a 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. 
505 8 |a 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. 
505 8 |a 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. 
505 8 |a 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. 
505 8 |a 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. 
505 8 |a Ultimate GemCutter and the Axes of Generalization (Competition Contribution). 
588 |a Description based on publisher supplied metadata and other sources. 
590 |a Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2023. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries.  
655 4 |a Electronic books. 
700 1 |a Rosu, Grigore. 
776 0 8 |i Print version:  |a Fisman, Dana  |t Tools and Algorithms for the Construction and Analysis of Systems  |d Cham : Springer International Publishing AG,c2022  |z 9783030995263 
797 2 |a ProQuest (Firm) 
830 0 |a Lecture Notes in Computer Science Series 
856 4 0 |u https://ebookcentral.proquest.com/lib/matrademy/detail.action?docID=6942731  |z Click to View 

Similar Items