@InProceedings{10.1007/978-3-031-77382-2_1,
author="Herber, Paula
and Adelt, Julius
and Tasche, Philip",
editor="Madeira, Alexandre
and Knapp, Alexander",
title="Formal Verification of Cyber-Physical Systems Using Domain-Specific Abstractions",
booktitle="Software Engineering and Formal Methods",
year="2025",
publisher="Springer Nature Switzerland",
address="Cham",
pages="3--21",
abstract="Cyber-physical systems have become ubiquitous in our daily lives, and their complexity continually evolves to unprecedented levels. In addition to their heterogeneity and interaction with a physical environment, we see a tremendous increase in the use of learning to make autonomous decisions in dynamic environments. These developments pose significant challenges for ensuring safety and resilience of cyber-physical systems. Formal methods have the potential to guarantee such properties under all circumstances. However, they are expensive and severely suffer from scalability issues. To improve scalability and applicability of formal methods, it is highly desirable to exploit domain-specific knowledge. In this paper, we summarize some of our recent efforts towards reusable specification and more scalable verification of cyber-physical systems using domain-specific abstractions.  In particular, we present our ideas to use domain-specific abstractions to provide 1) reusable semantics encodings that enable us to automatically transform domain-specific system design languages such as SystemC or Simulink into a formal representation, and 2) reusable specification mechanisms for contracts and invariants that can be used for deductive verification of safety and resilience of reactive, hybrid, and learning systems. We discuss promising results and open problems, and identify challenges for future work.",
isbn="978-3-031-77382-2"
}

Cyber-physical systems have become ubiquitous in our daily lives, and their complexity continually evolves to unprecedented levels. In addition to their heterogeneity and interaction with a physical environment, we see a tremendous increase in the use of learning to make autonomous decisions in dynamic environments. These developments pose significant challenges for ensuring safety and resilience of cyber-physical systems. Formal methods have the potential to guarantee such properties under all circumstances. However, they are expensive and severely suffer from scalability issues. To improve scalability and applicability of formal methods, it is highly desirable to exploit domain-specific knowledge. In this paper, we summarize some of our recent efforts towards reusable specification and more scalable verification of cyber-physical systems using domain-specific abstractions.  In particular, we present our ideas to use domain-specific abstractions to provide 1) reusable semantics encodings that enable us to automatically transform domain-specific system design languages such as SystemC or Simulink into a formal representation, and 2) reusable specification mechanisms for contracts and invariants that can be used for deductive verification of safety and resilience of reactive, hybrid, and learning systems. We discuss promising results and open problems, and identify challenges for future work.

@InProceedings{10.1007/978-3-031-77382-2_23,
author="Tasche, Philip
and Herber, Paula
and Huisman, Marieke",
editor="Madeira, Alexandre
and Knapp, Alexander",
title="Automated Invariant Generation for Efficient Deductive Reasoning About Embedded Systems",
booktitle="Software Engineering and Formal Methods",
year="2024",
publisher="Springer Nature Switzerland",
address="Cham",
pages="404--422",
abstract="Deductive verification is often more efficient than alternative techniques like model checking at reasoning about functional properties of programs. This is especially true when the program under verification contains very large or unbounded data ranges that model checkers struggle with. However, modular deductive verifiers struggle with verifying global properties, which are often crucial in concurrent and reactive embedded systems. Embedded systems often require complex user-defined invariants to capture the global state for the verification of local annotations, demanding high effort and expertise from the user. In this paper, we propose a method to automatically generate compact invariants that are sufficiently strong to enable effective deductive verification of global properties in embedded systems. Our key idea is that a good level of abstraction can be found automatically by choosing variables for refinement that influence relevant events and process interactions. We use this idea together with abstract interpretation to build a system's state space, abstracted to the relevant part for a given global property. We demonstrate the effectiveness of our approach on a SystemC design of an automotive control system that has in the past proved challenging to verify.",
isbn="978-3-031-77382-2"
}

Deductive verification is often more efficient than alternative techniques like model checking at reasoning about functional properties of programs. This is especially true when the program under verification contains very large or unbounded data ranges that model checkers struggle with. However, modular deductive verifiers struggle with verifying global properties, which are often crucial in concurrent and reactive embedded systems. Embedded systems often require complex user-defined invariants to capture the global state for the verification of local annotations, demanding high effort and expertise from the user. In this paper, we propose a method to automatically generate compact invariants that are sufficiently strong to enable effective deductive verification of global properties in embedded systems. Our key idea is that a good level of abstraction can be found automatically by choosing variables for refinement that influence relevant events and process interactions. We use this idea together with abstract interpretation to build a system's state space, abstracted to the relevant part for a given global property. We demonstrate the effectiveness of our approach on a SystemC design of an automotive control system that has in the past proved challenging to verify.

