|
|
|
|
| LEADER |
11337nam a22004693i 4500 |
| 001 |
EBC6523259 |
| 003 |
MiAaPQ |
| 005 |
20231204023215.0 |
| 006 |
m o d | |
| 007 |
cr cnu|||||||| |
| 008 |
231204s2021 xx o ||||0 eng d |
| 020 |
|
|
|a 9783030720162
|q (electronic bk.)
|
| 020 |
|
|
|z 9783030720155
|
| 035 |
|
|
|a (MiAaPQ)EBC6523259
|
| 035 |
|
|
|a (Au-PeEL)EBL6523259
|
| 035 |
|
|
|a (OCoLC)1244539366
|
| 040 |
|
|
|a MiAaPQ
|b eng
|e rda
|e pn
|c MiAaPQ
|d MiAaPQ
|
| 050 |
|
4 |
|a QA75.5-76.95
|
| 100 |
1 |
|
|a Groote, Jan Friso.
|
| 245 |
1 |
0 |
|a Tools and Algorithms for the Construction and Analysis of Systems :
|b 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.
|
| 250 |
|
|
|a 1st ed.
|
| 264 |
|
1 |
|a Cham :
|b Springer International Publishing AG,
|c 2021.
|
| 264 |
|
4 |
|c ©2021.
|
| 300 |
|
|
|a 1 online resource (483 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.12651
|
| 505 |
0 |
|
|a 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.
|
| 505 |
8 |
|
|a 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.
|
| 505 |
8 |
|
|a 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.
|
| 505 |
8 |
|
|a 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.
|
| 505 |
8 |
|
|a 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.
|
| 505 |
8 |
|
|a 3.1 Training of the Barrier Neural Network.
|
| 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 Larsen, Kim Guldstrand.
|
| 776 |
0 |
8 |
|i Print version:
|a Groote, Jan Friso
|t Tools and Algorithms for the Construction and Analysis of Systems
|d Cham : Springer International Publishing AG,c2021
|z 9783030720155
|
| 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=6523259
|z Click to View
|
