Sebastiaan J. C. Joosten
ABSTRACT
Society nowadays relies heavily on software, which makes verifying the correctness of software crucially important. Various verification tools have been proposed for this purpose, each focusing on a limited set of tasks, as there are many different ways to build and reason about software. This paper discusses two case studies from the VerifyThis2018 verification competition, worked out using the VerCors verification toolset. These case studies are sequential, while VerCors specialises in reasoning about parallel and concurrent software. This paper elaborates on our experiences of using VerCors to verify sequential programs. The first case study involves specifying and verifying the behaviour of a gap buffer; a data-structure commonly used in text editors. The second case study involves verifying a combinatorial problem based on Project Euler problem #114. We find that VerCors is well capable of reasoning about sequential software, and that certain techniques to reason about concurrency can help to reason about sequential programs. However, the extra annotations required to reason about concurrency bring some specificational overhead.
- Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias Ulbrich. 2016. Deductive Software Verification - The KeY Book. Lecture Notes in Computer Science, Vol. 10001. Springer International Publishing.Google Scholar
- A. Amighi, S. Blom, and M. Huisman. 2014. Resource Protection Using Atomics - Patterns and Verification. In APLAS. 255--274.Google Scholar
- A. Amighi, S. Blom, and M. Huisman. 2016. VerCors: A Layered Approach to Practical Verification of Concurrent Software. In PDP. 495--503.Google Scholar
- A. Amighi, C. Haack, M. Huisman, and C. Hurlin. 2015. Permission-based separation logic for multithreaded Java programs. LMCS 11, 1 (2015).Google Scholar
- Afshin Amighi, Marieke Huisman, Stefan Blom, Saddek Bensalem, and Simon Bliudze. 2018. Verification of Shared-Reading Synchronisers. In 1st International Workshop on Methods and Tools for Rigorous System Design 2018.Google Scholar
- S. Blom, S. Darabi, M. Huisman, and W. Oortwijn. 2017. The VerCors Tool Set: Verification of Parallel and Concurrent Software. In iFM (LNCS), Vol. 10510. Springer, 102--110.Google Scholar
- Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Dominik Haneberg, and Wolfgang Reif. 2015. KIV: overview and VerifyThis competition. STTT 17, 6 (01 Nov 2015), 677--694. Google ScholarDigital Library
- Jean-Christophe Filliâtre and Andrei Paskevich. 2013. Why3 --- Where Programs Meet Provers. In ESOP (LNCS), Matthias Felleisen and Philippa Gardner (Eds.), Vol. 7792. Springer, 125--128. Google ScholarDigital Library
- Marieke Huisman, Vladimir Klebanov, and Rosemary Monahan (Eds.). 2015. VerifyThis 2012 - A Program Verification Competition (STTT). Vol. 17. Issue 6. Google ScholarDigital Library
- B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx, and F. Piessens. 2011. VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In NFM. Google ScholarDigital Library
- P. Müller, M. Schwerhoff, and A.J. Summers. 2016. Viper - A Verification Infrastructure for Permission-Based Reasoning. In VMCAI. Google ScholarDigital Library
- W. Oortwijn, S. Blom, D. Gurov, M. Huisman, and M. Zaharieva-Stojanovski. 2017. An Abstraction Technique for Describing Concurrent Program Behaviour. In VSTTE (LNCS), Vol. 10712. 191--209.Google Scholar
- Julian Tschannen, Carlo A. Furia, Martin Nordio, and Nadia Polikar-pova. 2015. AutoProof: Auto-active Functional Verification of Object-oriented Programs. In TACAS (LNCS). Springer. Google ScholarDigital Library
- An exercise in verifying sequential programs with VerCors
Recommendations
Efficient Verification of Sequential and Concurrent C Programs
There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...
Verifying functional correctness of C programs with VCC
NFM'11: Proceedings of the Third international conference on NASA Formal methodsVCC [2] is an industrial-strength verification environment for low-level concurrent systems code written in C. VCC takes a program (annotated with function contracts, state assertions, and type invariants) and attempts to prove the correctness of these ...
Comments