.

0 (hodnocen0 x )

EB

ONLINE

Cham : Springer International Publishing AG, 2022

1 online resource (591 pages)

ISBN 9783030995249 (electronic bk.)

ISBN 9783030995232

Lecture Notes in Computer Science Ser. ; v.13243

Print version: Fisman, Dana Tools and Algorithms for the Construction and Analysis of Systems Cham : Springer International Publishing AG,c2022 ISBN 9783030995232

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.

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.

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.

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.

2.4 Limitations of Existing Methods.

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.

001896862

express

(Au-PeEL)EBL6942717

(MiAaPQ)EBC6942717

(OCoLC)1308973745