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
- Fri 26 Apr 2024 09:30 - 17:00Competing with Digital Servitization
- Wed 8 - Wed 15 May 2024Erasmus+ Inspire Days
- Wed 8 May 2024 20:00 - 22:00Lecture in Twents, there's nothing wrong with that!
- Tue 21 May 2024 12:45 - 14:00Week of Inspiration / Lecture & concert: To the end of the world
- Tue 21 May 2024 19:30 - 21:00Week of inspiration / Wanted: climate optimists!