Tests and Proofs

Name: Tests and Proofs | 18th International Conference, TAP 2024, Milan, Italy, September 9-10, 2024, Proceedings
Brand: Springer
Price: 139.09 EUR
Availability: OnlineOnly

18th International Conference, TAP 2024, Milan, Italy, September 9-10, 2024, Proceedings

Marieke Huisman Falk Howar(Herausgeber*in)

Springer (Verlag)

Erschienen am 9. September 2024

XIV, 177 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-031-72044-4 (ISBN)

139,09 €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
Invited Talk
Formalising Requirements for Verification
Contents
Invited Talks
Efficient Temporal Logic Runtime Monitoring for Tiny Systems
1 Introduction
2 Related Work
3 Linear Temporal Logic Runtime Monitoring on Small-Scale Systems - Step By Step
4 Keeping Track of Specification Violation Reasons
5 A Specialized Microcontroller Component for Temporal Logic Runtime Monitoring
6 Conclusion
References
Quality of Tests and Proofs
Is MCDC Really Better? Lessons from Combining Tests and Proofs
1 Overview
1.1 Coverage Measures
1.2 The Need for MCDC
1.3 Precise Definition and Properties of MCDC
2 Technology Base
2.1 The AutoProof Environment
2.2 Seeding Contradiction for Test Generation
2.3 SC for Achieving Branch Coverage
3 Seeding Contradiction for Achieving MCDC
3.1 Approach
3.2 Implementation
4 Evaluation
4.1 Experimental Setup
4.2 MCDC-SC Versus Branch-SC
4.3 MCDC-SC Versus Branch-SC and Adaptive Random Testing
5 Related Work
6 Limitations and Threats to Validity
7 Conclusions and Future Work
References
Refining CEGAR-Based Test-Case Generation with Feasibility Annotations
1 Introduction
2 Overview of CEGAR-Based Test-Case Generation
3 Feasibility Checking with Feasibility Annotations
3.1 Integrating Feasibility Annotations Into Satisfiability Checking
3.2 Learning from Unsatisfiability Proofs of Model-Guided Checks
3.3 Implementation
4 Experiments
4.1 Experimental Setup
4.2 Experimental Results
4.3 Threats to Validity
5 Related Work
6 Conclusion
References
No Smoke Without Fire: Detecting Specification Inconsistencies with Frama-C/WP
1 Introduction
2 Tracked Inconsistencies
2.1 Pre-condition Errors
2.2 Post-condition Errors
2.3 Dead Code Errors
2.4 Non-terminating Loops and Other Loop Errors
2.5 Exiting Errors
2.6 Avoiding Redundant Alarms
2.7 Avoiding Spurious Alarms
3 Design and Implementation
3.1 Reachability Analysis
3.2 Protected and Protecting Nodes
3.3 Weakest-Precondition Calculus for Smoke Tests
3.4 Proof Method
3.5 Providing Feedback to Users
4 Industrial Experiments
5 Related Work
6 Conclusion
References
Testing and Proving Advanced Properties
Runtime Verification for High-Level Security Properties: Case Study on the TPM Software Stack
1 Introduction
2 The Frama-C Verification Platform and Its Wp, E-ACSL and MetAcsl Plug-ins
3 Overview of the TPM and its Software Stack
4 Companion Memory Modeling for Sensitive Data
5 Defining and Verifying High-Level Security Properties
6 Evaluation and Key Lessons
6.1 Threats to Validity
6.2 Key Lessons
7 Related Work
8 Conclusion and Future Work
References
Cyclone: A New Tool for Verifying/Testing Graph-Based Structures
1 Introduction
2 Architecture
2.1 Usage
3 Building Graphs
3.1 Variables
3.2 Conditional Variables
3.3 Nodes and Edges
3.4 Conditional Transitions
3.5 Path Conditions
4 Specifying Properties
4.1 Assertions
4.2 Invariants
4.3 Checking Modes
5 Preliminary Evaluation
6 Related Work
6.1 Limitations
7 Conclusion
References
Applications of Tests and Proofs
Model-Based Testing of Quantum Computations
1 Introduction
2 Preliminaries
3 Test Models for Quantum Computations
3.1 Models of Quantum Computation
3.2 Process Models for Testing Quantum Computations
4 Test Processes for Quantum Computations
4.1 Test Processes and Tested Processes
4.2 Non-probabilistic Test Processes
4.3 Probabilistic Test Processes
5 Related Work
6 Conclusion
References
Affinitree: A Compositional Framework for Formal Analysis and Explanation of Deep Neural Networks
1 Introduction and Motivation
2 Theoretical Background
3 Related Work
4 Overview and Features
5 Design of Affinitree
5.1 Core Data Structure
5.2 Distillation Process
5.3 Modular Composition
5.4 Semantics-Preserving Pruning
5.5 Preconditions
6 Demonstration
6.1 Fairness Analysis
6.2 Decision Boundaries Near Adversarial Examples
6.3 Counterfactual Explanations
7 Conclusion
References
Exploring Loose Coupling of Slicing with Dynamic Symbolic Execution on the JVM
1 Introduction
2 Motivating Example
3 Analysis Pipeline
4 Results
5 Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken