Challenges of Software Verification (Intelligent Systems Reference Library, 238)

✍ Scribed by Vincenzo Arceri (editor), Agostino Cortesi (editor), Pietro Ferrara (editor), Martina Olliaro (editor)

• Publisher: Springer
• Year: 2023
• Tongue: English
• Leaves: 275
• Edition: 1st ed. 2023
• Category: Library

✦ Synopsis

This book provides an overview about the open challenges in software verification. Software verification is a branch of software engineering aiming at guaranteeing that software applications satisfy some requirements of interest. Over the years, the software verification community has proposed and considered several techniques: abstract interpretation, data-flow analysis, type systems, model checking are just a few examples. The theoretical advances have been always motivated by practical challenges that have led to an equal evolution of both these sides of software verification. Indeed, several verification tools have been proposed by the research community and any software application, in order to guarantee that certain software requirements are met, needs to integrate a verification phase in its life cycle, independently of the context of application or software size. This book is aimed at collecting contributions discussing recent advances in facing open challenges in software verification, relying on a broad spectrum of verification techniques. This book collects contributions ranging from theoretical to practical arguments, and it is aimed at both researchers in software verification and their practitioners.

✦ Table of Contents

Preface
Contents
Editors and Contributors
About the Editors
Contributors
1 Abstract Interpretation: From 0, 1, to infty
1.1 Introduction
1.2 Abstract Interpretation for the Untaught
1.3 Abstract Interpretation for the Savant
1.3.1 Software Engineering
1.3.2 Education
1.3.3 Scope of Abstract Interpretation
1.3.4 More Complex Properties
1.3.5 Properties of More Complex Data Structures
1.3.6 Properties of More Complex Control Structures
1.3.7 Computation Spaces
1.3.8 Choosing Precise and Efficient Abstractions
1.3.9 Induction Abstraction
1.3.10 Calculational Design of Abstract Interpreters
1.3.11 Language-Independent Abstract Interpretation
1.3.12 New Computation Models and Challenges
1.4 Conclusion
References
2 LiSA: A Generic Framework for Multilanguage Static Analysis
2.1 Introduction
2.1.1 An Illustrative Example
2.1.2 Contribution and Paper Structure
2.2 LiSA's Overall Architecture
2.3 The Internal Language
2.3.1 Control Flow Graphs
2.3.2 Symbolic Expressions
2.4 The Analysis State
2.5 Interprocedural Analysis
2.6 Frontends
2.7 Multilanguage Analysis
2.8 Conclusion
2.8.1 Future Directions
2.8.2 Related Work
References
3 How to Make Taint Analysis Precise
3.1 Introduction
3.2 Concrete Semantics
3.2.1 Influenced Concrete States
3.2.2 Semantics of Basic Instructions
3.2.3 Partial Traces Semantics
3.2.4 Reachable States Semantics
3.3 Application to Security
3.3.1 Sources
3.3.2 Sinks
3.3.3 Sanitizers
3.4 Data Flow Analyses for Security
3.5 Reachable States-Based Taint Analysis
3.6 Trace-Based Taint Analysis
3.6.1 Trace Influence Algebra
3.6.2 Influence Semantics with Features
3.6.3 Inter-Procedural Analysis
3.6.4 Features for Analysis Approximations
3.7 Experience
3.8 Conclusions
References
4 ``Fixing'' the Specification of Widenings
4.1 Introduction
4.2 Background
4.3 On the Specification of Widening Operators
4.3.1 Classifying Abstract Domain Implementations
4.3.2 Classifying AI Engine Implementations
4.4 Combinations of Abstract Domains and AI Engines
4.4.1 Some Thoughts on the Unsafe Combinations
4.4.2 Comparing the Safe Combinations
4.5 Lesson Learned and Recommendation
4.5.1 Safe Widenings for Convex Polyhedra
4.5.2 A Note on the Unusual Widening Specifications
4.6 Conclusion
References
5 Static Analysis for Data Scientists
5.1 Introduction
5.1.1 Example
5.1.2 Data Expectation Static Analyses
5.2 Input Data-Aware Concrete Semantics
5.2.1 Input Data
5.2.2 Dataframe-Manipulating Language
5.2.3 Input-Aware Semantics
5.3 Expectations Abstract Domains
5.3.1 Column Expectations Abstract Domain
5.3.2 Other Expectations Abstract Domains
5.4 Implementation
5.5 Conclusion
References
6 Completeness in Static Analysis by Abstract Interpretation: A Personal Point of View
6.1 Introduction
6.2 Completeness of the Abstraction: the Case of LRU Caches
6.3 Completeness or Incompleteness of the Analysis Method
6.3.1 Widening Operators
6.3.2 Exact Solving
6.3.3 Imprecise Abstract Transfer Functions
6.4 Undecidability of an Abstraction
6.4.1 Polyhedral Abstraction
6.4.2 Richer Domains
6.5 Perspectives and Conclusion
References
7 Lifting String Analysis Domains
7.1 Introduction
7.1.1 Paper Contribution
7.1.2 Paper Structure
7.2 Background
7.2.1 Mathematical Notation
7.2.2 Abstract Interpretation
7.2.3 Reduced Product
7.2.4 Granger Product
7.2.5 String Operators
7.3 Related Work
7.3.1 Enhancing Operators
7.3.2 Combinations of String Analyses
7.3.3 String Analysis: Applications
7.4 Concrete Domain and Semantics
7.4.1 Concrete Domain
7.4.2 Concrete Semantics
7.4.3 Example
7.5 String Abstract Domains
7.5.1 String Length
7.5.2 Character Inclusion
7.5.3 Prefix and Suffix
7.6 Segmentation Abstract Domain
7.6.1 Strings Concrete Representation
7.6.2 Abstract Domain
7.6.3 Abstract Semantics
7.7 Refined String Abstract Domains
7.7.1 Meaning of Refinement
7.7.2 Combining Segmentation and String Length Domains
7.7.3 Combining Segmentation and Character Inclusion Domains
7.7.4 Combining Segmentation and Prefix Domains
7.8 Conclusion
References
8 Local Completeness in Abstract Interpretation
8.1 Completeness, Fallacy, and Approximation
8.2 Proving Completeness
8.3 LCL: Local Completeness Logic
8.4 Concluding Remarks
References
9 The Top-Down Solver—An Exercise in A2I
9.1 Introduction
9.2 Getting Started
9.3 Adding Fixpoint Iteration
9.4 The Top-Down Solver TD
9.5 The Top-Down Solver with Tabulation
9.6 Introducing Widening and Narrowing
9.7 Conclusion
References
10 Regular Matching with Constraint Programming
10.1 Introduction
10.2 Preliminaries
10.2.1 Strings and Regular Languages
10.2.2 Constraint Programming and String Solving
10.3 Matching Regular Expressions
10.3.1 Match
10.3.2 Generalization to replace
10.4 Conclusions
References
11 Floating-Point Round-off Error Analysis of Safety-Critical Avionics Software
11.1 Introduction
11.2 Formal Verification of the ADS-B CPR Algorithm
11.3 Automatizing the Verification with PRECiSA
11.4 Case Study: Point-in-Polygon Algorithm
11.5 Related Work
11.6 Conclusion and Future Challenges
References
12 Risk Estimation in IoT Systems
12.1 Introduction
12.2 Indoor Environmental Monitoring Scenario
12.3 Technical Background
12.3.1 Overview of IoT-LySa
12.3.2 Control Flow Analysis
12.4 Using the CFA Results for Analysing Critical Decisions
12.4.1 Taint Analysis
12.4.2 What if Reasoning
12.4.3 Estimation of Risks
12.5 Concluding Remarks
References
13 Verification of Reaction Systems Processes
13.1 Introduction
13.2 Reaction Systems
13.3 SOS Rules for Reaction Systems
13.4 Bio-simulation
13.4.1 Assertion Language
13.4.2 Bio-similarity and Biological Equivalence
13.4.3 A Case Study: Metabolic Pathways in Mammalian Epithelial Cells
13.4.4 Dynamic Slicing of RS Processes
13.5 Quantitative Extensions of RSs
13.6 Implementation and Experimentation
13.7 Related Work
13.8 Conclusion and Future Work
References