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
- Sun 9 - Tue 18 Aug 2020CuriousU 2020 (CANCELLED)
- Thu 27 Aug 2020 15:00 - 16:30The 2020 TechMed Event: Kick-off meeting
- Mon 31 Aug 2020Opening Academic Year (OAY) on UTour
- Tue 8 Sep 2020 17:15 - 19:00Pioneers In HealthCare: Matchmaking event
- Sun 20 - Thu 24 Sep 2020SEFI annual conference online