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).
Thursday 19 December 2019 15:45 - 16:30
More events
- Tue 28 Oct 2025 19:30 - 21:00Nobel Lectures
- Wed 29 Oct 2025 12:30 - 13:30Infosession parttime programme Leadership for the Future
- Mon 3 Nov 2025 12:00 - 13:00Infosession parttime programme Digital Design & Architecture
- Tue 4 Nov 2025 19:30 - 21:00From shivering to sweating - the science behind body temperature
- Wed 5 Nov 2025Climate Event 2025