Tools and Algorithms for the Construction and Analysis of Systems : (Record no. 2569)
[ view plain ]
| 000 -Satzkennung | |
|---|---|
| Kontrollfeld mit fester Länge | 11423nam a22004813i 4500 |
| 001 - Kontrollnummer | |
| Kontrollfeld | EBC6523259 |
| 003 - Kontrollnummer Identifier | |
| Kontrollfeld | MiAaPQ |
| 005 - Datum und Zeit der letzten Transaktion | |
| Kontrollfeld | 20220324112739.0 |
| 006 - Datenelemente mit fester Länge - Weitere Materialmerkmale | |
| Kontrollfeld mit fester Länge | m o d | |
| 007 - Feld mit fester Länge zur physischen Beschreibung - Allgemeine Information | |
| Kontrollfeld mit fester Länge | cr cnu|||||||| |
| 008 - Feld mit fester Länge zur physischen Beschreibung - Allgemeine Angaben | |
| Kontrollfeld mit fester Länge | 220324s2021 xx o ||||0 eng d |
| 020 ## - Internationale Standardbuchnummer | |
| Internationale Standardbuchnummer | 9783030720162 |
| Nähere Angaben | (electronic bk.) |
| 020 ## - Internationale Standardbuchnummer | |
| Gelöschte/ungültige ISBN | 9783030720155 |
| 035 ## - Systemkontrollnummer | |
| System-Kontrollnummer | (MiAaPQ)EBC6523259 |
| 035 ## - Systemkontrollnummer | |
| System-Kontrollnummer | (Au-PeEL)EBL6523259 |
| 035 ## - Systemkontrollnummer | |
| System-Kontrollnummer | (OCoLC)1244539366 |
| 040 ## - Katalogisierungsquelle | |
| Original-Katalogisierungsstelle | MiAaPQ |
| Katalogisierungssprache | eng |
| Beschreibungsfestlegungen | rda |
| -- | pn |
| Übertragungsstelle | MiAaPQ |
| Bearbeitungsstelle | MiAaPQ |
| 050 #4 - Signatur der Library of Congress | |
| Notation | QA75.5-76.95 |
| 100 1# - Haupteintragung - Personenname | |
| Personenname | Groote, Jan Friso. |
| 245 10 - Titel | |
| Titel | Tools and Algorithms for the Construction and Analysis of Systems : |
| Zusatz zum Titel | 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. |
| 264 #1 - Produktion, Veröffentlichung, Distribution, Herstellung und Urheberrechtsvermerk | |
| Herstellungs-, Veröffentlichungs- Vertriebs-, Erzeugungsort | Cham : |
| Produzent, Herausgeber, Distributor, Hersteller | Springer International Publishing AG, |
| Datum der Herstellung, der Veröffentlichung, des Vertriebs oder des Urheberschutzvermerks | 2021. |
| 264 #4 - Produktion, Veröffentlichung, Distribution, Herstellung und Urheberrechtsvermerk | |
| Datum der Herstellung, der Veröffentlichung, des Vertriebs oder des Urheberschutzvermerks | �2021. |
| 300 ## - Physische Beschreibung | |
| Umfang | 1 online resource (483 pages) |
| 336 ## - Inhaltstyp | |
| Inhaltstypterm | text |
| Inhaltstypcode | txt |
| Quelle | rdacontent |
| 337 ## - Medientyp | |
| Bezeichnung des Medientyps | computer |
| Medientypcode | c |
| Quelle | rdamedia |
| 338 ## - Datenträgertyp | |
| Datenträgertypbezeichnung | online resource |
| Datenträgertypcode | cr |
| Quelle | rdacarrier |
| 490 1# - Gesamttitelangabe | |
| Gesamttitelangabe | Lecture Notes in Computer Science Ser. ; |
| Bandnummer/Folgebezeichnung | v.12651 |
| 505 0# - Fußnote zu strukturierten Inhaltsangaben | |
| Fußnote zu strukturierten Inhaltsangaben | 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# - Fußnote zu strukturierten Inhaltsangaben | |
| Fußnote zu strukturierten Inhaltsangaben | 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# - Fußnote zu strukturierten Inhaltsangaben | |
| Fußnote zu strukturierten Inhaltsangaben | 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# - Fußnote zu strukturierten Inhaltsangaben | |
| Fußnote zu strukturierten Inhaltsangaben | 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# - Fußnote zu strukturierten Inhaltsangaben | |
| Fußnote zu strukturierten Inhaltsangaben | 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# - Fußnote zu strukturierten Inhaltsangaben | |
| Fußnote zu strukturierten Inhaltsangaben | 3.1 Training of the Barrier Neural Network. |
| 588 ## - Anmerkung zur Ausgabe, zum Teil oder zur Iteration, die/der als Grunlage für die Identifizierung der Ressource verwendet wird | |
| Anmerkung zur Ausgabe, zum Teil oder zur Iteration, die/der als Grunlage für die Identifizierung der Ressource verwendet wird | Description based on publisher supplied metadata and other sources. |
| 590 ## - Lokale Fußnote (RLIN) | |
| Local note | Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2022. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries. |
| 655 #4 - Indexierungsterm - Genre/Form | |
| Genre/Form oder fokussierter Term | Electronic books. |
| 700 1# - Nebeneintragung - Personenname | |
| Personenname | Larsen, Kim Guldstrand. |
| 776 08 - Andere physische Form | |
| Verweisungsphrase | Print version: |
| Haupteintragung | Groote, Jan Friso |
| Titel | Tools and Algorithms for the Construction and Analysis of Systems |
| Ort, Verlag und Erscheinungsjahr | Cham : Springer International Publishing AG,c2021 |
| Internationale Standardbuchnummer | 9783030720155 |
| 797 2# - LOCAL ADDED ENTRY--CORPORATE NAME (RLIN) | |
| Körperschafts- oder Gebietskörperschaftsname als Eintragungselement | ProQuest (Firm) |
| 830 #0 - Nebeneintragung unter dem Gesamttitel - Einheitstitel | |
| Einheitstitel | Lecture Notes in Computer Science Ser. |
| 856 40 - Elektronische Adresse und Zugriff | |
| URL | <a href="https://www.nbs.de/bibliothek/faq">https://www.nbs.de/bibliothek/faq</a> |
| OPAC-Notiz | Wie greife ich auf das E-Book zu? |
| 856 40 - Elektronische Adresse und Zugriff | |
| URL | <a href="https://ebookcentral.proquest.com/lib/nbsde/detail.action?docID=6523259">https://ebookcentral.proquest.com/lib/nbsde/detail.action?docID=6523259</a> |
| OPAC-Notiz | Click to View |
No items available.