A Vision for Online Verification-Validation
Matthew A. Hammer, Bor-Yuh Evan Chang, David Van Horn

TL;DR
This paper introduces online verification-validation (OVV), a novel approach that combines static and dynamic analysis in a unified, phaseless manner to improve correctness guarantees in extensible dynamic languages.
Contribution
It proposes a new language and VM design enabling continuous, interleaved analysis and execution, allowing progressive verification of program components.
Findings
Implemented OVV semantics in Rust demonstrating progressive typing.
Showed OVV enables verification without traditional static/dynamic phase separation.
Presented a gradual type system integrated with OVV for extensible libraries.
Abstract
Today's programmers face a false choice between creating software that is extensible and software that is correct. Specifically, dynamic languages permit software that is richly extensible (via dynamic code loading, dynamic object extension, and various forms of reflection), and today's programmers exploit this flexibility to "bring their own language features" to enrich extensible languages (e.g., by using common JavaScript libraries). Meanwhile, such library-based language extensions generally lack enforcement of their abstractions, leading to programming errors that are complex to avoid and predict. To offer verification for this extensible world, we propose online verification-validation (OVV), which consists of language and VM design that enables a "phaseless" approach to program analysis, in contrast to the standard static-dynamic phase distinction. Phaseless analysis freely…
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 · Logic, programming, and type systems · Software Engineering Research
