|
|
|
|
| LEADER |
11346nam a22004693i 4500 |
| 001 |
EBC6942717 |
| 003 |
MiAaPQ |
| 005 |
20231204023222.0 |
| 006 |
m o d | |
| 007 |
cr cnu|||||||| |
| 008 |
231204s2022 xx o ||||0 eng d |
| 020 |
|
|
|a 9783030995249
|q (electronic bk.)
|
| 020 |
|
|
|z 9783030995232
|
| 035 |
|
|
|a (MiAaPQ)EBC6942717
|
| 035 |
|
|
|a (Au-PeEL)EBL6942717
|
| 035 |
|
|
|a (OCoLC)1308973745
|
| 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 I.
|
| 250 |
|
|
|a 1st ed.
|
| 264 |
|
1 |
|a Cham :
|b Springer International Publishing AG,
|c 2022.
|
| 264 |
|
4 |
|c Ã2022.
|
| 300 |
|
|
|a 1 online resource (591 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.13243
|
| 505 |
0 |
|
|a Intro -- ETAPS Foreword -- Preface -- Organization -- Contents - Part I -- Contents - Part II -- Synthesis -- HOLL: Program Synthesis for Higher Order Logic Locking -- 1 Introduction -- 2 HOLL Overview -- 2.1 Threat Model: the Untrusted Foundry -- 2.2 Defending with HOLL -- 2.3 Attacking with SynthAttack -- 3 Program Synthesis to Infer Key Relations -- 3.1 Lock and Key Inference -- 3.2 Expression Selection -- 4 HOLL: Implementation and Optimization -- 5 SynthAttack: Attacking HOLL with Program Synthesis -- 5.1 The SynthAttack Algorithm -- 6 Experimental Evaluation -- 6.1 Attack Resilience -- 6.2 Impact of Expression Selection on Attack Resilience -- 6.3 Hardware cost -- 7 Related Work -- 8 Discussion -- References -- The Complexity of LTL Rational Synthesis -- 1 Introduction -- 2 Preliminaries -- 2.1 LTL, trees, and automata -- 2.2 Concurrent multiplayer games -- 3 Rational Synthesis -- 4 The Complexity of Cooperative Rational Synthesis -- 5 The Complexity of Non-Cooperative Rational Synthesis -- 5.1 Turn-based games -- 5.2 Concurrent games -- 5.3 General rational synthesis -- References -- Synthesis of Compact Strategies for Coordination Programs -- 1 Introduction -- 2 Background -- 3 Compactness -- 3.1 Effective Minimality Constructions for LTL -- 3.2 Relationship to Quantitative Synthesis -- 3.3 Approximating Compactness -- 4 Evaluation -- 4.1 Multi-Robot Coordination -- 4.2 Compactness for LTL -- 5 Related Work -- References -- ZDD Boolean Synthesis -- 1 Introduction -- 2 Preliminaries -- 3 Realizability Using ZDDs -- 3.1 Realizable Set R -- 3.2 Full and Partial Realizability -- 4 Synthesis Using ZDDs -- 4.1 Witnesses for Single-Dimension Output Variable -- 4.2 Preserve CNF by Equivalent Witnesses -- 4.3 Algorithm for Constructing Witnesses -- 5 Experimental Evaluations -- 5.1 Experimental Methodology and and Setting.
|
| 505 |
8 |
|
|a 5.2 Compilation Time and Size of Diagram Representing Original Formula -- 5.3 Realizability Time -- 5.4 End-to-End Time and Peak Memory -- 5.5 Scalable Benchmarks Show ZDD has Slower Growing Demands of Time and Space -- 5.6 Overall Comparison -- 6 Conclusion -- References -- Verification -- Comparative Verification of the Digital Library of Mathematical Functions and Computer Algebra Systems -- 1 Introduction -- 1.1 Related Work -- 2 The DLMF dataset -- 3 Semantic LATEX to CAS translation -- 3.1 Parse sums, products, integrals, and limits -- 3.2 Lagrange's notation for differentiation and derivatives -- 4 Evaluation of the DLMF using CAS -- 4.1 Symbolic Evaluation -- 4.2 Numerical Evaluation -- 5 Results -- 5.1 Error Analysis -- 6 Conclusion -- 6.1 Future Work -- References -- Verifying Fortran Programs with CIVL -- 1 Introduction -- 2 Overview of CIVL Extension -- 3 Defect-Preserving Translation -- 3.1 Translation from Source to Source -- 3.2 Translation for Compilation -- 3.3 Translation for Verification -- 4 Fortran Array Modeling -- 4.1 Fortran Array Semantics -- 4.2 Modeling Fortran Arrays for Verification -- 5 Evaluation -- 5.1 Compute Environment and Experimental Artifacts -- 5.2 Specification and Verification Approach -- 5.3 Fortran Verification Benchmark Suites -- 5.4 Verifying Nek5000 Components -- 6 Related Work -- 7 Conclusion and Future Work -- References -- NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems -- 1 Introduction -- 2 Relay-based Railway Interlocking Systems -- 3 Norma: overview -- 4 Graphical modeling of RRIS -- 5 Compilation in Timed SMV -- 6 Simplification of RRIS models -- 6.1 Equivalence propagation -- 6.2 Abstracting electrical variables -- 7 Software architecture -- 8 Experimental Evaluation -- 9 Conclusions -- References -- Efficient Neural Network Analysis with Sum-of-Infeasibilities.
|
| 505 |
8 |
|
|a 1 Introduction -- 2 Related Work -- 3 Preliminaries -- 4 Sum of Infeasibilities in Neural Network Analysis -- 4.1 The Sum of Infeasibilities -- 4.2 Stochastically Minimizing the SoI with MCMC Sampling -- 5 The DeepSoI Algorithm -- 5.1 DeepSoI -- 5.2 Complete Analysis and Pseudo-impact Branching -- 6 Experimental Evaluation -- 6.1 Implementation. -- 6.2 Benchmarks. -- 6.3 Experimental Setup. -- 6.4 Ablation study of the proposed techniques. -- 6.5 Comparison with other complete analyzers. -- 6.6 Incremental Solving and the Rejection Threshold T -- 6.7 Improving the perturbation bounds found by AutoAttack -- 7 Conclusions and Future Work -- References -- Blockchain -- Formal Verification of the Ethereum 2.0 Beacon Chain -- 1 Introduction -- 2 The Beacon Chain Reference Implementation -- 2.1 System Description and Scope of the Study -- 2.2 The Beacon Chain Reference Implementation -- 2.3 Motivation for Formal Verification -- 2.4 Objectives of the Study -- 3 Formal Specification and Verification -- 3.1 Challenges -- 3.2 Methodologies -- 3.3 Results -- 4 Findings and Lessons Learned -- 4.1 Array-out-of-bounds Runtime Error -- 4.2 Beyond Runtime Errors -- 4.3 Finalisation and Justification -- 4.4 Reection -- 5 Conclusion -- References -- Fast and Reliable Formal Verification of Smart Contracts with the Move Prover -- 1 Introduction -- 2 Move and the Prover -- 3 Move Prover Design -- 3.1 Reference Elimination -- 3.2 Global Invariant Injection -- 3.3 Monomorphization -- 4 Analysis -- 5 Conclusion -- References -- A Max-SMT Superoptimizer for EVM handling Memory and Storage -- 1 Introduction and Related Work -- 2 The Architecture of GASOL -- 3 Synthesis of Stack and Memory Specifications -- 3.1 Initial Stack and Memory/Storage Specification -- 3.2 Memory/Storage Simplifications -- 3.4 Bounding the Operations Position -- 4 Max-SMT Superoptimization.
|
| 505 |
8 |
|
|a 4.1 Stack Representation in the SMT Encoding -- 4.2 Encoding the Pre-order Relation -- 4.3 Optimization using Max-SMT -- 5 Implementation and Experiments -- 6 Conclusions and Future Work -- References -- Grammatical Inference -- A New Approach for Active Automata Learning Based on Apartness -- 1 Introduction -- 2 Partial Mealy Machines and Apartness -- 3 Learning Algorithm -- 3.1 Hypothesis construction -- 3.2 Main loop of the algorithm -- 3.3 Consistency checking -- 3.4 Counterexample processing -- 3.5 Adaptive distinguishing sequences -- 3.6 Complexity -- 4 Experimental Evaluation -- 5 Conclusions and Future Work -- References -- Learning Realtime One-Counter Automata -- 1 Introduction -- 2 Preliminaries -- 3 Learning ROCAs -- 4 Experiments -- 4.1 Random ROCAs -- 4.2 JSON Documents and JSON Schemas -- 5 Future Work -- References -- Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic -- 1 Introduction -- 2 Preliminaries -- 3 High-level view of the algorithm -- 4 Searching for directed formulas -- 5 Boolean combinations of formulas -- 6 Theoretical guarantees -- 7 Experimental evaluation -- 7.1 RQ1: Performance Comparison -- 7.2 RQ2: Scalability -- 7.3 RQ3: Anytime Property -- 8 Conclusion -- References -- Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes -- 1 Introduction -- 1.1 Related Work -- 2 Background -- 2.1 Signal Temporal Logic -- 2.2 Kernel Crash Course -- 3 Overview of Our Approach and Results -- 4 A Kernel for Signal Temporal Logic -- 4.1 Definition of STL Kernel -- 4.2 The Base Measure 0 -- 4.3 Normalized Robustness -- 4.4 PAC Bounds for the STL Kernel -- 5 Experiments -- 5.1 Setting -- 5.2 Robustness and Satisfaction on Single Trajectories -- 5.3 Expected Robustness and Satisfaction Probability -- 5.4 Kernel Regression on Other Stochastic Processes -- 6 Conclusions.
|
| 505 |
8 |
|
|a References -- Verification Inference -- Inferring Interval-Valued Floating-Point Preconditions -- 1 Introduction -- 2 Overview -- 3 Precondition Inference by Subdivision -- 3.1 Extracting a Verified Precondition from Subdivisions -- 3.2 Precondition Optimization -- 4 Precondition Inference by Decision Tree Learning -- 4.1 Extracting Candidates from a Classification Tree -- 4.2 Refining Candidates by Growing Regions -- 4.3 Refining Candidates by Recursive Subdivision -- 5 Evaluation -- 6 Related Work -- 7 Conclusion -- References -- NeuReach: Learning Reachability Functions from Simulations -- 1 Introduction -- 2 Related work -- 3 Problem setup and an overview of the tool -- 4 Design of NeuReach: Learning reachability functions -- 4.1 Reachability with Empirical Risk Minimization -- 4.2 Probabilistic Correctness of NeuReach -- 5 Experimental evaluation -- 5.1 Benchmark systems -- 5.2 Experimental results -- 6 Conclusion -- References -- Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion -- 1 Introduction -- 2 Background -- 3 Breadth-First Inductive Generalization with Separation -- 3.1 Naive Inductive Generalization with Separation -- 3.2 Prefix Search at the Inductive Generalization Level -- 3.3 Algorithm for Inductive Generalization -- 4 k-Term Pseudo-DNF -- 5 An Algorithm for Invariant Inference -- 5.1 May-proof-obligations -- 5.2 Multi-block Generalization -- 5.3 Enforcing EPR -- 5.4 SMT Robustness -- 5.5 Complete Algorithm -- 6 Evaluation -- 6.1 Invariant Inference Benchmark -- 6.2 Experimental Setup -- 6.3 Results and Discussion -- 6.4 Ablation Study -- 7 Related Work -- 8 Conclusion -- References -- LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions -- 1 Introduction -- 2 Preliminaries -- 2.1 Neural Networks -- 2.2 Neural Network Verification -- 2.3 Existing Methods.
|
| 505 |
8 |
|
|a 2.4 Limitations of Existing Methods.
|
| 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 9783030995232
|
| 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=6942717
|z Click to View
|
