Cover Image

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

Bibliographic Details
Main Author: Groote, Jan Friso.
Other Authors: Larsen, Kim Guldstrand.
Format: eBook
Language:English
Published: Cham : Springer International Publishing AG, 2021.
Edition:1st ed.
Series:Lecture Notes in Computer Science Series
Subjects:
Electronic books.
Online Access:Click to View
Table of Contents:
  • Intro
  • ETAPS Foreword
  • Preface
  • Organization
  • Contents - Part II
  • Contents - Part I
  • Verification Techniques (not SMT)
  • Directed Reachability for Infinite-State Systems
  • 1 Introduction
  • 2 Preliminaries
  • 3 Directed Search Algorithms
  • 4 Directed Reachability
  • 4.1 Distance Under-approximations
  • 4.2 From Petri Net Relaxations to Distance Under-approximations
  • 4.3 Directed Reachability Based on Distance Under-approximations
  • 5 Experimental Results
  • References
  • Bridging Arrays and ADTs in Recursive Proofs
  • 1 Introduction
  • 2 Preliminaries
  • 3 Synthesis of Recursive Relational Invariants
  • 3.1 Overview
  • 3.2 Classifying Operations
  • 4 Recipe 1: Linear Scan
  • 4.1 Motivating Example
  • 4.2 Algorithm Description
  • 5 Recipe 2: Noop-based synthesis
  • 5.1 Motivating Example
  • 5.2 Algorithm details
  • 6 Evaluation
  • 7 Related Work
  • 8 Conclusion and Outlook
  • References
  • A Two-Phase Approach forConditional Floating-Point Verification
  • 1 Introduction
  • 2 A Two-Phase Approach
  • 2.1 First Phase: Whole Program Analysis
  • 2.2 Second Phase: Numerical Kernel Analysis
  • 2.3 Soundness Guarantees
  • 3 First Phase: Whole Program Analysis
  • 4 Second Phase: Static Analysis with Daisy and CBMC
  • 5 State of the Art on Real-World Programs
  • 6 Evaluation of our Two-Phase Approach
  • 7 Related Work
  • 8 Conclusion
  • Acknowledgements
  • References
  • Symbolic Coloured SCC Decomposition
  • 1 Introduction
  • 1.1 Related Work
  • 2 Problem Definition
  • 2.1 Graphs and Strongly Connected Components
  • 2.2 Coloured SCC Decomposition Problem
  • 3 Algorithm
  • 3.1 Symbolic Computation Model
  • 3.2 Forward-backward Algorithm
  • 3.3 Lock-step Algorithm
  • 3.4 Coloured Lock-step Algorithm
  • 3.5 Correctness and Complexity of the Coloured Lock-step Algorithm
  • 4 Experimental Evaluation
  • 4.1 Implementation
  • 4.2 Experiments.
  • 5 Conclusions
  • References
  • Case Studies
  • Local Search with a SAT Oracle for Combinatorial Optimization
  • 1 Introduction
  • 2 Background
  • 2.1 Constraint Optimization Program (COP)
  • 2.2 The Cell Placement Problem
  • 2.2.1 Constraint Optimization Program for Cell Placement
  • 2.3 Solving COP with SAT
  • 2.3.1 Bit-vector Solving and SAT.
  • 2.3.2 Extending Bit-vector Solving to Optimization.
  • 2.4 Local Search Algorithms
  • 2.4.1 Basic Local Search Strategy.
  • 2.4.2 Neighbourhood Functions.
  • 2.4.3 Advanced Versions of Local Search
  • 3 Local Search with SAT Oracle (LSSO)
  • 4 LSSO Algorithms for the Cell Placement Problem
  • 4.1 Neighbourhood Generators
  • 4.1.1 Neighbourhood Generator
  • 4.1.2 N₂: a Family of Neighbourhood Generators
  • 4.1.3 Hill-climbing Neighbourhood Generator N₃.
  • 4.2 LSSO-based Algorithms for Placement
  • 5 Experimental Results
  • 6 Conclusion
  • References
  • Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities
  • 1 Introduction
  • 1.1 Proof of Concept
  • 1.2 Detecting Intra-update Sniping Vulnerabilities
  • 2 A Model for Infrastructure as Code
  • 2.1 CloudFormation Infrastructures
  • 2.2 Model of a CloudFormation Infrastructure
  • 2.3 Execution Semantics
  • 2.4 Upgrade Semantics and Security Policy
  • 3 Architectural Design of the Hayha Tool
  • 3.1 Upgrade States
  • 3.2 Splitting Dependencies
  • 3.3 Finding Vulnerabilities
  • 4 Experiments
  • 5 Related Work
  • 6 Conclusion
  • Acknowledgement
  • References
  • Proof Generation/Validation
  • Certifying Proofs in the First-Order Theory of Rewriting
  • 1 Introduction
  • 2 Preliminaries
  • 3 Formulas
  • 4 Certificates
  • 5 FORTify
  • 6 FORT-h
  • 7 Experiments
  • 8 Conclusion
  • References
  • Syntax-Guided Quantifier Instantiation
  • 1 Introduction
  • 2 Background
  • 3 SyGuS Quantifier Instantiation (SyQI)
  • 3.1 Grammar Construction.
  • 3.2 Implementation Details
  • 4 Experiments
  • 5 Conclusion
  • References
  • Making Theory Reasoning Simpler
  • 1 Introduction
  • 2 Preliminaries and Related Work
  • 3 Gaussian variable elimination
  • 4 Arithmetic subterm generalization
  • 5 Evaluation
  • 6 Cancellation
  • 7 Experimental evaluation
  • 8 Conclusion
  • References
  • Deductive Stability Proofs for Ordinary Differential Equations
  • 1 Introduction
  • 2 Background: Di erential Dynamic Logic
  • 3 Asymptotic Stability of an Equilibrium Point
  • 3.1 Mathematical Preliminaries
  • 3.2 Formal Specification
  • 3.3 Lyapunov Functions
  • 3.4 Asymptotic Stability Variations
  • 4 General Stability
  • 4.1 General Stability and General Attractivity
  • 4.2 Specialization
  • 5 Stability in KeYmaera X
  • 6 Related Work
  • 7 Conclusion
  • References
  • Tool Papers
  • An SMT-Based Approach for Verifying Binarized Neural Networks
  • 1 Introduction
  • 2 Background
  • 3 Extending Reluplex to Support Sign Constraints
  • 4 Optimizations
  • 5 Implementation
  • 6 Evaluation
  • 7 Related Work
  • 8 Conclusion
  • Acknowledgements.
  • References
  • cake_lpr: Verified Propagation Redundancy Checking in CakeML
  • 1 Introduction
  • 2 Background
  • 2.1 HOL4 and CakeML
  • 2.2 SAT Problems and Clausal Proofs
  • 3 Linear Propagation Redundancy
  • 4 CakeML Proof Checking
  • 4.1 Verification Strategy
  • 4.2 Verified Optimizations
  • 5 Benchmarks
  • 5.1 SaDiCaL PR Benchmarks
  • 5.2 SAT Race 2019 Benchmarks
  • 5.3 Mutilated Chessboard RAT Microbenchmarks
  • 6 Related Work
  • 7 Conclusion
  • Acknowledgments.
  • A Correctness Theorem for cake_lpr
  • References
  • Deductive Verification of Floating-Point Java Programs in KeY
  • 1 Introduction
  • 2 Background
  • 2.1 Introduction to KeY
  • 2.2 Floating-Point Arithmetic in Java
  • 3 Floating-Point Support in KeY
  • 3.1 Arithmetics
  • 3.2 Transcendental Functions
  • 4 Evaluation.
  • 4.1 Benchmark Programs
  • 4.2 Proof Obligation Generation
  • 4.3 Evaluation of SMT Floating-Point Support
  • 4.4 Evaluation of Support for Transcendental Functions in KeY
  • 4.5 Discussion and insights
  • 5 Related Work
  • 6 Conclusion
  • Acknowledgements
  • References
  • Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types
  • 1 Introduction
  • 2 Overview of Helmholtz and Michelson
  • 2.1 Helmholtz
  • 2.2 An Example Contract in Michelson
  • 2.3 Specification
  • 3 Refinement Type System for Mini-Michelson
  • 3.1 Operational Semantics
  • 3.2 Refinement Type System
  • 4 Tool Implementation
  • 4.1 Annotations
  • 4.2 Case Study: Contract with Signature Verification
  • 4.3 Experiments
  • 5 Related Work
  • 6 Conclusion
  • References
  • SyReNN: A Tool for Analyzing Deep Neural Networks
  • 1 Introduction
  • 2 Preliminaries
  • 3 A Symbolic Representation of DNNs
  • 4 Computing the Symbolic Representation
  • 4.1 Algorithm for Extend
  • 4.2 Representing Polytopes
  • 5 SyReNN tool
  • 6 Applications of SyReNN
  • 6.1 Integrated Gradients
  • 6.2 Visualization of DNN Decision Boundaries
  • 6.3 Patching of DNNs
  • 7 Related Work
  • 8 Conclusion and Future Work
  • References
  • MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers
  • 1 Introduction
  • 2 Background
  • 2.1 A Brief Overview of Algorithm Selection
  • 2.2 Supervised Learning, Adaptive Boosting, Curse of Dimensionality, and K-Fold Cross-Validation
  • 2.3 Unsupervised Learning and Principal Component Analysis
  • 3 An overview of MachSMT
  • 3.1 Features, Preprocessing, and Learning
  • 3.2 Variants of MachSMT
  • 3.3 Using MachSMT
  • 3.4 User-defined Features
  • 4 Experimental Evaluation of MachSMT on SMT-COMP 2019 and 2020 Data
  • 4.1 Experimental Setup and Methodology
  • 4.2 Experimental Results
  • 5 Analysis and Discussion of Results
  • 6 Related Work.
  • 6.1 Key di erences between SATZilla and MachSMT
  • 6.2 Algorithm Selection for Logic Solvers and Their Applications
  • 7 Conclusions and Future Work
  • References
  • dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts
  • 1 Introduction
  • 2 Decision tree learning for controller representation
  • 3 Tool
  • 4 Predicate domain
  • 4.1 Categorical predicates
  • 4.2 Algebraic predicates
  • 5 Predicate selection
  • 6 New insights about determinization
  • 7 Experiments
  • 8 Conclusion
  • References
  • Tool Demo Papers
  • HLola: a Very Functional Tool for Extensible Stream Runtime Verification
  • 1 Introduction
  • 2 The HLola Tool
  • 3 Example Specifications
  • References
  • AMulet 2.0 for Verifying Multiplier Circuits
  • 1 Introduction
  • 2 Circuit Verification using Computer Algebra
  • 3 Usage
  • 4 AMulet 2.0
  • 5 Evaluation
  • 6 Conclusion
  • References
  • RTLola on Board: Testing Real Driving Emissions on your Phone
  • 1 Introduction
  • 2 RDE Monitoring on Android
  • 3 User Experience
  • 4 Conclusion
  • References
  • Replicating Restart with ProlongedRetrials: An Experimental Report
  • 1 Introduction
  • 2 Restart with Prolonged Retrials
  • 3 Experiments
  • 4 Conclusion
  • References
  • A Web Interface for Petri Nets with Transits and Petri Games
  • 1 Introduction
  • 2 Web Interface for Petri Nets with Transits
  • 3 Web Interface for Petri Games
  • 4 Implementation Details
  • 5 Conclusion
  • References
  • Momba: JANI Meets Python
  • 1 Introduction
  • 2 Scenario-Based Model Construction
  • 3 Validation by Simulation
  • 4 Harvesting the Benefits
  • 5 Conclusion
  • References
  • SV-Comp Tool Competition Papers
  • Software Verification: 10th Comparative Evaluation (SV-COMP 2021)
  • 1 Introduction
  • 2 Organization, Definitions, Formats, and Rules
  • 3 Reproducibility
  • 4 Results and Discussion
  • 5 Conclusion.
  • References.

Similar Items