Delta-based Verification of Software Product Families
summary
Delta-based verification represents original calls as abstract execution statements and requires methods to be refactored into a Shallow Single Original Normal Form so each delta can be verified in isolation. A formal Change-Old-Behavior schema plus abstract execution proofs ensure refactorings are semantics-preserving, letting modifications change behavior while keeping verification costs polynomial instead of exponential. Benchmarks on BankAccount and MinePump show comparable costs for small changes and much lower re-verification effort when adding methods.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:22Problem Statement
- 1:03Contrastbased Approach
- 1:57Productbased Approach
- 2:40Latent Substitution Principle
- 3:41Problem
- 5:51Abstract Statement
- 6:56Behavior Preserving Methods
- 7:29NonBehavior Preserving Methods
- 9:01NonBehavior Refactoring
- 9:28General Schemata
- 12:55Comparison
- 13:43Recap
related talks
28mGradual Verification: Assuring Software Incrementally
15mOn the Impact of Formal Verification on Software Development
19mPredictable Verification using Intrinsic Definitions
01h 02mLanguage Design meets Verifying Compilers
20mDark Factories: Verification-First Agentic Engineering
24mProving False in Object Oriented Verification Programs by Exploiting Non-Termination
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
14mAutomatically Verifying Replication-aware Linearizability