Kooperativer Bibliotheksverbund

UID:

Format: 1 Online-Ressource

ISBN: 9783030720162

Series Statement: Lecture notes in computer science 12651

Additional Edition: Erscheint auch als Druck-Ausgabe ISBN 978-3-030-72015-5

Language: English

Keywords: Konferenzschrift

DOI: 10.1007/978-3-030-72016-2

URL: Volltext  (kostenfrei)

URL: Volltext  (kostenfrei)

UID:

Format: 1 online resource (483 pages)

ISBN: 9783030720162

Series Statement: Lecture Notes in Computer Science Ser. ; v.12651

Note: 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. , 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. , 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. , 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. , 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. , 3.1 Training of the Barrier Neural Network.

Additional Edition: Print version: Groote, Jan Friso Tools and Algorithms for the Construction and Analysis of Systems Cham : Springer International Publishing AG,c2021 ISBN 9783030720155

Language: English

Keywords: Electronic books. ; Electronic books

URL: Click to View

URL: Full-text  ((OIS Credentials Required))

URL: lizenzpflichtig

UID:

Format: 1 online resource (483 pages)

Edition: 1st ed. 2021.

ISBN: 3-030-72016-0

Series Statement: Theoretical Computer Science and General Issues, 12651

Content: This open access two-volume set constitutes the proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021, which was held during March 27 – April 1, 2021, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021. The conference was planned to take place in Luxembourg and changed to an online format due to the COVID-19 pandemic. The total of 41 full papers presented in the proceedings was carefully reviewed and selected from 141 submissions. The volume also contains 7 tool papers; 6 Tool Demo papers, 9 SV-Comp Competition Papers. The papers are organized in topical sections as follows: Part I: Game Theory; SMT Verification; Probabilities; Timed Systems; Neural Networks; Analysis of Network Communication. Part II: Verification Techniques (not SMT); Case Studies; Proof Generation/Validation; Tool Papers; Tool Demo Papers; SV-Comp Tool Competition Papers.

Note: Game Theory -- A Game for Linear-time - Branching-time Spectroscopy -- On Satisficing in Quantitative Games -- Quasipolynomial Computation of Nested Fixpoints -- SMT Verification -- A Flexible Proof Format for SAT Solver-Elaborator Communication -- Generating Extended Resolution Proofs with a BDD-Based SAT Solver -- Bounded Model Checking for Hyperproperties -- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays -- SAT Solving with GPU Accelerated Inprocessing -- FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions -- Probabilities -- Finding Provably Optimal Markov Chains -- Inductive Synthesis for Probabilistic Programs Reaches New Horizons -- Analysis of Markov Jump Processes under Terminal Constraints -- Multi-objective Optimization of Long-run Average and Total Rewards -- Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes -- Probabilistic and Systematic Coverage of Consecutive Test-Method Pairs for Detecting Order-Dependent Flaky Tests -- Timed Systems -- Timed Automata Relaxation for Reachability -- Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata -- Algebraic Quantitative Semantics for Efficient Online Temporal Monitoring -- Neural Networks -- Synthesizing Context-free Grammars from Recurrent Neural Networks -- Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models -- Improving Neural Network Verification through Spurious Region Guided Refinement -- Analysis of Network Communication Resilient Capacity-Aware Routing -- Network Traffic Classification by Program Synthesis. . , English

Additional Edition: ISBN 3-030-72015-2

Language: English

DOI: 10.1007/978-3-030-72016-2

UID:

Format: 1 Online-Ressource(XXI, 471 p. 106 illus.)

Edition: 1st ed. 2021.

ISBN: 9783030720162

Series Statement: Theoretical Computer Science and General Issues 12651

Content: Game Theory -- A Game for Linear-time - Branching-time Spectroscopy -- On Satisficing in Quantitative Games -- Quasipolynomial Computation of Nested Fixpoints -- SMT Verification -- A Flexible Proof Format for SAT Solver-Elaborator Communication -- Generating Extended Resolution Proofs with a BDD-Based SAT Solver -- Bounded Model Checking for Hyperproperties -- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays -- SAT Solving with GPU Accelerated Inprocessing -- FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions -- Probabilities -- Finding Provably Optimal Markov Chains -- Inductive Synthesis for Probabilistic Programs Reaches New Horizons -- Analysis of Markov Jump Processes under Terminal Constraints -- Multi-objective Optimization of Long-run Average and Total Rewards -- Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes -- Probabilistic and Systematic Coverage of Consecutive Test-Method Pairs for Detecting Order-Dependent Flaky Tests -- Timed Systems -- Timed Automata Relaxation for Reachability -- Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata -- Algebraic Quantitative Semantics for Efficient Online Temporal Monitoring -- Neural Networks -- Synthesizing Context-free Grammars from Recurrent Neural Networks -- Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models -- Improving Neural Network Verification through Spurious Region Guided Refinement -- Analysis of Network Communication Resilient Capacity-Aware Routing -- Network Traffic Classification by Program Synthesis. .

