Tests and Proofs
18th International Conference, TAP 2024, Milan, Italy, September 9-10, 2024, Proceedings
Published on 9. September 2024
XIV, 177 pages
978-3-031-72044-4 (ISBN)
Description
This book constitutes the proceedings of the 18th International Conference on Tests and Proofs, TAP 2024. TAP 2024 took place in Milan, Italy, on September 9 and 10, 2024 as part of the Formal Methods symposium (FM 2024), which included four more co-located conferences besides TAP: FMICS (Formal Methods in Industrial Critical Systems), LOPSTR (In ternational Symposium on Logic-based Program Synthesis and Transformation), PPDP (International Symposium on Principles and Practice of Declarative Pro gramming), and FACS (International Conference on Formal Aspects of Compo nent Software.
The 7 full papers together with 1 short paper included in this volume were carefully reviewed and selected from 14 submissions. TAP's scope encompasses many aspects of verification technology, including foundational work, tool development, and empirical research.
More details
Series
Language
English
Place of publication
Cham
Switzerland
Publishing group
Springer International Publishing
Target group
Professional and scholarly
Product notice
Reflowable
Illustrations
XIV, 177 p. 64 illus., 33 illus. in color.
File size
9,08 MB
ISBN-13
978-3-031-72044-4 (9783031720444)
DOI
10.1007/978-3-031-72044-4
Schweitzer Classification
Other editions
Additional editions
Marieke Huisman | Falk Howar
Tests and Proofs
18th International Conference, TAP 2024, Milan, Italy, September 9-10, 2024, Proceedings
Book
09/2024
Springer
€149.79
Shipment within 15-20 days
Content
- 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
