Cached Verification: Haskell implementation of a verification splitter By Sebastiaan Josten

A non-interactive verifier like VerCors or OpenJML, will let users spend considerable time waiting to see if everything still verifies. We build a preprocessor for such tools that slices a single file into several independently verifiable files, calls the verifier in parallel, and caches the results. We call our tool SplitVerify. SplitVerify uses dependency analysis and whitespace/comment reduction, to increase the chance that the verification of a part of the project is cached. The tool is built using Haskell, using a bidirectional semi-language-agnostic parser and generic programming to keep SplitVerify lightweight and maintainable. As of today, SplitVerify uses only 752 lines of code (counted with cloc).