Tools and Algorithms for the Construction and Analysis of Systems : : 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.

Tools and Algorithms for the Construction and Analysis of Systems : : 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.

Saved in:
Bibliographic Details
Superior document:Lecture Notes in Computer Science Series ; v.13243
:
Fisman, Dana.
TeilnehmendeR:
Rosu, Grigore.
Place / Publishing House:Cham : : Springer International Publishing AG,, 2022.
Ã2022.
Year of Publication:2022
Edition:1st ed.
Language:English
Series:Lecture Notes in Computer Science Series
Online Access:
Physical Description:1 online resource (591 pages)
Tags: Add Tag
No Tags, Be the first to tag this record!
Table of Contents:
  • 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.
  • 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.
  • 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.

Similar Items