Content: This open access two-volume set constitutes the proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021, which was held during March 27 – April 1, 2021, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021. The conference was planned to take place in Luxembourg and changed to an online format due to the COVID-19 pandemic. The total of 41 full papers presented in the proceedings was carefully reviewed and selected from 141 submissions. The volume also contains 7 tool papers; 6 Tool Demo papers, 9 SV-Comp Competition Papers. The papers are organized in topical sections as follows: Part I: Game Theory; SMT Verification; Probabilities; Timed Systems; Neural Networks; Analysis of Network Communication. Part II: Verification Techniques (not SMT); Case Studies; Proof Generation/Validation; Tool Papers; Tool Demo Papers; SV-Comp Tool Competition Papers.

Note: Open Access

Additional Edition: ISBN 9783030720155

Additional Edition: ISBN 9783030720179

Additional Edition: Erscheint auch als Druck-Ausgabe ISBN 9783030720155

Additional Edition: Erscheint auch als Druck-Ausgabe ISBN 9783030720179

Language: English

DOI: 10.1007/978-3-030-72016-2

URL: kostenfrei

UID:

Format: XXI, 471 p. 106 illus. , online resource.

Edition: 1st ed. 2021.

ISBN: 9783030720162

Series Statement: Theoretical Computer Science and General Issues ; 12651

Content: This open access two-volume set constitutes the proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021, which was held during March 27 - April 1, 2021, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021. The conference was planned to take place in Luxembourg and changed to an online format due to the COVID-19 pandemic. The total of 41 full papers presented in the proceedings was carefully reviewed and selected from 141 submissions. The volume also contains 7 tool papers; 6 Tool Demo papers, 9 SV-Comp Competition Papers. The papers are organized in topical sections as follows: Part I: Game Theory; SMT Verification; Probabilities; Timed Systems; Neural Networks; Analysis of Network Communication. Part II: Verification Techniques (not SMT); Case Studies; Proof Generation/Validation; Tool Papers; Tool Demo Papers; SV-Comp Tool Competition Papers.

Note: Game Theory -- A Game for Linear-time - Branching-time Spectroscopy -- On Satisficing in Quantitative Games -- Quasipolynomial Computation of Nested Fixpoints -- SMT Verification -- A Flexible Proof Format for SAT Solver-Elaborator Communication -- Generating Extended Resolution Proofs with a BDD-Based SAT Solver -- Bounded Model Checking for Hyperproperties -- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays -- SAT Solving with GPU Accelerated Inprocessing -- FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions -- Probabilities -- Finding Provably Optimal Markov Chains -- Inductive Synthesis for Probabilistic Programs Reaches New Horizons -- Analysis of Markov Jump Processes under Terminal Constraints -- Multi-objective Optimization of Long-run Average and Total Rewards -- Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes -- Probabilistic and Systematic Coverage of Consecutive Test-Method Pairs for Detecting Order-Dependent Flaky Tests -- Timed Systems -- Timed Automata Relaxation for Reachability -- Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata -- Algebraic Quantitative Semantics for Efficient Online Temporal Monitoring -- Neural Networks -- Synthesizing Context-free Grammars from Recurrent Neural Networks -- Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models -- Improving Neural Network Verification through Spurious Region Guided Refinement -- Analysis of Network Communication Resilient Capacity-Aware Routing -- Network Traffic Classification by Program Synthesis. .

In: Springer Nature eBook

Additional Edition: Printed edition: ISBN 9783030720155

Additional Edition: Printed edition: ISBN 9783030720179

Language: English

DOI: 10.1007/978-3-030-72016-2

URL: https://doi.org/10.1007/978-3-030-72016-2

URL: https://doi.org/10.1007/978-3-030-72016-2

UID:

Format: xxi, 471 Seiten , Illustrationen, Diagramme

ISBN: 9783030720155

Series Statement: Lecture notes in computer science 12651

In: 1

Additional Edition: Erscheint auch als Online-Ausgabe ISBN 978-3-030-72016-2

Language: English

Keywords: Konferenzschrift

UID:

Format: 1 online resource (483 pages)

Edition: 1st ed. 2021.

ISBN: 3-030-72016-0

Series Statement: Theoretical Computer Science and General Issues, 12651

Content: This open access two-volume set constitutes the proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021, which was held during March 27 – April 1, 2021, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021. The conference was planned to take place in Luxembourg and changed to an online format due to the COVID-19 pandemic. The total of 41 full papers presented in the proceedings was carefully reviewed and selected from 141 submissions. The volume also contains 7 tool papers; 6 Tool Demo papers, 9 SV-Comp Competition Papers. The papers are organized in topical sections as follows: Part I: Game Theory; SMT Verification; Probabilities; Timed Systems; Neural Networks; Analysis of Network Communication. Part II: Verification Techniques (not SMT); Case Studies; Proof Generation/Validation; Tool Papers; Tool Demo Papers; SV-Comp Tool Competition Papers.