@InProceedings{10.1007/978-3-031-76554-4_12,
author="Rubbens, Robert
and Bos, Petra van den
and Huisman, Marieke",
editor="Kosmatov, Nikolai
and Kov{\'a}cs, Laura",
title="VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory",
booktitle="Integrated Formal Methods",
year="2024",
publisher="Springer Nature Switzerland",
address="Cham",
pages="217--236",
abstract="In the VeyMont tool, choreographies can be used to specify concurrent programs using a sequential format. To support choreography-based development, VeyMont verifies a given choreography for functional correctness and memory safety, and subsequently generates a correct concurrent program. However, the initial version of VeyMont did not support programs with shared memory. This paper shows how we overcome this limitation, by adding support for ownership annotations to VeyMont. Moreover, we also adapted the concurrent program generation, so that it does not only generate code, but also annotations. As a result, further changes and optimizations of the concurrent program can directly be verified. We demonstrate the extended capabilities of VeyMont on illustrative case studies.",
isbn="978-3-031-76554-4"
}

In the VeyMont tool, choreographies can be used to specify concurrent programs using a sequential format. To support choreography-based development, VeyMont verifies a given choreography for functional correctness and memory safety, and subsequently generates a correct concurrent program. However, the initial version of VeyMont did not support programs with shared memory. This paper shows how we overcome this limitation, by adding support for ownership annotations to VeyMont. Moreover, we also adapted the concurrent program generation, so that it does not only generate code, but also annotations. As a result, further changes and optimizations of the concurrent program can directly be verified. We demonstrate the extended capabilities of VeyMont on illustrative case studies.

@InProceedings{10.1007/978-3-031-77382-2_11,
author="Wittingen, Ellen
and Huisman, Marieke
and {\c{S}}akar, {\"O}mer",
editor="Madeira, Alexandre
and Knapp, Alexander",
title="Deductive Verification of SYCL in VerCors",
booktitle="Software Engineering and Formal Methods",
year="2024",
publisher="Springer Nature Switzerland",
address="Cham",
pages="182--199",
abstract="SYCL is a C++ programming model for the development of heterogeneous programs. It uses the concept of kernels, where multiple instances of a computation are executed concurrently on a computing unit. This concurrency entails that the set of possible program behaviours can be of considerable size, which makes these programs error-prone. Formal verification could be used to ensure the correctness of all these possible program behaviours. However, there exist no formal verification tools for SYCL.",
isbn="978-3-031-77382-2"
}

SYCL is a C++ programming model for the development of heterogeneous programs. It uses the concept of kernels, where multiple instances of a computation are executed concurrently on a computing unit. This concurrency entails that the set of possible program behaviours can be of considerable size, which makes these programs error-prone. Formal verification could be used to ensure the correctness of all these possible program behaviours. However, there exist no formal verification tools for SYCL.

@InProceedings{Haak24FMICS,
author="van den Haak, Lars B.
and Wijs, Anton
and Huisman, Marieke
and van den Brand, Mark",
editor="Haxthausen, Anne E.
and Serwe, Wendelin",
title="Verifying a Radio Telescope Pipeline Using HaliVer: Solving Nonlinear and Quantifier Challenges",
booktitle="Formal Methods for Industrial Critical Systems",
year="2024",
publisher="Springer Nature Switzerland",
address="Cham",
pages="152--169",
abstract="This paper describes a case study to verify memory safety of a radio telescope pipeline, which was targeted with the PADRE project of Astron, SURF and the Netherlands eScienceCenter. As performance is important for this application, the implementation of the radio telescope pipeline should run on a GPU device. Therefore, we encoded the radio telescope pipeline using the Halide scheduling language, which achieved a significant speedup. Next, we used the HaliVer tool to automatically generate formal pre- and postconditions, loop invariants and assertions, which the deductive verifier VerCors can use to prove memory safety. We identified two challenges for the automatic generation of formal annotations for a tool such as VerCors. The first challenge was related to the flattening of multi-dimensional arrays to single arrays and the second challenge concerns the use of many arrays in a program in combination with many quantifiers to specify read and write permissions. For both challenges, we propose solutions, and implemented these. Not every solution proved successful. We discuss the lessons learned and future plans to solve a core scalability issue for large optimised parallel programs.",
isbn="978-3-031-68150-9",
doi="10.1007/978-3-031-68150-9_9"
}

This paper describes a case study to verify memory safety of a radio telescope pipeline, which was targeted with the PADRE project of Astron, SURF and the Netherlands eScienceCenter. As performance is important for this application, the implementation of the radio telescope pipeline should run on a GPU device. Therefore, we encoded the radio telescope pipeline using the Halide scheduling language, which achieved a significant speedup. Next, we used the HaliVer tool to automatically generate formal pre- and postconditions, loop invariants and assertions, which the deductive verifier VerCors can use to prove memory safety. We identified two challenges for the automatic generation of formal annotations for a tool such as VerCors. The first challenge was related to the flattening of multi-dimensional arrays to single arrays and the second challenge concerns the use of many arrays in a program in combination with many quantifiers to specify read and write permissions. For both challenges, we propose solutions, and implemented these. Not every solution proved successful. We discuss the lessons learned and future plans to solve a core scalability issue for large optimised parallel programs.

@InProceedings{Armborst24,
author="Armborst, Lukas
and Bos, Pieter
and van den Haak, Lars B.
and Huisman, Marieke
and Rubbens, Robert
and {\c{S}}akar, {\"O}mer
and Tasche, Philip",
editor="Gurfinkel, Arie
and Ganesh, Vijay",
title="The VerCors Verifier: A Progress Report",
booktitle="Computer Aided Verification",
year="2024",
publisher="Springer Nature Switzerland",
address="Cham",
pages="3--18",
abstract="This paper gives an overview of the most recent developments on the VerCors verifier. VerCors is a deductive verifier for concurrent software, written in multiple programming languages, where the specifications are written in terms of pre-/postcondition contracts using permission-based separation logic. In essence, VerCors is a program transformation tool: it translates an annotated program into input for the Viper framework, which is then used as verification back-end. The paper discusses the different programming languages and features for which VerCors provides verification support. It also discusses how the tool internally has been reorganised to become easily extendible, and to improve the connection and interaction with Viper. In addition, we also introduce two tools built on top of VerCors, which support correctness-preserving transformations of verified programs. Finally, we discuss how the VerCors verifier has been used on a range of realistic case studies.",
isbn="978-3-031-65630-9",
doi="10.1007/978-3-031-65630-9_1"
}

This paper gives an overview of the most recent developments on the VerCors verifier. VerCors is a deductive verifier for concurrent software, written in multiple programming languages, where the specifications are written in terms of pre-/postcondition contracts using permission-based separation logic. In essence, VerCors is a program transformation tool: it translates an annotated program into input for the Viper framework, which is then used as verification back-end. The paper discusses the different programming languages and features for which VerCors provides verification support. It also discusses how the tool internally has been reorganised to become easily extendible, and to improve the connection and interaction with Viper. In addition, we also introduce two tools built on top of VerCors, which support correctness-preserving transformations of verified programs. Finally, we discuss how the VerCors verifier has been used on a range of realistic case studies.

@inproceedings{Haak24,
title = "HaliVer: Deductive Verification and Scheduling Languages Join Forces",
abstract = "The HALIVER tool integrates deductive verification into the popular scheduling language HALIDE, used for image processing pipelines and array computations. HALIVER uses VERCORS, a separation logic-based verifier, to verify the correctness of (1) the HALIDE algorithms and (2) the optimised parallel code produced by HALIDE when an optimisation schedule is applied to an algorithm. This allows proving complex, optimised code correct while reducing the effort to provide the required verification annotations. For both approaches, the same specification is used. We evaluated the tool on several optimised programs generated from characteristic HALIDE algorithms, using all but one of the essential scheduling directives available in HALIDE. Without annotation effort, HALIVER proves memory safety in almost all programs. With annotations HALIVER, additionally, proves functional correctness properties. We show that the approach is viable and reduces the manual annotation effort by an order of magnitude.",
keywords = "2024 OA procedure",
author = "{van den Haak}, Lars and Anton Wijs and Marieke Huisman and {van den Brand}, Mark",
year = "2024",
month = apr,
day = "5",
doi = "10.1007/978-3-031-57256-2_4",
language = "English",
isbn = "978-3-031-57255-5",
pages = "71--89",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
note = "30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, TACAS 2024 ; Conference date: 06-04-2024 Through 11-04-2024",

}

The HALIVER tool integrates deductive verification into the popular scheduling language HALIDE, used for image processing pipelines and array computations. HALIVER uses VERCORS, a separation logic-based verifier, to verify the correctness of (1) the HALIDE algorithms and (2) the optimised parallel code produced by HALIDE when an optimisation schedule is applied to an algorithm. This allows proving complex, optimised code correct while reducing the effort to provide the required verification annotations. For both approaches, the same specification is used. We evaluated the tool on several optimised programs generated from characteristic HALIDE algorithms, using all but one of the essential scheduling directives available in HALIDE. Without annotation effort, HALIVER proves memory safety in almost all programs. With annotations HALIVER, additionally, proves functional correctness properties. We show that the approach is viable and reduces the manual annotation effort by an order of magnitude.

@inproceedings{Oorschot24,
title = "First Steps towards Deductive Verification of LLVM IR",
abstract = "Over the last years, deductive program verifiers have substantially improved, and their applicability on non-trivial applications has been demonstrated. However, a major bottleneck is that for every new programming language, a new deductive verifier has to be built.This paper describes the first steps in a project that aims to address this problem, by language-agnostic support for deductive verification: Rather than building a deductive program verifier for every programming language, we develop deductive program verification technology for a widely-used intermediate representation language (LLVM IR), such that we eventually get verification support for any language that can be compiled into the LLVM IR format.Concretely, this paper describes the design of VCLLVM, a prototype tool that adds LLVM IR as a supported language to the VerCors verifier. We discuss the challenges that have to be addressed to develop verification support for such a low-level language. Moreover, we also sketch how we envisage to build verification support for any specified source program that can be compiled into LLVM IR on top of VCLLVM.",
keywords = "2024 OA procedure",
author = "{van Oorschot}, Dr{\'e} and Huisman, Marieke and {\c{S}}akar, {\"O}mer",
year = "2024",
month = apr,
day = "6",
doi = "10.1007/978-3-031-57259-3_15",
language = "English",
isbn = "978-3-031-57258-6",
series = "Lecture Notes in Computer Science",
pages = "290--303",
editor = "Dirk Beyer and Ana Cavalcanti",
booktitle = "Fundamental Approaches to Software Engineering",
note = "27th International Conference on Fundamental Approaches to Software Engineering, FASE 2024, FASE ; Conference date: 06-04-2024 Through 11-04-2024",

}

Over the last years, deductive program verifiers have substantially improved, and their applicability on non-trivial applications has been demonstrated. However, a major bottleneck is that for every new programming language, a new deductive verifier has to be built.This paper describes the first steps in a project that aims to address this problem, by language-agnostic support for deductive verification: Rather than building a deductive program verifier for every programming language, we develop deductive program verification technology for a widely-used intermediate representation language (LLVM IR), such that we eventually get verification support for any language that can be compiled into the LLVM IR format.Concretely, this paper describes the design of VCLLVM, a prototype tool that adds LLVM IR as a supported language to the VerCors verifier. We discuss the challenges that have to be addressed to develop verification support for such a low-level language. Moreover, we also sketch how we envisage to build verification support for any specified source program that can be compiled into LLVM IR on top of VCLLVM.

@InProceedings{Tasche24,
author="Tasche, Philip
and Monti, Ra{\'u}l E.
and Drerup, Stefanie Eva
and Blohm, Pauline
and Herber, Paula
and Huisman, Marieke",
editor="Dimitrova, Rayna
and Lahav, Ori
and Wolff, Sebastian",
title="Deductive Verification of Parameterized Embedded Systems Modeled in SystemC",
booktitle="Verification, Model Checking, and Abstract Interpretation",
year="2024",
publisher="Springer Nature Switzerland",
address="Cham",
pages="187--209",
abstract="Major strengths of deductive verification include modular verification and support for functional properties and unbounded parameters. However, in embedded systems, crucial safety properties often depend on concurrent process interactions, events, and time. Such properties are global in nature and thus difficult to verify in a modular fashion. Furthermore, the execution and scheduling semantics of industrially used embedded system design languages such as SystemC are typically only informally defined. In this paper, we propose a deductive verification approach for embedded systems that are modeled with SystemC. Our main contribution is twofold: 1) We provide a formal encoding and an automated transformation of SystemC designs for verification with the VerCors deductive verifier. 2) We present a novel approach for invariant construction to abstractly capture global dependencies. Our encoding enables an automated formalization and deductive verification of parameterized SystemC designs, and the invariant construction enables local reasoning about global properties with comparatively low manual effort. We demonstrate the applicability of our approach on three parameterized case studies, including an automotive control system.",
isbn="978-3-031-50521-8"
}

Major strengths of deductive verification include modular verification and support for functional properties and unbounded parameters. However, in embedded systems, crucial safety properties often depend on concurrent process interactions, events, and time. Such properties are global in nature and thus difficult to verify in a modular fashion. Furthermore, the execution and scheduling semantics of industrially used embedded system design languages such as SystemC are typically only informally defined. In this paper, we propose a deductive verification approach for embedded systems that are modeled with SystemC. Our main contribution is twofold: 1) We provide a formal encoding and an automated transformation of SystemC designs for verification with the VerCors deductive verifier. 2) We present a novel approach for invariant construction to abstractly capture global dependencies. Our encoding enables an automated formalization and deductive verification of parameterized SystemC designs, and the invariant construction enables local reasoning about global properties with comparatively low manual effort. We demonstrate the applicability of our approach on three parameterized case studies, including an automotive control system.

@article{Lathouwers24,
title = {Survey of annotation generators for deductive verifiers},
journal = {Journal of Systems and Software},
volume = {211},
pages = {111972},
year = {2024},
issn = {0164-1212},
doi = {https://doi.org/10.1016/j.jss.2024.111972},
url = {https://www.sciencedirect.com/science/article/pii/S0164121224000153},
author = {Sophie Lathouwers and Marieke Huisman},
keywords = {Deductive verification, Specifications, Annotations, Specification inference, Specification generation, Survey},
abstract = {Deductive verifiers require intensive user interaction in the form of writing precise specifications, thereby limiting their use in practice. While many solutions have been proposed to generate specifications, their evaluations and comparisons to other tools are limited. As a result, it is unclear what the best approaches for specification inference are and how these impact the overall specification writing process. In this paper we take steps to address this problem by providing an overview of specification inference tools that can be used for deductive verification of Java programs. For each tool, we discuss its approach to specification inference and identify its advantages and disadvantages. Moreover, we identify the types of specifications that it infers and use this to estimate the impact of the tool on the overall specification writing process. Finally, we identify the ideal features of a specification generator and discuss important challenges for future research.}
}

Deductive verifiers require intensive user interaction in the form of writing precise specifications, thereby limiting their use in practice. While many solutions have been proposed to generate specifications, their evaluations and comparisons to other tools are limited. As a result, it is unclear what the best approaches for specification inference are and how these impact the overall specification writing process. In this paper we take steps to address this problem by providing an overview of specification inference tools that can be used for deductive verification of Java programs. For each tool, we discuss its approach to specification inference and identify its advantages and disadvantages. Moreover, we identify the types of specifications that it infers and use this to estimate the impact of the tool on the overall specification writing process. Finally, we identify the ideal features of a specification generator and discuss important challenges for future research.

@phdthesis{Lathouwers23,
  title = "Exploring annotations for deductive verification",
  author = "Sophie Lathouwers",
  year = "2023",
  month = oct,
  day = "17",
  doi = "10.3990/1.9789036558464",
  isbn = "978-90-365-5845-7",
  series = "DSI Ph.D. Thesis Series",
  publisher = "University of Twente",
  number = "23-009",
  address = "Netherlands",
  school = "University of Twente",
  url={https://research.utwente.nl/files/320453422/Dissertation-Lathouwers-with-cover-and-clickable-links.pdf}
}

@inproceedings{ArmborstH23,
  author       = {Lukas Armborst and
                  Sophie Lathouwers and
                  Marieke Huisman},
  editor       = {Paula Herber and
                  Anton Wijs},
  title        = {Joining Forces! Reusing Contracts for Deductive Verifiers Through
                  Automatic Translation},
  booktitle    = {iFM 2023 - 18th International Conference, iFM 2023, Leiden, The Netherlands,
                  November 13-15, 2023, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {14300},
  pages        = {153--171},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-47705-8\_9},
  doi          = {10.1007/978-3-031-47705-8\_9}
}

@inproceedings{Bliudze2023,
AUTHOR = {Bliudze, Simon and van den Bos, Petra and Huisman, Marieke and Rubbens, Robert and Safina, Larisa},
TITLE = {{JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java}},
URL = {https://hal.inria.fr/hal-03911393},
BOOKTITLE = {{26th International Conference on Fundamental Approaches to Software Engineering}},
address="Cham",
YEAR = {2023},
MONTH = Apr,
url={https://hal.inria.fr/hal-03911393/file/javabip-meets-vercors-submitted-draft-2022-10-21.pdf}
}

@InProceedings{Monti2022,
author="Monti, Ra{\'u}l E.
and Rubbens, Robert
and Huisman, Marieke",
editor="Margaria, Tiziana
and Steffen, Bernhard",
title="On Deductive Verification of an Industrial Concurrent Software Component with VerCors",
booktitle="Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles",
year="2022",
publisher="Springer International Publishing",
address="Cham",
pages="517--534",
isbn="978-3-031-19849-6"
}

@incollection{vandenBos2022,
author="van den Bos, Petra
and Huisman, Marieke",
editor="Jansen, Nils
and Stoelinga, Mari{\"e}lle
and van den Bos, Petra",
title="The Integration of Testing and Program Verification",
booktitle="A Journey from Process Algebra via Timed Automata to Model Learning : Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday",
year="2022",
publisher="Springer Nature Switzerland",
address="Cham",
pages="524--538",
doi="10.1007/978-3-031-15629-8_28",
url="https://doi.org/10.1007/978-3-031-15629-8_28"
}

@inproceedings{Lathouwers2022,
author = {Lathouwers, Sophie and Huisman, Marieke},
title = {Formal Specifications Investigated: A Classification and Analysis of Annotations for Deductive Verifiers},
year = {2022},
isbn = {9781450392877},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3524482.3527652},
doi = {10.1145/3524482.3527652},
pages = {69–79},
numpages = {11},
keywords = {annotations, taxonomy, specifications, deductive verification, auto-active verification},
location = {Pittsburgh, Pennsylvania},
series = {FormaliSE '22}
}

@phdthesis{Safari2022b,
title = "Correct Optimized GPU Programs",
author = "Mohsen Safari",
year = "2022",
month = apr,
day = "5",
doi = "10.3990/1.9789036553421",
language = "English",
isbn = "978-90-365-5342-1",
series = "DSI Ph.D. thesis series",
publisher = "University of Twente",
number = "22-003",
address = "Netherlands",
school = "University of Twente",
}

@article{Safari2022,
title = {Formal verification of parallel prefix sum and stream compaction algorithms in CUDA},
journal = {Theoretical Computer Science},
volume = {912},
pages = {81-98},
year = {2022},
issn = {0304-3975},
doi = {https://doi.org/10.1016/j.tcs.2022.02.027},
url = {https://www.sciencedirect.com/science/article/pii/S0304397522001232},
author = {Mohsen Safari and Marieke Huisman},
keywords = {GPU verification, CUDA, Deductive verification, Separation logic, Prefix sum, Stream compaction}
}

@InProceedings{Sakar2022,
author="{\c{S}}akar, {\"O}mer
and Safari, Mohsen
and Huisman, Marieke
and Wijs, Anton",
editor="Fisman, Dana
and Rosu, Grigore",
title="Alpinist: An Annotation-Aware GPU Program Optimizer",
booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
year="2022",
publisher="Springer International Publishing",
address="Cham",
pages="332--352",
isbn="978-3-030-99527-0",
url="https://link.springer.com/chapter/10.1007/978-3-030-99527-0_18"
}

@InProceedings{Sung2022,
author="Jongmans, Sung-Shik
and van den Bos, Petra",
editor="Sergey, Ilya",
title="A Predicate Transformer for Choreographies",
booktitle="Programming Languages and Systems",
year="2022",
publisher="Springer International Publishing",
address="Cham",
pages="520--547",
isbn="978-3-030-99336-8",
url="https://link.springer.com/chapter/10.1007/978-3-030-99336-8_19"
}

@misc{Hollander2021,
  month = {August},
  title = {Verification of a model checking algorithm in VerCors},
  year = {2021},
  author = {J.P. {Hollander}},
  url = {http://essay.utwente.nl/88268/},
}

@misc{Sleurink2021,
  month = {June},
  year = {2021},
  author = {Matthias {Sleurink}},
  title = {Automatic Generation of Test Cases for VerCors Verification Cases Failing with Null Errors},
  url = {http://essay.utwente.nl/86828/},
}

@misc{Bos2021,
  title = {Program verification for quantum algorithms},
  author = {P. {Bos}},
  year = {2021},
  month = {June},
  url = {http://essay.utwente.nl/86508/}
}

@inproceedings{HuismanM21,
  author    = {Marieke Huisman and
               Ra{\'{u}}l E. Monti},
  title     = {Teaching Design by Contract using Snap!},
  booktitle = {3rd International Workshop on Software Engineering Education for the
               Next Generation, SEENG@ICSE 2021, Madrid, Spain, May 24, 2021},
  pages     = {1--5},
  publisher = {{IEEE}},
  year      = {2021},
  url       = {https://doi.org/10.1109/SEENG53126.2021.00007},
  doi       = {10.1109/SEENG53126.2021.00007},
  timestamp = {Thu, 14 Oct 2021 09:56:38 +0200},
  biburl    = {https://dblp.org/rec/conf/icse-seeng/HuismanM21.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{BlomDHS21,
  author    = {Stefan Blom and
               Saeed Darabi and
               Marieke Huisman and
               Mohsen Safari},
  title     = {Correct program parallelisations},
  journal   = {Int. J. Softw. Tools Technol. Transf.},
  volume    = {23},
  number    = {5},
  pages     = {741--763},
  year      = {2021},
  url       = {https://doi.org/10.1007/s10009-020-00601-z},
  doi       = {10.1007/s10009-020-00601-z},
  timestamp = {Wed, 01 Dec 2021 08:54:11 +0100},
  biburl    = {https://dblp.org/rec/journals/sttt/BlomDHS21.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{RubbensLH21,
  author    = {Robert Rubbens and
               Sophie Lathouwers and
               Marieke Huisman},
  editor    = {Alberto Lluch{-}Lafuente and
               Anastasia Mavridou},
  title     = {Modular Transformation of Java Exceptions Modulo Errors},
  booktitle = {Formal Methods for Industrial Critical Systems - 26th International
               Conference, {FMICS} 2021, Paris, France, August 24-26, 2021, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {12863},
  pages     = {67--84},
  publisher = {Springer},
  year      = {2021},
  url       = {https://doi.org/10.1007/978-3-030-85248-1\_5},
  doi       = {10.1007/978-3-030-85248-1\_5},
  timestamp = {Wed, 01 Sep 2021 12:53:45 +0200},
  biburl    = {https://dblp.org/rec/conf/fmics/RubbensLH21.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{SafariOH21,
  author    = {Mohsen Safari and
               Wytse Oortwijn and
               Marieke Huisman},
  editor    = {Cezara Dragoi and
               Suvam Mukherjee and
               Kedar S. Namjoshi},
  title     = {Automated Verification of the Parallel Bellman-Ford Algorithm},
  booktitle = {Static Analysis - 28th International Symposium, {SAS} 2021, Chicago,
               IL, USA, October 17-19, 2021, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {12913},
  pages     = {346--358},
  publisher = {Springer},
  year      = {2021},
  url       = {https://doi.org/10.1007/978-3-030-88806-0\_17},
  doi       = {10.1007/978-3-030-88806-0\_17},
  timestamp = {Mon, 18 Oct 2021 08:49:55 +0200},
  biburl    = {https://dblp.org/rec/conf/sas/SafariOH21.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings {Armborst2021,
author = {L. Armborst and M. Huisman},
booktitle = {2021 2021 IEEE/ACM 9th International Conference on Formal Methods in Software Engineering (FormaliSE) (FormaliSE)},
title = {Permission-Based Verification of Red-Black Trees and Their Merging},
year = {2021},
volume = {},
issn = {},
pages = {111-123},
keywords = {tree data structures;annotations;merging;tools;software;ip networks;arrays},
doi = {10.1109/FormaliSE52586.2021.00017},
url = {https://research.utwente.nl/files/253558432/Permission_Based_Verification_of_Red_Black_Trees_and_Their_Merging.pdf},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
month = {may}
}

@InProceedings{10.1007/978-3-030-61467-6_18,
author="Huisman, Marieke
and Monti, Ra{\'u}l E.",
editor="Margaria, Tiziana
and Steffen, Bernhard",
title="On the Industrial Application of Critical Software Verification with VerCors",
booktitle="Leveraging Applications of Formal Methods, Verification and Validation: Applications",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="273--292",
abstract="Although software verification is evolving fast in both theoretical and practical aspects, it still remains absent from the actual industrial production cycle. Case studies can help to encourage these integrations. We report on our experiences applying software verification in several projects with industry. In particular, we report on two projects on the verification of tunnel control software at Technolution, where we go from a high-level design to concrete code. These case studies show the power of combining model checking (using mCRL2) and deductive verification (using VerCors) as complementary approaches. We also report on a project with Thales, where we looked at antenna bearing control software, and specified this based on their requirements documents. For all cases, we report on lessons learned and on directions for future work to improve both our tool and the industrial methodology for ensuring software correctness. Notably, our second case study involves the modelling and verification of critical software by a team of engineers from Technolution. This case study is an ongoing project; we describe our experience on the team's learning curve for this experiment and present the preliminary conclusions on the case study.",
isbn="978-3-030-61467-6",
url = {https://doi.org/10.1007/978-3-030-61467-6_18}
}

Although software verification is evolving fast in both theoretical and practical aspects, it still remains absent from the actual industrial production cycle. Case studies can help to encourage these integrations. We report on our experiences applying software verification in several projects with industry. In particular, we report on two projects on the verification of tunnel control software at Technolution, where we go from a high-level design to concrete code. These case studies show the power of combining model checking (using mCRL2) and deductive verification (using VerCors) as complementary approaches. We also report on a project with Thales, where we looked at antenna bearing control software, and specified this based on their requirements documents. For all cases, we report on lessons learned and on directions for future work to improve both our tool and the industrial methodology for ensuring software correctness. Notably, our second case study involves the modelling and verification of critical software by a team of engineers from Technolution. This case study is an ongoing project; we describe our experience on the team's learning curve for this experiment and present the preliminary conclusions on the case study.

@inproceedings{6eeab50f65fe4d19ba70c113f073785d,
title = "A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms",
abstract = "Sorting is one of the fundamental operations in computer science, and many sequential and parallel algorithms have been proposed in the literature. Swap-based sorting algorithms are one category of sorting algorithms where elements are swapped repeatedly to achieve the desired order. Since these algorithms are widely used in practice, their (functional) correctness, i.e., proving sortedness and permutation properties, is of utmost importance. However, proving the permutation property using automated program verifiers is much more challenging as the formal definition of this property involves existential quantifiers. In this paper, we propose a generic pattern to verify the permutation property for any sequential and parallel swap-based sorting algorithm automatically. To demonstrate our approach, we use VerCors, a verification tool based on separation logic for concurrent and parallel programs, to verify the permutation property of bubble sort, selection sort, insertion sort, parallel odd-even transposition sort, quick sort, two in-place merge sorts and TimSort for any arbitrary size of input.",
author = "Mohsen Safari and Marieke Huisman",
year = "2020",
month = nov,
day = "13",
doi = "10.1007/978-3-030-63461-2_14",
language = "English",
isbn = "978-3-030-63460-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer Singapore",
pages = "257--275",
editor = "Brijesh Dongol and Elena Troubitsyna",
booktitle = "Integrated Formal Methods - 16th International Conference, IFM 2020, Lugano, Switzerland, November 16-20, 2020, Proceedings",
address = "Singapore",
note = "16th International Conference on Integrated Formal Methods, IFM 2020, IFM 2020 ; Conference date: 16-11-2020 Through 20-11-2020",
url = {https://doi.org/10.1007/978-3-030-63461-2_14}
}

Sorting is one of the fundamental operations in computer science, and many sequential and parallel algorithms have been proposed in the literature. Swap-based sorting algorithms are one category of sorting algorithms where elements are swapped repeatedly to achieve the desired order. Since these algorithms are widely used in practice, their (functional) correctness, i.e., proving sortedness and permutation properties, is of utmost importance. However, proving the permutation property using automated program verifiers is much more challenging as the formal definition of this property involves existential quantifiers. In this paper, we propose a generic pattern to verify the permutation property for any sequential and parallel swap-based sorting algorithm automatically. To demonstrate our approach, we use VerCors, a verification tool based on separation logic for concurrent and parallel programs, to verify the permutation property of bubble sort, selection sort, insertion sort, parallel odd-even transposition sort, quick sort, two in-place merge sorts and TimSort for any arbitrary size of input.

@inproceedings{7e7d9f1f6e944f7fa094090c63a9d4ed,
title = "Formal Methods for GPGPU Programming: Is the Demand Met?",
abstract = "Over the years, researchers have developed many formal method tools to support software development. However, hardly any studies are conducted to determine whether the actual problems developers encounter are sufficiently addressed. For the relatively young field of GPU programming, we would like to know whether the tools developed so far are sufficient, or whether some problems still need attention. To this end, we first look at what kind of problems programmers encounter in OpenCL and CUDA. We gather problems from Stack Overflow and categorise them with card sorting. We find that problems related to memory, synchronisation of threads, threads in general and performance are essential topics. Next, we look at (verification) tools in industry and research, to see how these tools addressed the problems we discovered. We think many problems are already properly addressed, but there is still a need for easy to use sound tools. Alternatively, languages or programming styles can be created, that allows for easier checking for soundness.",
keywords = "Bugs, CUDA, Formal methods, GPGPU, GPU, OpenCL, Verification",
author = "{van den Haak}, Lars and Wijs, {Anton J.} and {van den Brand}, {Mark G.J.} and Marieke Huisman",
year = "2020",
doi = "10.1007/978-3-030-63461-2_9",
language = "English",
isbn = "9783030634605",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "160--177",
editor = "Brijesh Dongol and Elena Troubitsyna",
booktitle = "Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings",
address = "Germany",
note = "16th International Conference on Integrated Formal Methods, IFM 2020 ; Conference date: 16-11-2020 Through 20-11-2020",
url = {https://doi.org/10.1007/978-3-030-63461-2_9}
}

Over the years, researchers have developed many formal method tools to support software development. However, hardly any studies are conducted to determine whether the actual problems developers encounter are sufficiently addressed. For the relatively young field of GPU programming, we would like to know whether the tools developed so far are sufficient, or whether some problems still need attention. To this end, we first look at what kind of problems programmers encounter in OpenCL and CUDA. We gather problems from Stack Overflow and categorise them with card sorting. We find that problems related to memory, synchronisation of threads, threads in general and performance are essential topics. Next, we look at (verification) tools in industry and research, to see how these tools addressed the problems we discovered. We think many problems are already properly addressed, but there is still a need for easy to use sound tools. Alternatively, languages or programming styles can be created, that allows for easier checking for soundness.

@inproceedings{8ddbbdbc353e4e209075577edcfc6a5e,
title = "Verification and Validation of Concurrent and Distributed Systems (Track Summary)",
abstract = "Usually, greater concurrency is the goal of any distributed system, yet distribution also introduces issues of consistency and separate failure domains. With the increase of device connectivity and virtualization techniques, developing correct and reliable concurrent and distributed systems characterized by high performance is notoriously difficult. This requires novel verification techniques, or extensions, adaptations and improvements of existing ones, to address emergent problems. The track on Verification and Validation of Concurrent and Distributed Systems aims to discuss key challenges that need to be tackled in order to enable the efficient and scalable assurance of modern concurrent and distributed systems, as well as present methods and tools that bear the promise to achieve the latter.",
author = "Marieke Huisman and Cristina Seceleanu",
year = "2020",
doi = "10.1007/978-3-030-61362-4_24",
language = "English",
isbn = "978-3-030-61361-7",
series = "Lecture Notes in Computer Science",
publisher = "Springer Singapore",
pages = "421--425",
editor = "Tiziana Margaria and Bernhard Steffen",
booktitle = "Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part I",
address = "Singapore",
note = "9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, ISoLA 2020 ; Conference date: 20-10-2020 Through 30-10-2020",
url = {https://doi.org/10.1007/978-3-030-61362-4_24}
}

Usually, greater concurrency is the goal of any distributed system, yet distribution also introduces issues of consistency and separate failure domains. With the increase of device connectivity and virtualization techniques, developing correct and reliable concurrent and distributed systems characterized by high performance is notoriously difficult. This requires novel verification techniques, or extensions, adaptations and improvements of existing ones, to address emergent problems. The track on Verification and Validation of Concurrent and Distributed Systems aims to discuss key challenges that need to be tackled in order to enable the efficient and scalable assurance of modern concurrent and distributed systems, as well as present methods and tools that bear the promise to achieve the latter.

@InProceedings{5f6f89956d7a4f62abe4b4422ebabec9,
title = "The VerifyThis Collaborative Long Term Challenge",
abstract = "Over the last years, we have seen tremendous progress in the area of deductive program verification. To demonstrate this progress, and to bring the area of deductive program verification even further, we have proposed the VerifyThis Collaborative Long Term Challenge, which calls upon the program verification community to verify different aspects of a realistic software application over a period of several months. Goal of the challenge is to foster collaboration in order to verify a realistic and industrially-relevant software application. This paper outlines the considerations that we made when selecting the challenge, and discusses how we believe it will encourage collaboration. It presents the software application that was selected for the challenge in 2019–2020, discusses the practical set up of the challenge, and briefly reports on the received solutions and an online workshop where the different solutions were presented.",
author = "Marieke Huisman and Monti, {Ra{\'u}l E.} and Mattias Ulbrich and Alexander Weigl",
year = "2020",
month = dec,
day = "4",
doi = "10.1007/978-3-030-64354-610",
language = "English",
isbn = "978-3-030-64353-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer Singapore",
pages = "246--260",
editor = "Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H{\"a}hnle and Mattias Ulbrich",
booktitle = "Deductive Software Verification: Future Perspectives",
address = "Singapore",
url = {https://doi.org/10.1007/978-3-030-64354-610}
}

Over the last years, we have seen tremendous progress in the area of deductive program verification. To demonstrate this progress, and to bring the area of deductive program verification even further, we have proposed the VerifyThis Collaborative Long Term Challenge, which calls upon the program verification community to verify different aspects of a realistic software application over a period of several months. Goal of the challenge is to foster collaboration in order to verify a realistic and industrially-relevant software application. This paper outlines the considerations that we made when selecting the challenge, and discusses how we believe it will encourage collaboration. It presents the software application that was selected for the challenge in 2019–2020, discusses the practical set up of the challenge, and briefly reports on the received solutions and an online workshop where the different solutions were presented.

@InProceedings{629eae67ae304c6e9e843bda7ea80ac1,
title = "Improving Performance of the VerCors Program Verifier",
abstract = "As program verification tools are becoming more powerful, and are used on larger programs, their performance also becomes more and more important. In this paper we investigate performance bottlenecks in the VerCors program verifier. Moreover, we also discuss two solutions to the identified performance bottlenecks: an improved encoding of arrays, as well as a technique to automatically generate trigger expressions to guide the underlying prover when reasoning about quantifiers. For both solutions we measure the effect on the performance. We see that the new encoding vastly reduces the verification time of certain programs, while other programs keep showing comparable times. This effect remains when moving to newer backends for VerCors.",
author = "Henk Mulder and Marieke Huisman and Joosten, {Sebastiaan J. C.}",
year = "2020",
doi = "10.1007/978-3-030-64354-6_3",
language = "English",
series = "Lecture Notes in Computer Science",
publisher = "Springer Singapore",
pages = "65--82",
editor = "Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H{\"a}hnle and Mattias Ulbrich",
booktitle = "Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY",
address = "Singapore",
url = {https://doi.org/10.1007/978-3-030-64354-6_3}
}

As program verification tools are becoming more powerful, and are used on larger programs, their performance also becomes more and more important. In this paper we investigate performance bottlenecks in the VerCors program verifier. Moreover, we also discuss two solutions to the identified performance bottlenecks: an improved encoding of arrays, as well as a technique to automatically generate trigger expressions to guide the underlying prover when reasoning about quantifiers. For both solutions we measure the effect on the performance. We see that the new encoding vastly reduces the verification time of certain programs, while other programs keep showing comparable times. This effect remains when moving to newer backends for VerCors.

@InProceedings{10.1007/978-3-030-64276-1_10,
author={Safari, Mohsen
and Huisman, Marieke},
editor={Pun, Violet Ka I.
and Stolz, Volker
and Simao, Adenilso},
title={Formal Verification of Parallel Stream Compaction and Summed-Area Table Algorithms},
booktitle={Theoretical Aspects of Computing -- ICTAC 2020},
year={2020},
publisher={Springer International Publishing},
address={Cham},
pages={181-199},
abstract={Dedicated many-core processors such as GPGPUs, enable programmers to design and implement parallel algorithms to optimize performance. The stream compaction and summed-area table algorithms are two examples where parallel versions have been proposed in the literature with substantial speed ups compared to sequential counterparts.},
isbn={978-3-030-64276-1},
url={https://doi.org/10.1007/978-3-030-64276-1_10}
}

Dedicated many-core processors such as GPGPUs, enable programmers to design and implement parallel algorithms to optimize performance. The stream compaction and summed-area table algorithms are two examples where parallel versions have been proposed in the literature with substantial speed ups compared to sequential counterparts.

@InProceedings{10.1007/978-3-030-55754-6_10,
author="Safari, Mohsen
and Oortwijn, Wytse
and Joosten, Sebastiaan
and Huisman, Marieke",
editor="Lee, Ritchie
and Jha, Susmit
and Mavridou, Anastasia",
title="Formal Verification of Parallel Prefix Sum",
booktitle="NASA Formal Methods",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="170--186",
abstract="With the advent of dedicated hardware for multicore programming, parallel algorithms have become omnipresent. For example, various algorithms have been proposed for the parallel computation of a prefix sum in the literature. As the prefix sum is a basic building block for many other multicore algorithms, such as sorting, its correctness is of utmost importance. This means, the algorithm should be functionally correct, and the implementation should be thread and memory safe.",
isbn="978-3-030-55754-6",
url="https://doi.org/10.1007/978-3-030-55754-6_10"
}

With the advent of dedicated hardware for multicore programming, parallel algorithms have become omnipresent. For example, various algorithms have been proposed for the parallel computation of a prefix sum in the literature. As the prefix sum is a basic building block for many other multicore algorithms, such as sorting, its correctness is of utmost importance. This means, the algorithm should be functionally correct, and the implementation should be thread and memory safe.

@InProceedings{10.1007/978-3-030-45190-5_14,
author="Oortwijn, Wytse
and Huisman, Marieke
and Joosten, Sebastiaan J. C.
and van de Pol, Jaco",
editor="Biere, Armin
and Parker, David",
title="Automated Verification of Parallel Nested DFS",
booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="247--265",
abstract="Model checking algorithms are typically complex graph algorithms, whose correctness is crucial for the usability of a model checker. However, establishing the correctness of such algorithms can be challenging and is often done manually. Mechanising the verification process is crucially important, because model checking algorithms are often parallelised for efficiency reasons, which makes them even more error-prone. This paper shows how the VerCors concurrency verifier is used to mechanically verify the parallel nested depth-first search (NDFS) graph algorithm of Laarman et al. [25]. We also demonstrate how having a mechanised proof supports the easy verification of various optimisations of parallel NDFS. As far as we are aware, this is the first automated deductive verification of a multi-core model checking algorithm.",
isbn="978-3-030-45190-5"
}

Model checking algorithms are typically complex graph algorithms, whose correctness is crucial for the usability of a model checker. However, establishing the correctness of such algorithms can be challenging and is often done manually. Mechanising the verification process is crucially important, because model checking algorithms are often parallelised for efficiency reasons, which makes them even more error-prone. This paper shows how the VerCors concurrency verifier is used to mechanically verify the parallel nested depth-first search (NDFS) graph algorithm of Laarman et al. [25]. We also demonstrate how having a mechanised proof supports the easy verification of various optimisations of parallel NDFS. As far as we are aware, this is the first automated deductive verification of a multi-core model checking algorithm.

@InProceedings{10.1007/978-3-030-39322-9_19,
author="Oortwijn, Wytse
and Gurov, Dilian
and Huisman, Marieke",
editor="Beyer, Dirk
and Zufferey, Damien",
title="Practical Abstractions for Automated Verification of Shared-Memory Concurrency",
booktitle="Verification, Model Checking, and Abstract Interpretation",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="401--425",
abstract="Modern concurrent and distributed software is highly complex. Techniques to reason about the correct behaviour of such software are essential to ensure its reliability. To be able to reason about realistic programs, these techniques must be modular and compositional as well as practical by being supported by automated tools. However, many existing approaches for concurrency verification are theoretical and focus on expressivity and generality. This paper contributes a technique for verifying behavioural properties of concurrent and distributed programs that makes a trade-off between expressivity and usability. The key idea of the approach is that program behaviour is abstractly modelled using process algebra, and analysed separately. The main difficulty is presented by the typical abstraction gap between program implementations and their models. Our approach bridges this gap by providing a deductive technique for formally linking programs with their process-algebraic models. Our verification technique is modular and compositional, is proven sound with Coq, and has been implemented in the automated concurrency verifier VerCors. Moreover, our technique is demonstrated on multiple case studies, including the verification of a leader election protocol.",
isbn="978-3-030-39322-9"
}

Modern concurrent and distributed software is highly complex. Techniques to reason about the correct behaviour of such software are essential to ensure its reliability. To be able to reason about realistic programs, these techniques must be modular and compositional as well as practical by being supported by automated tools. However, many existing approaches for concurrency verification are theoretical and focus on expressivity and generality. This paper contributes a technique for verifying behavioural properties of concurrent and distributed programs that makes a trade-off between expressivity and usability. The key idea of the approach is that program behaviour is abstractly modelled using process algebra, and analysed separately. The main difficulty is presented by the typical abstraction gap between program implementations and their models. Our approach bridges this gap by providing a deductive technique for formally linking programs with their process-algebraic models. Our verification technique is modular and compositional, is proven sound with Coq, and has been implemented in the automated concurrency verifier VerCors. Moreover, our technique is demonstrated on multiple case studies, including the verification of a leader election protocol.

@misc{essay82062,
title       = {Encoding deadlock-free monitors in the VerCors verification tool},
month       = {July},
year        = {2020},
author      = {M.J. {Roelink}},
abstract    = {When developing a concurrent program, a deadlock is never the intended result. However, avoiding them is often attributed to the experience of the developer, as a compiler is generally not able to detect them. Recently, a technique has been proposed to verify deadlock-freeness of a program with monitors. The aim of this research is to investigate how this technique can be encoded in the VerCors verification tool to verify deadlock-freeness of Java-like programs. This paper specifies the required annotation syntax and describes the implementation of the technique in VerCors.},
url         = {http://essay.utwente.nl/82062/}
}

When developing a concurrent program, a deadlock is never the intended result. However, avoiding them is often attributed to the experience of the developer, as a compiler is generally not able to detect them. Recently, a technique has been proposed to verify deadlock-freeness of a program with monitors. The aim of this research is to investigate how this technique can be encoded in the VerCors verification tool to verify deadlock-freeness of Java-like programs. This paper specifies the required annotation syntax and describes the implementation of the technique in VerCors.

@MastersThesis{essay80892,
title       = {Extending support for axiomatic data types in VerCors},
author      = {\"O.F.O. {\c{S}akar}},
year        = {2020},
month       = {April},
url         = {http://essay.utwente.nl/80892/},
abstract    = {VerCors is a static verifier of concurrent/parallel programs developed at the University of Twente. The software that is verified with VerCors (and similar tools) use common data types such as lists or sets. The behavior of these data types is modeled in VerCors using axiomatic data types (ADTs). VerCors currently supports axiomatic data types such as sequences/lists, sets, and bags. To extend the support for ADTs, a list of features to add to VerCors was compiled by using input from end-users. An implementation-level view of VerCors is given with general approaches to implementing a feature in VerCors. For each feature in this list a definition is given, its encoding into Viper (the back end of VerCors) is discussed and its implementation using the general approaches is explained.}
}

VerCors is a static verifier of concurrent/parallel programs developed at the University of Twente. The software that is verified with VerCors (and similar tools) use common data types such as lists or sets. The behavior of these data types is modeled in VerCors using axiomatic data types (ADTs). VerCors currently supports axiomatic data types such as sequences/lists, sets, and bags. To extend the support for ADTs, a list of features to add to VerCors was compiled by using input from end-users. An implementation-level view of VerCors is given with general approaches to implementing a feature in VerCors. For each feature in this list a definition is given, its encoding into Viper (the back end of VerCors) is discussed and its implementation using the general approaches is explained.

@MastersThesis{essay81338,
month       = {May},
author      = {R.B. {Rubbens}},
year        = {2020},
title       = {Improving Support for Java Exceptions and Inheritance in VerCors},
abstract    = {In the age where one software bug can cost millions, software correctness is paramount. Static verifiers are used more and more in both academia and industry to prevent these costly bugs. They can formally prove that an implementation adheres to a specification. With the recent increased use of concurrency, proving correctness of software has become more challenging. However, progress is being made in this area: several static verifiers can now also verify languages in concurrent environments. Unfortunately their features are lagging behind: most checkers do not proceed beyond the prototyping phase and do not tackle the more practical language features. To improve the situation, this work presents an approach for implementing verification support for exceptions and inheritance as presented in Java. We also present, in great detail, the transformation of a language with exceptions and inheritance into a language without, and discuss the theory underlying the practical support for exceptions and inheritance. Finally, we briefly evaluate the approaches for both exceptions and inheritance, and discuss what can be further improved in static verification.},
url         = {http://essay.utwente.nl/81338/}
}

In the age where one software bug can cost millions, software correctness is paramount. Static verifiers are used more and more in both academia and industry to prevent these costly bugs. They can formally prove that an implementation adheres to a specification. With the recent increased use of concurrency, proving correctness of software has become more challenging. However, progress is being made in this area: several static verifiers can now also verify languages in concurrent environments. Unfortunately their features are lagging behind: most checkers do not proceed beyond the prototyping phase and do not tackle the more practical language features. To improve the situation, this work presents an approach for implementing verification support for exceptions and inheritance as presented in Java. We also present, in great detail, the transformation of a language with exceptions and inheritance into a language without, and discuss the theory underlying the practical support for exceptions and inheritance. Finally, we briefly evaluate the approaches for both exceptions and inheritance, and discuss what can be further improved in static verification.

@InProceedings{34e7beecf4454c0bac5684a16ea3605e,
title = "Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools",
abstract = "Deductive software verification aims at formally verifying that all possible behaviors of a given program satisfy formally defined, possibly complex properties, where the verification process is based on logical inference. We follow the trajectory of the field from its inception in the late 1960s via its current state to its promises for the future, from pen-and-paper proofs for programs written in small, idealized languages to highly automated proofs of complex library or system code written in mainstream languages. We take stock of the state-of-art and give a list of the most important challenges for the further development of the field of deductive software verification.",
author = "Reiner H{\"a}hnle and Marieke Huisman",
year = "2019",
doi = "10.1007/978-3-319-91908-9_18",
language = "English",
isbn = "978-3-319-91907-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "345--373",
editor = "Bernhard Steffen and Gerhard Woeginger",
booktitle = "Computing and Software Science",
url = {https://doi.org/10.1007/978-3-319-91908-9_18}
}

Deductive software verification aims at formally verifying that all possible behaviors of a given program satisfy formally defined, possibly complex properties, where the verification process is based on logical inference. We follow the trajectory of the field from its inception in the late 1960s via its current state to its promises for the future, from pen-and-paper proofs for programs written in small, idealized languages to highly automated proofs of complex library or system code written in mainstream languages. We take stock of the state-of-art and give a list of the most important challenges for the further development of the field of deductive software verification.

@InProceedings{10.1007/978-3-030-34968-4_22,
author="Oortwijn, Wytse
and Huisman, Marieke",
editor="Ahrendt, Wolfgang
and Tapia Tarifa, Silvia Lizeth",
title="Practical Abstractions for Automated Verification of Message Passing Concurrency",
booktitle="Integrated Formal Methods",
year="2019",
publisher="Springer International Publishing",
address="Cham",
pages="399--417",
abstract="Distributed systems are notoriously difficult to develop correctly, due to the concurrency in their communicating subsystems. Several techniques are available to help developers to improve the reliability of message passing software, including deductive verification and model checking. Both these techniques have advantages as well as limitations, which are complementary in nature. This paper contributes a novel verification technique that combines the strengths of deductive and algorithmic verification to reason elegantly about message passing concurrent programs, thereby reducing their limitations. Our approach allows to verify data-centric properties of message passing programs using concurrent separation logic (CSL), and allows to specify their communication behaviour as a process-algebraic model. The key novelty of the approach is that it formally bridges the typical abstraction gap between programs and their models, by extending CSL with logical primitives for proving deductively that a program refines its process-algebraic model. These models can then be analysed via model checking, using mCRL2, to reason indirectly about the program's communication behaviour. Our verification approach is compositional, comes with a mechanised correctness proof in Coq, and is implemented as an encoding in Viper.",
isbn="978-3-030-34968-4",
url ="https://doi.org/10.1007/978-3-030-34968-4_22"
}

Distributed systems are notoriously difficult to develop correctly, due to the concurrency in their communicating subsystems. Several techniques are available to help developers to improve the reliability of message passing software, including deductive verification and model checking. Both these techniques have advantages as well as limitations, which are complementary in nature. This paper contributes a novel verification technique that combines the strengths of deductive and algorithmic verification to reason elegantly about message passing concurrent programs, thereby reducing their limitations. Our approach allows to verify data-centric properties of message passing programs using concurrent separation logic (CSL), and allows to specify their communication behaviour as a process-algebraic model. The key novelty of the approach is that it formally bridges the typical abstraction gap between programs and their models, by extending CSL with logical primitives for proving deductively that a program refines its process-algebraic model. These models can then be analysed via model checking, using mCRL2, to reason indirectly about the program's communication behaviour. Our verification approach is compositional, comes with a mechanised correctness proof in Coq, and is implemented as an encoding in Viper.

@InProceedings{10.1007/978-3-030-34968-4_23,
author="Oortwijn, Wytse
and Huisman, Marieke",
editor="Ahrendt, Wolfgang
and Tapia Tarifa, Silvia Lizeth",
title="Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System",
booktitle="Integrated Formal Methods",
year="2019",
publisher="Springer International Publishing",
address="Cham",
pages="418--436",
abstract="Over the last decades, significant progress has been made on formal techniques for software verification. However, despite this progress, these techniques are not yet structurally applied in industry. To reduce the well-known industry--academia gap, industrial case studies are much-needed, to demonstrate that formal methods are now mature enough to help increase the reliability of industrial software. Moreover, case studies also help researchers to get better insight into industrial needs.",
isbn="978-3-030-34968-4",
url="https://doi.org/10.1007/978-3-030-34968-4_23"
}

Over the last decades, significant progress has been made on formal techniques for software verification. However, despite this progress, these techniques are not yet structurally applied in industry. To reduce the well-known industry–academia gap, industrial case studies are much-needed, to demonstrate that formal methods are now mature enough to help increase the reliability of industrial software. Moreover, case studies also help researchers to get better insight into industrial needs.

@phdthesis{eed8e862be3a4fe785a4e94855d13674,
title = "Deductive techniques for model-based concurrency verification",
abstract = "This thesis contributes formal techniques for verifying global behavioural properties of real-world concurrent software in a sound and practical manner.The first part of this thesis discusses how Concurrent Separation Logic (CSL) can be used to mechanically verify the parallel nested depth-first search (NDFS) model checking algorithm. This verification has been performed using VerCors. We also demonstrate how our mechanized correctness proof allows verifying various optimisations of parallel NDFS with only little extra effort.The second part contributes an abstraction technique for verifying global behavioural properties of shared-memory concurrent software. This abstraction technique allows specifying program behavior as a process-algebraic model, with an elegant algebraic structure. Furthermore, we extend CSL with logical primitives that allow one to prove that a program refines its process-algebraic specification. This abstraction technique is proven sound using Coq and is implemented in VerCors. We demonstrate our approach on various examples, including a real-world case study from industry that concerns safety-critical code.In part three, we lift our abstraction technique to the distributed case, by adapting it for verifying message passing concurrent software. This adaptation uses process-algebraic specifications to abstract the communication behavior of distributed agents. We also investigate how model checking of these specifications can soundly be combined with the deductive verification of the specified program.",
author = "Oortwijn, {Wytse Hendrikus Marinus}",
year = "2019",
month = "12",
day = "12",
doi = "10.3990/1.9789036548984",
language = "English",
isbn = "978-90-365-4898-4",
series = "DSI Ph.D. Thesis Series",
publisher = "University of Twente",
number = "19-021",
address = "Netherlands",
school = "University of Twente",
url="https://doi.org/10.3990/1.9789036548984"
}

This thesis contributes formal techniques for verifying global behavioural properties of real-world concurrent software in a sound and practical manner.The first part of this thesis discusses how Concurrent Separation Logic (CSL) can be used to mechanically verify the parallel nested depth-first search (NDFS) model checking algorithm. This verification has been performed using VerCors. We also demonstrate how our mechanized correctness proof allows verifying various optimisations of parallel NDFS with only little extra effort.The second part contributes an abstraction technique for verifying global behavioural properties of shared-memory concurrent software. This abstraction technique allows specifying program behavior as a process-algebraic model, with an elegant algebraic structure. Furthermore, we extend CSL with logical primitives that allow one to prove that a program refines its process-algebraic specification. This abstraction technique is proven sound using Coq and is implemented in VerCors. We demonstrate our approach on various examples, including a real-world case study from industry that concerns safety-critical code.In part three, we lift our abstraction technique to the distributed case, by adapting it for verifying message passing concurrent software. This adaptation uses process-algebraic specifications to abstract the communication behavior of distributed agents. We also investigate how model checking of these specifications can soundly be combined with the deductive verification of the specified program.

@misc{essay77569,
           month = {March},
          author = {ir. H.M. {Nguyen}},
            year = {2019},
           title = {Formal verification of a red-black tree data structure},
             url = {http://essay.utwente.nl/77569/},
        abstract = {Nowadays, although software has been integrated deeply into our society, software errors are still common. Because the failure of software can have devastating effects, being certain that a program does what it is meant to do is crucial. This thesis conducts a case study in deductive verification, which is a sub-area of formal verification. The case study involves a company in the Netherlands and their industrial red-black tree code. This thesis is intended to be an experience report to show how formal verification can be used to help proving the correctness of a program. Ultimately, we want to be able to verify the industrial red-black tree code. However, in this thesis, we only cover the verification of a standard red-black tree code. The main section presents how specifications of a red-black tree can be developed, and the obstacles that are met during the development. Finally, we conclude with the comparisons with the results of other authors and possible future work.}
}

Nowadays, although software has been integrated deeply into our society, software errors are still common. Because the failure of software can have devastating effects, being certain that a program does what it is meant to do is crucial. This thesis conducts a case study in deductive verification, which is a sub-area of formal verification. The case study involves a company in the Netherlands and their industrial red-black tree code. This thesis is intended to be an experience report to show how formal verification can be used to help proving the correctness of a program. Ultimately, we want to be able to verify the industrial red-black tree code. However, in this thesis, we only cover the verification of a standard red-black tree code. The main section presents how specifications of a red-black tree can be developed, and the obstacles that are met during the development. Finally, we conclude with the comparisons with the results of other authors and possible future work.

@InProceedings{10.1007/978-3-030-17502-3_12,
author= {Ernst, Gidon and Huisman, Marieke and Mostowski, Wojciech and Ulbrich, Mattias},
title="VerifyThis -- Verification Competition with a Human Factor",
booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
year="2019",
publisher="Springer International Publishing",
address="Cham",
pages="176--195",
abstract="VerifyThis is a series of competitions that aims to evaluate the current state of deductive tools to prove functional correctness of programs. Such proofs typically require human creativity, and hence it is not possible to measure the performance of tools independently of the skills of its user. Similarly, solutions can be judged by humans only. In this paper, we discuss the role of the human in the competition setup and explore possible future changes to the current format. Regarding the impact of VerifyThis on deductive verification research, a survey conducted among the previous participants shows that the event is a key enabler for gaining insight into other approaches, and that it fosters collaboration and exchange.",
isbn="978-3-030-17502-3",
url= "https://link.springer.com/chapter/10.1007/978-3-030-17502-3_12"
}

VerifyThis is a series of competitions that aims to evaluate the current state of deductive tools to prove functional correctness of programs. Such proofs typically require human creativity, and hence it is not possible to measure the performance of tools independently of the skills of its user. Similarly, solutions can be judged by humans only. In this paper, we discuss the role of the human in the competition setup and explore possible future changes to the current format. Regarding the impact of VerifyThis on deductive verification research, a survey conducted among the previous participants shows that the event is a key enabler for gaining insight into other approaches, and that it fosters collaboration and exchange.

@book{c4fd4c231b0743a58ef1b41e7a574deb,
    title       = "VerifyThis2018: A Program Verification Competition",
    abstract    = "VerifyThis 2018 was a two-day program verification competition which took place on April 14 and 15,2018 in Thessaloniki, Greece as part of the European Joint Conferences on Theory and Practice of Software(ETAPS 2018). It was the sixth instalment in the VerifyThis competition series. This article provides an overview of the VerifyThis 2018 event, the challenges that were posed during the competition, and a high-level overview of the solutions to these challenges. It concludes with the results of the competition.",
    author      = "Marieke Huisman and Rosemary Monahan and Peter M{\"u}ller and Andrei Paskevich and Gidon Ernst",
    year        = "2019",
    month       = "1",
    language    = "English",
    url         = {https://hal.inria.fr/hal-01981937/}
}

VerifyThis 2018 was a two-day program verification competition which took place on April 14 and 15,2018 in Thessaloniki, Greece as part of the European Joint Conferences on Theory and Practice of Software(ETAPS 2018). It was the sixth instalment in the VerifyThis competition series. This article provides an overview of the VerifyThis 2018 event, the challenges that were posed during the competition, and a high-level overview of the solutions to these challenges. It concludes with the results of the competition.

@MastersThesis{essay78496,
month = {July},
title = {Performance of program verification with VerCors},
author = {Henk {Mulder}},
year = {2019},
url = {http://essay.utwente.nl/78496/},
abstract = {Program verification is only as useful as its ability to produce results in a timely
manner. In this research we investigate what performance bottlenecks are in
the VerCors verification tool for concurrent programs. The aim is to identify
the cause of a performance bottleneck, in order to optimize the tool.
We introduce a technique to identify what properties of a program are more
difficult to verify. Using those results, we present solutions to two performance
bottlenecks that were identified: 1. An alternative encoding of arrays is implemented
in the tool which allows the tool to reason up to 4 times faster about
programs that make use of arrays. 2. Our research in generating triggers for
quantified expressions show that speedups up to 30% are possible. Though further
research is required to investigate if this solution can be generalized and
optimized further.}
}

Program verification is only as useful as its ability to produce results in a timely manner. In this research we investigate what performance bottlenecks are in the VerCors verification tool for concurrent programs. The aim is to identify the cause of a performance bottleneck, in order to optimize the tool. We introduce a technique to identify what properties of a program are more difficult to verify. Using those results, we present solutions to two performance bottlenecks that were identified: 1. An alternative encoding of arrays is implemented in the tool which allows the tool to reason up to 4 times faster about programs that make use of arrays. 2. Our research in generating triggers for quantified expressions show that speedups up to 30% are possible. Though further research is required to investigate if this solution can be generalized and optimized further.

@InProceedings{10.1007/978-3-319-98938-9_3,
author="Boerman, Jan and Huisman, Marieke and Joosten, Sebastiaan",
editor="Furia, Carlo A.
and Winter, Kirsten",
title="Reasoning About JML: Differences Between KeY and OpenJML",
booktitle="Integrated Formal Methods",
year="2018",
publisher="Springer International Publishing",
address="Cham",
pages="30--46",
abstract="To increase the impact and capabilities of formal verification, it should be possible to apply different verification techniques on the same specification. However, this can only be achieved if verification tools agree on the syntax and underlying semantics of the specification language and unfortunately, in practice, this is often not the case.",
isbn="978-3-319-98938-9",
url={https://link.springer.com/chapter/10.1007/978-3-319-98938-9_3}
}

To increase the impact and capabilities of formal verification, it should be possible to apply different verification techniques on the same specification. However, this can only be achieved if verification tools agree on the syntax and underlying semantics of the specification language and unfortunately, in practice, this is often not the case.

@inproceedings{DBLP:conf/birthday/HuismanJ18,
  author    = {Marieke Huisman and Sebastiaan J. C. Joosten},
  title     = {Towards Reliable Concurrent Software},
  booktitle = {Principled Software Development},
  pages     = {129--146},
  publisher = {Springer},
  year      = {2018},
  url       = {https://link.springer.com/chapter/10.1007/978-3-319-98047-8_9}
}

@inproceedings{DBLP:conf/isola/JoostenH18,
  author    = {Sebastiaan J. C. Joosten and Marieke Huisman},
  title     = {Static Code Verification Through Process Models},
  booktitle = {ISoLA {(3)}},
  series    = {Lecture Notes in Computer Science},
  volume    = {11246},
  pages     = {343--354},
  publisher = {Springer},
  year      = {2018},
  url       = {https://link.springer.com/chapter/10.1007%2F978-3-030-03424-5_23}
}

@inproceedings{DBLP:conf/isola/HuismanBDS18,
  author    = {Marieke Huisman and Stefan Blom and Saeed Darabi and Mohsen Safari},
  title     = {Program Correctness by Transformation},
  booktitle = {ISoLA {(1)}},
  series    = {Lecture Notes in Computer Science},
  volume    = {11244},
  pages     = {365--380},
  publisher = {Springer},
  year      = {2018},
  url       = {https://link.springer.com/chapter/10.1007/978-3-030-03418-4_22}
}

@inproceedings{DBLP:conf/issta/JoostenOSH18,
  author    = {Sebastiaan J. C. Joosten and Wytse Oortwijn and Mohsen Safari and Marieke Huisman},
  title     = {An exercise in verifying sequential programs with VerCors},
  booktitle = {{ISSTA/ECOOP} Workshops},
  pages     = {40--45},
  publisher = {{ACM}},
  year      = {2018},
  url       = {https://research.utwente.nl/en/publications/an-exercise-in-verifying-sequential-programs-with-vercors}
}

@inproceedings{DBLP:journals/corr/abs-1806-09851,
  author    = {Afshin Amighi and Marieke Huisman and Stefan Blom},
  title     = {Verification of Shared-Reading Synchronisers},
  booktitle = {MeTRiD@ETAPS},
  series    = {{EPTCS}},
  volume    = {272},
  pages     = {107--120},
  year      = {2018},
  url       = {https://arxiv.org/abs/1806.09851}
}

@phdthesis{e36589ceaad34ad595fd9fbd0626542b,
   title = "Verification of program parallelization",
    abstract = "This thesis presents a set of verification techniques based on permission-based separation logic to reason about the data race freedom and functional correctness of program parallelizations. Our reasoning techniques address different forms of high-level and low-level parallelization. For high-level parallel programs, we first define the Parallel Programming Language (PPL), a simple core language that captures the main features of deterministic parallel programming; then we discuss how PPL programs and consequently, real-world deterministic parallel programs (e.g. OpenMP programs) are verified. For low-level parallel programs, we specifically focus on reasoning about GPGPU kernels. At the end we discuss how the presented verification techniques are chained together to reason about the semantic equivalence of high-level parallel programs where they are automatically transformed to low-level parallel programs by a parallelizing compiler. Thus, effectively enabling a holistic verification solution for such parallelization frameworks.",
    author = "Saeed Darabi",
    note = "IPA Dissertation Series No. 2018-02 IDS PhD. Thesis Series No. 18-458",
    year = "2018",
    month = "3",
    day = "2",
    doi = "10.3990/1.9789036544849",
    language = "English",
    isbn = "978-90-365-4484-9",
    school = "University of Twente",
    url     = {https://research.utwente.nl/en/publications/verification-of-program-parallelization}
}

This thesis presents a set of verification techniques based on permission-based separation logic to reason about the data race freedom and functional correctness of program parallelizations. Our reasoning techniques address different forms of high-level and low-level parallelization. For high-level parallel programs, we first define the Parallel Programming Language (PPL), a simple core language that captures the main features of deterministic parallel programming; then we discuss how PPL programs and consequently, real-world deterministic parallel programs (e.g. OpenMP programs) are verified. For low-level parallel programs, we specifically focus on reasoning about GPGPU kernels. At the end we discuss how the presented verification techniques are chained together to reason about the semantic equivalence of high-level parallel programs where they are automatically transformed to low-level parallel programs by a parallelizing compiler. Thus, effectively enabling a holistic verification solution for such parallelization frameworks.

@phdthesis{7077aace92e5428aaa370770a09e2b7a,
    title       = "Specification and verification of synchronisation classes in Java: A practical approach",
    abstract    = "Digital services are becoming an essential part of our daily lives. To provide these services, efficient software plays an important role. Concurrent programming is a technique that developers can exploit to gain more performance. In a concurrent program several threads of execution simultaneously are being executed. Sometimes they have to compete to access shared resources, like memory. This race of accessing shared memories can cause unexpected errors. Programmers use synchronisation constructs to tame the concurrency and control the accesses. In order to develop reliable concurrent software, the correctness of these synchronisation constructs is crucial.In this thesis we use a program logic, called permission-based Separation Logic, to statically reason about the correctness of synchronisation constructs. The logic has the power to reason about correct ownership of threads regarding shared memory. A correctly functioning synchroniser is responsible for exchanging a correct permission when a thread requests access to the shared memory. We use our VERCORS verification tool-set to verify the correctness of various synchronisation constructs.In Chapter 1 we discuss the scope of the thesis. All the required technical background about permission-based Separation Logic and synchronisation classes is explained in Chapter 2. In Chapter 3 we discuss how threads' start and join as minimum synchronisation points can be verified. To verify correctness of the synchronisation classes we have to first specify expected behaviour of the classes. This is covered in Chapter 4. In this chapter we present a unified approach to abstractly describe the common behaviour of synchronisers. Using our specifications, one is able to reason about the correctness of the client programs that access the shared state through the synchronisers.The atomic classes of java.util.concurrent are the core element of every synchronisation construct implementation. In Chapter 5 and Chapter 6 we propose a specification for atomic classes. Using this contract, we verified the implementation of synchronisation constructs w.r.t to their specifications from Chapter 4. In our proposed contract the specification of the atomic classes is parameterized with the protocols and resource invariants. Based on the context, the parameters can be defined. In Chapter 7 we propose a verification stack where each layer of stack verifies one particular aspect of a specified concurrent program in which atomic operations are the main synchronisation constructs. We demonstrate how to verify that a non-blocking data structure is data-race free and well connected. Based on the result of the verification from the lower layers, upper layers can reason about the functional properties of the concurrent data structure.In Chapter 8 we present a sound specification and verification technique to reason about data race freedom and functional correctness of GPU kernels that use atomic operations as synchronisation mechanism.Finally, Chapter 9 concludes the thesis with future directions.",
    author      = "A. Amighi",
    note        = "CTIT Ph.D. thesis series No. 17-451 IPA dissertation series No. 2018-01",
    year        = "2018",
    month       = "1",
    day         = "17",
    doi         = "10.3990/1.9789036544399",
    language    = "English",
    isbn        = "978-90-365-4439-9",
    publisher   = "University of Twente",
    address     = "Netherlands",
    school      = "University of Twente",
    url         = {https://research.utwente.nl/en/publications/specification-and-verification-of-synchronisation-classes-in-java}
}

Digital services are becoming an essential part of our daily lives. To provide these services, efficient software plays an important role. Concurrent programming is a technique that developers can exploit to gain more performance. In a concurrent program several threads of execution simultaneously are being executed. Sometimes they have to compete to access shared resources, like memory. This race of accessing shared memories can cause unexpected errors. Programmers use synchronisation constructs to tame the concurrency and control the accesses. In order to develop reliable concurrent software, the correctness of these synchronisation constructs is crucial.In this thesis we use a program logic, called permission-based Separation Logic, to statically reason about the correctness of synchronisation constructs. The logic has the power to reason about correct ownership of threads regarding shared memory. A correctly functioning synchroniser is responsible for exchanging a correct permission when a thread requests access to the shared memory. We use our VERCORS verification tool-set to verify the correctness of various synchronisation constructs.In Chapter 1 we discuss the scope of the thesis. All the required technical background about permission-based Separation Logic and synchronisation classes is explained in Chapter 2. In Chapter 3 we discuss how threads' start and join as minimum synchronisation points can be verified. To verify correctness of the synchronisation classes we have to first specify expected behaviour of the classes. This is covered in Chapter 4. In this chapter we present a unified approach to abstractly describe the common behaviour of synchronisers. Using our specifications, one is able to reason about the correctness of the client programs that access the shared state through the synchronisers.The atomic classes of java.util.concurrent are the core element of every synchronisation construct implementation. In Chapter 5 and Chapter 6 we propose a specification for atomic classes. Using this contract, we verified the implementation of synchronisation constructs w.r.t to their specifications from Chapter 4. In our proposed contract the specification of the atomic classes is parameterized with the protocols and resource invariants. Based on the context, the parameters can be defined. In Chapter 7 we propose a verification stack where each layer of stack verifies one particular aspect of a specified concurrent program in which atomic operations are the main synchronisation constructs. We demonstrate how to verify that a non-blocking data structure is data-race free and well connected. Based on the result of the verification from the lower layers, upper layers can reason about the functional properties of the concurrent data structure.In Chapter 8 we present a sound specification and verification technique to reason about data race freedom and functional correctness of GPU kernels that use atomic operations as synchronisation mechanism.Finally, Chapter 9 concludes the thesis with future directions.

@techreport{HuismanMonahanMueller2017_1000077160,
author       = {Huisman, Marieke and Monahan, Rosemary and Müller, Peter and Mostowski, Wojciech and Ulbrich, Mattias},
year         = {2017},
title        = {VerifyThis 2017 : A Program Verification Competition},
doi         = {10.5445/IR/1000077160},
institution  = {Karlsruher Institut für Technologie (KIT)},
issn         = {2190-4782},
series       = {Karlsruhe Reports in Informatics},
pagetotal    = {9},
language     = {english},
volume       = {2017},
number       = {10},
url={https://publikationen.bibliothek.kit.edu/1000077160}
}

@inproceedings{ARCADE2017:24_Challenges_in_Deductive,
  author    = {Reiner H\textbackslash{}"ahnle and Marieke Huisman},
  title     = {24 Challenges in Deductive Software Verification},
  booktitle = {ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements},
  editor    = {Giles Reger and Dmitriy Traytel},
  series    = {EPiC Series in Computing},
  volume    = {51},
  pages     = {37--41},
  year      = {2017},
  publisher = {EasyChair},
  bibsource = {EasyChair, https://easychair.org},
  issn      = {2398-7340},
  url       = {https://easychair.org/publications/paper/kdZ7},
  doi       = {10.29007/j2cm}
  }
  

@inproceedings{DBLP:conf/ifm/BlomDHO17,
  author    = {Stefan Blom and Saeed Darabi and Marieke Huisman and Wytse Oortwijn},
  title     = {The VerCors Tool Set: Verification of Parallel and Concurrent Software},
  booktitle = {{IFM}},
  series    = {Lecture Notes in Computer Science},
  volume    = {10510},
  pages     = {102--110},
  publisher = {Springer},
  year      = {2017},
  url       = {https://link.springer.com/chapter/10.1007/978-3-319-66845-1_7}
}

@article{DBLP:journals/sttt/HuismanKMT17,
  author    = {Marieke Huisman and Vladimir Klebanov and Rosemary Monahan and Michael Tautschnig},
  title     = {VerifyThis 2015 - {A} program verification competition},
  journal   = {{STTT}},
  volume    = {19},
  number    = {6},
  pages     = {763--771},
  year      = {2017},
  url       = {https://link.springer.com/article/10.1007/s10009-016-0438-x}
}

@inproceedings{DBLP:conf/nfm/DarabiBH17,
  author    = {Saeed Darabi and Stefan C. C. Blom and Marieke Huisman},
  title     = {A Verification Technique for Deterministic Parallel Programs},
  booktitle = {{NFM}},
  series    = {Lecture Notes in Computer Science},
  volume    = {10227},
  pages     = {247--264},
  year      = {2017},
  url       = {https://link.springer.com/chapter/10.1007/978-3-319-57288-8_17}
}

@inproceedings{DBLP:conf/vstte/OortwijnBGHZ17,
  author    = {Wytse Oortwijn and Stefan Blom and Dilian Gurov and Marieke Huisman and Marina Zaharieva{-}Stojanovski},
  title     = {An Abstraction Technique for Describing Concurrent Program Behaviour},
  booktitle = {{VSTTE}},
  series    = {Lecture Notes in Computer Science},
  volume    = {10712},
  pages     = {191--209},
  publisher = {Springer},
  year      = {2017},
  url       = {https://link.springer.com/chapter/10.1007/978-3-319-72308-2_12}
}

@InProceedings{Huisman2016,
author= {Huisman, Marieke and Ahrendt, Wolfgang and Grahl, Daniel and Hentschel, Martin},
editor="Ahrendt, Wolfgang
and Beckert, Bernhard
and Bubel, Richard
and H{\"a}hnle, Reiner
and Schmitt, Peter H.
and Ulbrich, Mattias",
title="Formal Specification with the Java Modeling Language",
bookTitle="Deductive Software Verification -- The KeY Book: From Theory to Practice",
year="2016",
publisher="Springer International Publishing",
address="Cham",
pages="193--241",
abstract="This text is a general, self contained, and tool  independent introduction into the Java Modeling Language, JML. It  appears in a book about the KeY approach and tool for the  verification of Java software, because JML is the dominating  starting point of KeY style Java verification. However, this chapter  does not depend on any specific tool nor verification methodology in  any way. This introduction is written for all readers with an  interest in formal specification of software in general, and anyone  who wants to learn about the JML approach to specification in  particular.",
isbn="978-3-319-49812-6",
doi="10.1007/978-3-319-49812-6_7",
url="https://doi.org/10.1007/978-3-319-49812-6_7"
}

This text is a general, self contained, and tool independent introduction into the Java Modeling Language, JML. It appears in a book about the KeY approach and tool for the verification of Java software, because JML is the dominating starting point of KeY style Java verification. However, this chapter does not depend on any specific tool nor verification methodology in any way. This introduction is written for all readers with an interest in formal specification of software in general, and anyone who wants to learn about the JML approach to specification in particular.

@book{b8dbe2be359242bf8f03dad396167e24,
title = "VerifyThis 2016: A Program Verification Competition",
abstract = "VerifyThis 2016 was a one-day program verification competition which took place on April 2nd, 2016 in Eindhoven, The Netherlands as part of the European Joint Conferences on Theory and Practice of Soft- ware (ETAPS 2016). It was the fifth instalment in the VerifyThis competition series. This article provides an overview of the VerifyThis 2016 event, the challenges that were posed during the competition, and a high-level overview of the solutions to these challenges. It concludes with the results of the competition.",
keywords = "Program Verification, EWI-27060, IR-100549, Competition, METIS-317220",
author = "Marieke Huisman and Rosemary Monahan and Peter Müller and Erik Poll",
note = "eemcs-eprint-27060",
year = "2016",
month = "6",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-16-07",
address = "Netherlands",
url = "https://research.utwente.nl/en/publications/verifythis-2016-a-program-verification-competition(b8dbe2be-3592-42bf-8f03-dad396167e24).html"
}

VerifyThis 2016 was a one-day program verification competition which took place on April 2nd, 2016 in Eindhoven, The Netherlands as part of the European Joint Conferences on Theory and Practice of Soft- ware (ETAPS 2016). It was the fifth instalment in the VerifyThis competition series. This article provides an overview of the VerifyThis 2016 event, the challenges that were posed during the competition, and a high-level overview of the solutions to these challenges. It concludes with the results of the competition.

@inproceedings{DBLP:conf/pdp/AmighiBH16,
  author    = {Afshin Amighi and Stefan Blom and Marieke Huisman},
  title     = {VerCors: {A} Layered Approach to Practical Verification of Concurrent
               Software},
  booktitle = {{PDP}},
  pages     = {495--503},
  publisher = {{IEEE} Computer Society},
  year      = {2016},
  url       = {https://ieeexplore.ieee.org/abstract/document/7445381}
}

@inproceedings{DBLP:journals/corr/OortwijnBH16,
  author    = {Wytse Oortwijn and Stefan Blom and Marieke Huisman},
  title     = {Future-based Static Analysis of Message Passing Programs},
  booktitle = {{PLACES}},
  series    = {{EPTCS}},
  volume    = {211},
  pages     = {65--72},
  year      = {2016},
  url       = {https://arxiv.org/abs/1606.05942}
}

@MastersThesis{essay71180,
 month      = {November},
 title      = {Reasoning about Active Object Programs},
 author     = {J. {Zeilstra}},
 year       = {2016},
 url        = {http://essay.utwente.nl/71180/},
 abstract   = {Proving the correctness is important to ensure faultless functionality. To prove the correctness of Active Object programs in Java, this research translates them to message passing programs.
Active Object are not a build-in feature of the Java programming language. For asynchronous method calls, we used the Java Future interface to return result values. We created a formal specification for the Java Future interface and proved a simple implementation correct using the VerCors tool set.
We implemented the communication to Active Objects using message passing with the MPJ Express library. To verify this implementation, the message passing library has been annotated and a definition of valid messages in this program is given. We also annotated our implementation, however we encountered problems annotating the returning of result values. The annotations require a lot of administrative overhead and are hard to get correct. 
Also the existing VerCors tool set is not capable yet to automatically verify the program, mainly because it lacks support for output parameters or sum notation in the process algebra for futures.}
}

Proving the correctness is important to ensure faultless functionality. To prove the correctness of Active Object programs in Java, this research translates them to message passing programs. Active Object are not a build-in feature of the Java programming language. For asynchronous method calls, we used the Java Future interface to return result values. We created a formal specification for the Java Future interface and proved a simple implementation correct using the VerCors tool set. We implemented the communication to Active Objects using message passing with the MPJ Express library. To verify this implementation, the message passing library has been annotated and a definition of valid messages in this program is given. We also annotated our implementation, however we encountered problems annotating the returning of result values. The annotations require a lot of administrative overhead and are hard to get correct. Also the existing VerCors tool set is not capable yet to automatically verify the program, mainly because it lacks support for output parameters or sum notation in the process algebra for futures.

@inproceedings{Kandziora:2015:RAC:2786536.2786541,
 author = {Kandziora, Jorne and Huisman, Marieke and Bockisch, Christoph and Zaharieva-Stojanovski, Marina},
 title = {Run-time Assertion Checking of JML Annotations in Multithreaded Applications with e-OpenJML},
 booktitle = {Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs},
 series = {FTfJP '15},
 year = {2015},
 isbn = {978-1-4503-3656-7},
 location = {Prague, Czech Republic},
 pages = {8:1--8:6},
 articleno = {8},
 numpages = {6},
 url = {http://doi.acm.org/10.1145/2786536.2786541},
 doi = {10.1145/2786536.2786541},
 acmid = {2786541},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

@Article{Huisman2015,
author={Huisman, Marieke and Klebanov, Vladimir and Monahan, Rosemary},
title="VerifyThis 2012",
journal="International Journal on Software Tools for Technology Transfer",
year="2015",
month="Nov",
day="01",
volume="17",
number="6",
pages="647--657",
abstract="VerifyThis 2012 was a 2-day verification competition that took place as part of the International Symposium on Formal Methods (FM 2012) on August 30--31, 2012, in Paris, France. It was the second installment in the VerifyThis series. After the competition, an open call solicited contributions related to the VerifyThis 2012 challenges and overall goals. As a result, seven papers were submitted and, after review and revision, included in this special issue. In this introduction to the special issue, we provide an overview of the VerifyThis competition series, an account of related activities in the area, and an overview of solutions submitted to the organizers both during and after the 2012 competition. We conclude with a summary of results and some remarks concerning future installments of VerifyThis.",
issn="1433-2787",
doi="10.1007/s10009-015-0396-8",
url="https://doi.org/10.1007/s10009-015-0396-8"
}

VerifyThis 2012 was a 2-day verification competition that took place as part of the International Symposium on Formal Methods (FM 2012) on August 30–31, 2012, in Paris, France. It was the second installment in the VerifyThis series. After the competition, an open call solicited contributions related to the VerifyThis 2012 challenges and overall goals. As a result, seven papers were submitted and, after review and revision, included in this special issue. In this introduction to the special issue, we provide an overview of the VerifyThis competition series, an account of related activities in the area, and an overview of solutions submitted to the organizers both during and after the 2012 competition. We conclude with a summary of results and some remarks concerning future installments of VerifyThis.

@inproceedings{BlomDH15,
    Author = {S. Blom and S. Darabi and M. Huisman},
    Booktitle = FASE,
    Pages = {202--217},
    Series = lncs,
    Title = {{Verification of Loop Parallelisations}},
    Volume = {9033},
    Year = {2015},
    url = {https://link.springer.com/chapter/10.1007/978-3-662-46675-9_14}
}

@inproceedings{BlomHZ15,
    Author      = {Blom, S. and Huisman, M. and Zaharieva-Stojanovski, M.},
    Booktitle   = SEFM,
    Title       = {History-based verification of functional behaviour of concurrent programs},
    Year        = {2015},
    url         = {https://link.springer.com/chapter/10.1007/978-3-319-22969-0_6}
}

@article{DBLP:journals/corr/AmighiHHH14,
  author    = {Afshin Amighi and
               Christian Haack and
               Marieke Huisman and
               Cl{\'{e}}ment Hurlin},
  title     = {Permission-Based Separation Logic for Multithreaded Java Programs},
  journal   = {Logical Methods in Computer Science},
  volume    = {11},
  number    = {1},
  year      = {2015},
  url       = {https://lmcs.episciences.org/998}
}

@article{DBLP:journals/sttt/BlomH15,
  author    = {Stefan Blom and Marieke Huisman},
  title     = {Witnessing the elimination of magic wands},
  journal   = {{STTT}},
  volume    = {17},
  number    = {6},
  pages     = {757--781},
  year      = {2015},
  url       = {https://link.springer.com/article/10.1007/s10009-015-0372-3}
}
    

@phdthesis{Zaharieva15,
    Author = {M. Zaharieva-Stojanovski},
    Doi = {10.3990/1.9789036539241},
    Number = {15-375},
    School = {University of Twente},
    Series = {CTIT Ph.D. Thesis Series},
    Title = {{Closer to Reliable Software: Verifying Functional Behaviour of Concurrent Programs}},
    Year = {2015},
    url     = {https://research.utwente.nl/en/publications/closer-to-reliable-software-verifying-functional-behaviour-of-con},
    Bdsk-Url-1 = {https://doi.org/10.3990/1.9789036539241}
}
    

@article{BlomHM14,
    Author      = {S. Blom and M. Huisman and M. Mihel\v{c}i\'{c}},
    Issn        = {0167-6423},
    Issue       = {part 3},
    Journal     = scp,
    Pages       = {376--388},
    Publisher   = elsevier,
    Title       = {{Specification and Verification of {GPGPU} Programs}},
    Volume      = 95,
    Year        = {2014},
    url         = {https://www.sciencedirect.com/science/article/pii/S0167642314001531}
}

@inproceedings{DBLP:conf/fm/BlomH14,
  author    = {Stefan Blom and Marieke Huisman},
  title     = {The VerCors Tool for Verification of Concurrent Programs},
  booktitle = {{FM}},
  series    = {Lecture Notes in Computer Science},
  volume    = {8442},
  pages     = {127--131},
  publisher = {Springer},
  year      = {2014},
  url       = {https://link.springer.com/chapter/10.1007/978-3-319-06410-9_9}
}

@inproceedings{DBLP:conf/sfm/AmighiBDHMZ14,
  author    = {Afshin Amighi and Stefan Blom and Saeed Darabi and Marieke Huisman and Wojciech Mostowski and Marina Zaharieva{-}Stojanovski},
  title     = {Verification of Concurrent Systems with VerCors},
  booktitle = {{SFM}},
  series    = {Lecture Notes in Computer Science},
  volume    = {8483},
  pages     = {172--216},
  publisher = {Springer},
  year      = {2014},
  url       = {https://link.springer.com/chapter/10.1007/978-3-319-07317-0_5}
}

@inproceedings{AmighiAPLAS,
    Author      = {A. Amighi and S. Blom and M. Huisman},
    Booktitle   = {APLAS},
    Pages       = {255--274},
    Title       = {Resource Protection Using Atomics - Patterns and Verification},
    Year        = {2014},
    url         = {https://research.utwente.nl/en/publications/resource-protection-using-atomics-patterns-and-verifications}
    }
    

@inproceedings{DBLP:conf/fase/Zaharieva-StojanovskiH14,
  author    = {Marina Zaharieva{-}Stojanovski and
               Marieke Huisman},
  title     = {Verifying Class Invariants in Concurrent Programs},
  booktitle = {{FASE}},
  series    = {Lecture Notes in Computer Science},
  volume    = {8411},
  pages     = {230--245},
  publisher = {Springer},
  year      = {2014},
  url       = {https://link.springer.com/chapter/10.1007/978-3-642-54804-8_16}
}

@inproceedings{AmighiBHZ12,
    Author = {A. Amighi and Blom, S. and Huisman, M. and Zaharieva-Stojanovski, M.},
    Booktitle = {PLPV},
    Pages = {71--82},
    Publisher = {ACM},
    Title = {The {VerCors} Project: Setting Up Basecamp},
    Year = "2012",
    url_Link = {https://doi.org/10.1145/2103776.2103785}
}

@article{Haack76303,
    Author      = {C. Haack and M. Huisman and C. Hurlin},
    Journal     = {Nieuwsbrief van de Nederlandse Vereniging voor Theoretische Informatica},
    Pages       = {13--23},
    Publisher   = {Nederlandse Vereniging voor Theoretische Informatica},
    Title       = {Permission-Based Separation Logic for Multithreaded Java Programs},
    Volume      = {15},
    Year        = {2011},
    url         = {https://research.utwente.nl/en/publications/permission-based-separation-logic-for-multi-threaded-java-program}
    }

@phdthesis{DBLP:phd/hal/Hurlin09,
  author    = {Cl{\'{e}}ment Hurlin},
  title     = {Specification and Verification of Multithreaded Object-Oriented Programs
               with Separation Logic. (Sp{\'{e}}cification et v{\'{e}}rification
               de programmes orient{\'{e}}s objets en logique de s{\'{e}}paration)},
  school    = {University of Nice Sophia Antipolis, France},
  year      = {2009},
  url       = {https://tel.archives-ouvertes.fr/tel-00424979},
  timestamp = {Fri, 15 Jul 2016 22:10:33 +0200},
  biburl    = {https://dblp.org/rec/bib/phd/hal/Hurlin09},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/jot/HaackH09,
  author    = {Christian Haack and Cl{\'{e}}ment Hurlin},
  title     = {Resource Usage Protocols for Iterators},
  journal   = {Journal of Object Technology},
  volume    = {8},
  number    = {4},
  pages     = {55--83},
  year      = {2009},
  url       = {https://doi.org/10.5381/jot.2009.8.4.a3},
  doi       = {10.5381/jot.2009.8.4.a3},
  timestamp = {Fri, 26 May 2017 22:54:46 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/jot/HaackH09},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/amast/HaackH08,
  author    = {Christian Haack and Cl{\'{e}}ment Hurlin},
  title     = {Separation Logic Contracts for a Java-Like Language with Fork/Join},
  booktitle = {Algebraic Methodology and Software Technology, 12th International
               Conference, {AMAST} 2008, Urbana, IL, USA, July 28-31, 2008, Proceedings},
  pages     = {199--215},
  year      = {2008},
  crossref  = {DBLP:conf/amast/2008},
  url       = {https://doi.org/10.1007/978-3-540-79980-1\_16},
  doi       = {10.1007/978-3-540-79980-1\_16},
  timestamp = {Tue, 14 May 2019 10:00:38 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/amast/HaackH08},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}