On the Industrial Application of Critical Software Verification with VerCors.
Huisman, M.; and Monti, R. E.
In Margaria, T.; and Steffen, B., editor(s),
Leveraging Applications of Formal Methods, Verification and Validation: Applications, pages 273–292, Cham, 2020. Springer International Publishing
![On the Industrial Application of Critical Software Verification with VerCors [link]](//bibbase.org/img/filetypes/link.svg "Paper")
Paper
link
bibtex
abstract
5 downloads
@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.
A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms.
Safari, M.; and Huisman, M.
In Dongol, B.; and Troubitsyna, E., editor(s),
Integrated Formal Methods - 16th International Conference, IFM 2020, Lugano, Switzerland, November 16-20, 2020, Proceedings, of
Lecture Notes in Computer Science, pages 257–275, Singapore, November 2020. Springer Singapore
16th International Conference on Integrated Formal Methods, IFM 2020, IFM 2020 ; Conference date: 16-11-2020 Through 20-11-2020
Paper
doi
link
bibtex
abstract
1 download
@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.
Formal Methods for GPGPU Programming: Is the Demand Met?.
van den Haak , L.; Wijs, A.; van den Brand , M.; and Huisman, M.
In Dongol, B.; and Troubitsyna, E., editor(s),
Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings, of
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pages 160–177, Germany, 2020. Springer
16th International Conference on Integrated Formal Methods, IFM 2020 ; Conference date: 16-11-2020 Through 20-11-2020
Paper
doi
link
bibtex
abstract
@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.
Verification and Validation of Concurrent and Distributed Systems (Track Summary).
Huisman, M.; and Seceleanu, C.
In Margaria, T.; and Steffen, B., editor(s),
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, of
Lecture Notes in Computer Science, pages 421–425, Singapore, 2020. Springer Singapore
9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, ISoLA 2020 ; Conference date: 20-10-2020 Through 30-10-2020
Paper
doi
link
bibtex
abstract
@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.
The VerifyThis Collaborative Long Term Challenge.
Huisman, M.; Monti, R.; Ulbrich, M.; and Weigl, A.
In Ahrendt, W.; Beckert, B.; Bubel, R.; Hähnle, R.; and Ulbrich, M., editor(s),
Deductive Software Verification: Future Perspectives, of
Lecture Notes in Computer Science, pages 246–260, Singapore, December 2020. Springer Singapore
Paper
doi
link
bibtex
abstract
@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.
Automated Verification of Parallel Nested DFS.
Oortwijn, W.; Huisman, M.; Joosten, S. J. C.; and van de Pol, J.
In Biere, A.; and Parker, D., editor(s),
Tools and Algorithms for the Construction and Analysis of Systems, pages 247–265, Cham, 2020. Springer International Publishing
link
bibtex
abstract
@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.
Practical Abstractions for Automated Verification of Shared-Memory Concurrency.
Oortwijn, W.; Gurov, D.; and Huisman, M.
In Beyer, D.; and Zufferey, D., editor(s),
Verification, Model Checking, and Abstract Interpretation, pages 401–425, Cham, 2020. Springer International Publishing
link
bibtex
abstract
1 download
@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.
Extending support for axiomatic data types in VerCors.
Şakar, Ö.
Master's thesis, April 2020.
Paper
link
bibtex
abstract
@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.
Improving Support for Java Exceptions and Inheritance in VerCors.
Rubbens, R.
Master's thesis, May 2020.
Paper
link
bibtex
abstract
2 downloads
@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.
![Exploring annotations for deductive verification [pdf]](http://bibbase.org/img/filetypes/pdf.svg "Paper")
![The Integration of Testing and Program Verification [link]](http://bibbase.org/img/filetypes/link.svg "Paper")
Paper
doi
link
bibtex