Verification, Model Checking, and Abstract Interpretation

Name: Verification, Model Checking, and Abstract Interpretation | 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16-18, 2022, Proceedings
Brand: Springer
Price: 96.29 EUR
Availability: OnlineOnly

23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16-18, 2022, Proceedings

Bernd Finkbeiner Thomas Wies(Herausgeber*in)

Springer (Verlag)

Erschienen am 13. Januar 2022

X, 520 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-030-94583-1 (ISBN)

96,29 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Intro
Preface
Organization
Contents
Flavors of Sequential Information Flow
1 Introduction
2 The First-Order Logic of Trace Sets
2.1 Preliminaries
2.2 Hypertrace Logic
2.3 The Trace-Prefixed Fragment of Hypertrace Logic
2.4 The Time-Prefixed Fragment of Hypertrace Logic
3 Two-State Local Independence
4 Expressiveness
4.1 Indistinguishable Trace Sets
4.2 Point Semantics
4.3 Segment Semantics
5 Related Work
6 Conclusion
References
Relational String Abstract Domains
1 Introduction
1.1 Paper Contribution
1.2 Paper Structure
2 Related Work
3 Background
4 The Imp Language
5 A Suite of String Relational Abstract Domains
5.1 General Relational Framework
5.2 Character Inclusion Relational Abstract Domain
5.3 Substring Relational Abstract Domain
5.4 Extension to String Expressions
6 Experimental Results
6.1 Case Studies
6.2 Improving Precision of Non-relational Abstract Domains
6.3 Scalability of Sub
7 Conclusion
References
Fanoos: Multi-resolution, Multi-strength, Interactive Explanations for Learned Systems
1 Introduction
2 The Methodology of Fanoos
2.1 Knowledge Domains and User Questions
2.2 Reachability Analysis of the Learned System
2.3 Generating Descriptions
2.4 User Feedback and Revaluation
2.5 Capturing the Concept of Abstractness
3 Fanoos Interaction Example
4 Related Work and Discussion
5 Experiments and Results
5.1 Experiment Design
5.2 Metrics
5.3 Results
6 Conclusions and Future Work
References
Loop Verification with Invariants and Contracts
1 Introduction
2 Motivation and Overview
3 Preliminaries
4 Verification of Loops with Invariants and Contracts
5 Translating Between the Approaches
6 Loop Contracts in Hoare Logic
7 Specification of Examples and Comparison
8 Related Work
9 Conclusion and Outlook
References
EPMC Gets Knowledge in Multi-agent Systems
1 Introduction
2 Architecture
2.1 EPMC Core
2.2 Plugins Available in EPMC
2.3 PETL Model Checker as a Plugin
3 Empirical Evaluation
4 Related Work
5 Conclusion
References
High Assurance Software for Financial Regulation and Business Platforms
1 Introduction
2 MorphirIR Stack
2.1 Surface Languages
2.2 Validation Pipeline
2.3 Monitoring and Compilation
3 Validation Methodology
3.1 BSQChk Validation Workflow
4 MorphirIR Core Langauge
4.1 Types and Values
4.2 Expressions
4.3 Containers and Operations
5 Experience Report
5.1 Languages Targeting MorphirIR
5.2 Validation Pipeline
5.3 Injection of Compliance and Audit Logs
6 Conclusion
References
Gradient-Descent for Randomized Controllers Under Partial Observability
1 Introduction
2 Preliminaries
2.1 Parametric Markov Chains
2.2 Expected Rewards
2.3 Problem Statement
3 Computing Gradients for Expected Rewards
3.1 Equation-System Based Characterisation
3.2 Derived Automaton
4 Gradient Descent
4.1 Plain GD
4.2 GD Update Methods
4.3 Dealing with Parameter Regions
5 Empirical Evaluation
5.1 Set-Up
5.2 Results
6 Related Work
7 Conclusion and Future Work
References
Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking
1 Introduction
2 Preliminaries
2.1 Labelled Transition Systems
2.2 Linear Temporal Logic
2.3 Nondeterministic Büchi Automata
2.4 Petri Nets
3 Automata-Guided Partial Order Reduction
3.1 Automata-Driven Stubborn Set Method for LTL
3.2 Stubborn Sets for LTL Model Checking on Petri Nets
4 Automata-Driven Guided Search
5 Experimental Evaluation
6 Conclusion
References
Verifying Pufferfish Privacy in Hidden Markov Models
1 Introduction
2 Preliminaries
3 Pufferfish Privacy Framework
4 Geometric Mechanism as Hidden Markov Model
4.1 Geometric Mechanism
4.2 Differential Privacy Using Markov Chains
4.3 Pufferfish Privacy Using Hidden Markov Models
5 Pufferfish Privacy Verification
5.1 Complexity of Pufferfish Privacy Problem
5.2 Verifying Pufferfish Privacy
6 Pufferfish Privacy Verifier: FAIER
6.1 Evaluation for FAIER
6.2 Noisy Max
6.3 Above Threshold
7 Combining Techniques for Differential Privacy
7.1 Comparison
7.2 Combining Verification and Testing
8 Related Work
References
A Flow-Insensitive-Complete Program Representation
1 Introduction
2 Motivating Example
3 Background Definitions
3.1 Program
3.2 Static Information
3.3 Block Local Semantics
3.4 Flow-Sensitive Collecting Semantics
3.5 Flow-Insensitive Collecting Semantics
4 Flow-Insensitive Complete (FIC) Programs
5 Main Theorem: Flow Insensitive Completeness
6 Transformation to Flow Insensitive Complete Form
6.1 Sufficient Conditions for FIC Form
6.2 Transformation of a SSA Program Form to FIC Form
6.3 Correctness of the Transformation
7 Experiments
8 Related Work
9 Conclusion
References
Lightweight Shape Analysis Based on Physical Types
1 Introduction
2 Overview Example
3 Language and Semantics
4 Physical Representation Types
5 Type-Based Shape Domain
6 Static Analysis
7 Retained and Staged Points-To Predicates
8 Experimental Evaluation
9 Related Works and Conclusion
References
Fast Three-Valued Abstract Bit-Vector Arithmetic
1 Introduction
1.1 Our Contribution
2 Related Work
3 Basic Definitions
3.1 Abstract Bit Encodings
3.2 Abstract Transformers
3.3 Algorithm Complexity Considerations
3.4 Naïve Universal Abstract Algorithm
4 Formal Problem Statement
5 Modular Extreme-Finding Technique
6 Fast Abstract Addition
7 Fast Abstract Multiplication
7.1 Obtaining a Best Abstract Transformer
7.2 At Most One Double-Unknown k-th Column Pair
7.3 Multiple Double-Unknown k-th Column Pairs
7.4 Implementation Considerations
7.5 Fast Abstract Multiplication Algorithm
8 Experimental Evaluation
8.1 Visualisation and Interpretation
9 Conclusion
References
Satisfiability and Synthesis Modulo Oracles
1 Introduction
2 Oracles
2.1 Preliminaries and Notation
2.2 Basic Definitions
3 Satisfiability Modulo Theories and Oracles
3.1 Algorithm for Definitional SMTO
4 Synthesis Modulo Oracles
4.1 Algorithm for Synthesis with Oracles
5 Instances of Synthesis Modulo Oracles
6 Delphi: A Satisfiability and Synthesis Modulo Oracles Solver
6.1 Case Studies
6.2 Observations
7 Conclusion
References
Bisimulations for Neural Network Reduction
1 Introduction
2 Preliminaries
3 Neural Networks
4 NN-Bisimulation and Semantic Equivalence
5 -NN-Bisimulation and Semantic Closeness
6 Minimization Algorithm
7 Conclusions
References
NP Satisfiability for Arrays as Powers
1 Introduction
2 NP Complexity for Power Structures
2.1 Corollary: Quantifier-Free Skolem Arithmetic is in NP
3 Explicit Sets of Indices and a Polynomial Verifier for QFBAPA
4 NP Complexity for QFBAPAI
5 Combination with the Array Theory
6 Further Related Work
7 Conclusion and Future Work
References
STAMINA 2.0: Improving Scalability of Infinite-State Stochastic Model Checking
1 Introduction
2 Overview of the STAMINA Tool
3 Improvements over STAMINA 1.0
4 Results
5 Conclusion
References
Generalized Arrays for Stainless Frames
1 Introduction
2 First Example: Stack
3 Extended Example: Map on a Tree
4 First-Class Heaps
5 Heap Encoding
5.1 Encoding tmap
5.2 Translation Rules
5.3 Quantifier-Free Frame Conditions
5.4 First-Class Heaps
6 Evaluation
7 Conclusions
References
Making PROGRESS in Property Directed Reachability
1 Introduction
2 Related Work
3 Preliminaries
3.1 Basics and Notations
3.2 An Overview of PDR
4 Restrictions
4.1 Finding Proof Obligations
4.2 Generalizing Proof Obligations
4.3 Blocking Cubes
4.4 Generalizing Blocked Cubes
4.5 Overall Algorithm
5 Skipping Restrictions by Analyzing a Spurious Proof
5.1 Detecting Spurious Proofs in PDR
5.2 Restriction Skipping Loop
6 Implementation of PROGRESS-PDR
6.1 Combining PROGRESS-PDRwith Standard PDR
6.2 Choosing Appropriate Restrictions
6.3 PDR with Restrictions
6.4 Re-using Information from Previous Restricted PDR Run
7 Experimental Results
7.1 Design Decisions for PROGRESS-PDR
7.2 PROGRESS-PDRvs. PDR
7.3 PROGRESS-PDR vs. BMC
8 Conclusions and Future Work
References
Scaling Up Livelock Verification for Network-on-Chip Routing Algorithms
1 Introduction
2 Preliminaries
3 Related Work
4 Link-Fault-Tolerant Routing Algorithm
5 Refutation-Based Verification
5.1 Disproving Livelock Through Refutation-Based Simulation
5.2 Proving Livelock Using IVy
6 User-Aided Livelock Removal
7 Unroutable Packets
8 Zone-Based Routing Model
9 Zone-Based IVy Implementation
10 Verification of Livelock Freedom
10.1 Incremental Removal of Livelock Traces in Routing Algorithm
10.2 Verification Results for Zone-Based Routing Algorithm
10.3 Detecting Unroutable Packets
11 Conclusion
References
Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applications that Do Not Terminate
1 Introduction
2 Event-Driven Concurrency Model
2.1 Event-Driven Concurrency Model
2.2 Background on Stateless DPOR
3 Preliminaries
4 Technique Overview
4.1 Problem 1: Premature Termination
4.2 Problem 2: State Matching for Previously Explored States
4.3 Problem 3: State Matching Incompletely Explored States
4.4 Problem 4: Events as Transitions
5 Stateful Dynamic Partial Order Reduction
6 Implementation and Evaluation
6.1 Implementation
6.2 Evaluation
7 Related Work
8 Conclusion
References
Verifying Solidity Smart Contracts via Communication Abstraction in SmartACE
1 Introduction
2 Architecture and Design Principles of SmartACE
3 Contract Modelling
3.1 Static Analysis
3.2 Source-to-Source Translation
3.3 Harness Design
4 Integration with Analyzers
5 Case Study: Verifying OpenZeppelin Contracts
5.1 Verification of [language=Solidity,basicstyle=] Ownable
5.2 Verification of [language=Solidity,basicstyle=] RefundEscrow
5.3 Verification of [language=Solidity,basicstyle=] Auction
5.4 Discussion
6 Related Work
7 Conclusion
References
Out of Control: Reducing Probabilistic Models by Control-State Elimination
1 Introduction
2 A Bird's Eye View
3 Technical Background on PCFPs
4 PCFP Reduction
4.1 Variable Unfolding
4.2 Elimination
5 Implementation
6 Experiments
7 Conclusion
References
Mixed Semantics Guided Layered Bounded Reachability Analysis of Compositional Linear Hybrid Automata
1 Introduction
2 Background
3 Mixed Semantics Guided Layered BMC
3.1 Graph Structure Traversal Through Step Semantics
3.2 Path Feasibility Verification Through Shallow Semantics
3.3 Bounded Graph Structure Refinement
4 Path Pruning-Based Optimization
4.1 Non-identical Path Guided Path Pruning
4.2 Multiple Infeasible Path Segments-Based Pruning
5 Experimental Results
6 Related Work
7 Conclusion
References
Bit-Precise Reasoning via Int-Blasting
1 Introduction
2 Preliminaries
3 Integer Arithmetic with Bitwise and
4 Int-Blasting
4.1 From TBV to TIA (&N4pt)
4.2 Correctness
4.3 TIA (&N4pt)-Satisfiability: Eager Approach
4.4 TIA (&N4pt)-Satisfiability: Lazy Approach
5 Experimental Results
5.1 Implementation and Experiments
5.2 Results
6 Related Work, Conclusion, and Future Work
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken