An Exercise in Verifying Sequential Programs with VerCors

Sebastiaan Jozef Christiaan Joosten, Wytse Oortwijn, Mohsen Safari, Marieke Huisman

    Research output: Contribution to conferencePaperAcademicpeer-review

    3 Citations (Scopus)
    68 Downloads (Pure)

    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. Interestingly, 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.
    Original languageEnglish
    Number of pages6
    Publication statusPublished - 16 Jul 2018
    Event20th Workshop on Formal Techniques for Java-like Programs Formal techniques: FTfJP 2018 with ECOOP and ISSTA - Amsterdam, Netherlands
    Duration: 16 Jul 201821 Jul 2018
    Conference number: 20
    https://conf.researchr.org/track/FTfJP-2018/FTfJP-2018-papers

    Conference

    Conference20th Workshop on Formal Techniques for Java-like Programs Formal techniques
    Abbreviated titleFTfJP 2018
    CountryNetherlands
    CityAmsterdam
    Period16/07/1821/07/18
    Internet address

    Fingerprint

    File editors
    Data structures

    Cite this

    Joosten, S. J. C., Oortwijn, W., Safari, M., & Huisman, M. (2018). An Exercise in Verifying Sequential Programs with VerCors. Paper presented at 20th Workshop on Formal Techniques for Java-like Programs Formal techniques, Amsterdam, Netherlands.
    Joosten, Sebastiaan Jozef Christiaan ; Oortwijn, Wytse ; Safari, Mohsen ; Huisman, Marieke . / An Exercise in Verifying Sequential Programs with VerCors. Paper presented at 20th Workshop on Formal Techniques for Java-like Programs Formal techniques, Amsterdam, Netherlands.6 p.
    @conference{4396dc60b4b54016b4684394c8b557d4,
    title = "An Exercise in Verifying Sequential Programs with VerCors",
    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. Interestingly, 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.",
    author = "Joosten, {Sebastiaan Jozef Christiaan} and Wytse Oortwijn and Mohsen Safari and Marieke Huisman",
    year = "2018",
    month = "7",
    day = "16",
    language = "English",
    note = "20th Workshop on Formal Techniques for Java-like Programs Formal techniques : FTfJP 2018 with ECOOP and ISSTA, FTfJP 2018 ; Conference date: 16-07-2018 Through 21-07-2018",
    url = "https://conf.researchr.org/track/FTfJP-2018/FTfJP-2018-papers",

    }

    Joosten, SJC, Oortwijn, W, Safari, M & Huisman, M 2018, 'An Exercise in Verifying Sequential Programs with VerCors' Paper presented at 20th Workshop on Formal Techniques for Java-like Programs Formal techniques, Amsterdam, Netherlands, 16/07/18 - 21/07/18, .

    An Exercise in Verifying Sequential Programs with VerCors. / Joosten, Sebastiaan Jozef Christiaan; Oortwijn, Wytse; Safari, Mohsen ; Huisman, Marieke .

    2018. Paper presented at 20th Workshop on Formal Techniques for Java-like Programs Formal techniques, Amsterdam, Netherlands.

    Research output: Contribution to conferencePaperAcademicpeer-review

    TY - CONF

    T1 - An Exercise in Verifying Sequential Programs with VerCors

    AU - Joosten, Sebastiaan Jozef Christiaan

    AU - Oortwijn, Wytse

    AU - Safari, Mohsen

    AU - Huisman, Marieke

    PY - 2018/7/16

    Y1 - 2018/7/16

    N2 - 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. Interestingly, 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.

    AB - 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. Interestingly, 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.

    M3 - Paper

    ER -

    Joosten SJC, Oortwijn W, Safari M, Huisman M. An Exercise in Verifying Sequential Programs with VerCors. 2018. Paper presented at 20th Workshop on Formal Techniques for Java-like Programs Formal techniques, Amsterdam, Netherlands.