Liveness for Verification
Roly Perera, Simon J. Gay

TL;DR
This paper introduces a novel approach to program verification using liveness concepts, integrating continuous testing into IDEs to verify object compatibility and compliance, thereby identifying runtime errors dynamically.
Contribution
It presents a new method combining liveness-based verification with IDE integration for concurrent object languages, focusing on runtime error detection and formal duality of testing types.
Findings
Effective IDE support for runtime error reflection
Compatibility and compliance testing integrated into development
Discussion of challenges and future opportunities
Abstract
We explore the use of liveness for interactive program verification for a simple concurrent object language. Our experimental IDE integrates two (formally dual) kinds of continuous testing into the development environment: compatibility-checking, which verifies an object's use of other objects, and compliance-checking, which verifies an object's claim to refine the behaviour of another object. Source code errors highlighted by the IDE are not static type errors but the reflection back to the source of runtime errors that occur in some execution of the system. We demonstrate our approach, and discuss opportunities and challenges.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Testing and Debugging Techniques · Formal Methods in Verification · Logic, programming, and type systems