Note: Game Theory -- A Game for Linear-time - Branching-time Spectroscopy -- On Satisficing in Quantitative Games -- Quasipolynomial Computation of Nested Fixpoints -- SMT Verification -- A Flexible Proof Format for SAT Solver-Elaborator Communication -- Generating Extended Resolution Proofs with a BDD-Based SAT Solver -- Bounded Model Checking for Hyperproperties -- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays -- SAT Solving with GPU Accelerated Inprocessing -- FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions -- Probabilities -- Finding Provably Optimal Markov Chains -- Inductive Synthesis for Probabilistic Programs Reaches New Horizons -- Analysis of Markov Jump Processes under Terminal Constraints -- Multi-objective Optimization of Long-run Average and Total Rewards -- Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes -- Probabilistic and Systematic Coverage of Consecutive Test-Method Pairs for Detecting Order-Dependent Flaky Tests -- Timed Systems -- Timed Automata Relaxation for Reachability -- Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata -- Algebraic Quantitative Semantics for Efficient Online Temporal Monitoring -- Neural Networks -- Synthesizing Context-free Grammars from Recurrent Neural Networks -- Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models -- Improving Neural Network Verification through Spurious Region Guided Refinement -- Analysis of Network Communication Resilient Capacity-Aware Routing -- Network Traffic Classification by Program Synthesis. . , English

Additional Edition: ISBN 3-030-72015-2

Language: English

DOI: 10.1007/978-3-030-72016-2

UID:

Format: 1 online resource (483 pages)

Edition: 1st ed. 2021.

ISBN: 3-030-72016-0

Series Statement: Theoretical Computer Science and General Issues, 12651

Content: This open access two-volume set constitutes the proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021, which was held during March 27 – April 1, 2021, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021. The conference was planned to take place in Luxembourg and changed to an online format due to the COVID-19 pandemic. The total of 41 full papers presented in the proceedings was carefully reviewed and selected from 141 submissions. The volume also contains 7 tool papers; 6 Tool Demo papers, 9 SV-Comp Competition Papers. The papers are organized in topical sections as follows: Part I: Game Theory; SMT Verification; Probabilities; Timed Systems; Neural Networks; Analysis of Network Communication. Part II: Verification Techniques (not SMT); Case Studies; Proof Generation/Validation; Tool Papers; Tool Demo Papers; SV-Comp Tool Competition Papers.

Note: Game Theory -- A Game for Linear-time - Branching-time Spectroscopy -- On Satisficing in Quantitative Games -- Quasipolynomial Computation of Nested Fixpoints -- SMT Verification -- A Flexible Proof Format for SAT Solver-Elaborator Communication -- Generating Extended Resolution Proofs with a BDD-Based SAT Solver -- Bounded Model Checking for Hyperproperties -- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays -- SAT Solving with GPU Accelerated Inprocessing -- FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions -- Probabilities -- Finding Provably Optimal Markov Chains -- Inductive Synthesis for Probabilistic Programs Reaches New Horizons -- Analysis of Markov Jump Processes under Terminal Constraints -- Multi-objective Optimization of Long-run Average and Total Rewards -- Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes -- Probabilistic and Systematic Coverage of Consecutive Test-Method Pairs for Detecting Order-Dependent Flaky Tests -- Timed Systems -- Timed Automata Relaxation for Reachability -- Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata -- Algebraic Quantitative Semantics for Efficient Online Temporal Monitoring -- Neural Networks -- Synthesizing Context-free Grammars from Recurrent Neural Networks -- Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models -- Improving Neural Network Verification through Spurious Region Guided Refinement -- Analysis of Network Communication Resilient Capacity-Aware Routing -- Network Traffic Classification by Program Synthesis. . , English

Additional Edition: ISBN 3-030-72015-2

Language: English

DOI: 10.1007/978-3-030-72016-2

UID:

Format: 1 Online-Ressource.

ISBN: 978-3-030-72016-2

Series Statement: Lecture notes in computer science 12651

Additional Edition: Erscheint auch als Druck-Ausgabe ISBN 978-3-030-72015-5

Language: English

Keywords: Konferenzschrift

DOI: 10.1007/978-3-030-72016-2

URL: Volltext  (kostenfrei)

URL: Volltext  (kostenfrei)

UID:

Format: 1 Online-Ressource.

ISBN: 978-3-030-72016-2

Series Statement: Lecture notes in computer science 12651

Additional Edition: Erscheint auch als Druck-Ausgabe ISBN 978-3-030-72015-5

Language: English

Keywords: Konferenzschrift

DOI: 10.1007/978-3-030-72016-2

URL: Volltext  (kostenfrei)

URL: Volltext  (kostenfrei)