Verifying a Radio Telescope Pipeline Using HaliVer: Solving Nonlinear and Quantifier Challenges. van den Haak, L. B., Wijs, A., Huisman, M., & van den Brand, M. In Haxthausen, A. E. & Serwe, W., editors, Formal Methods for Industrial Critical Systems, pages 152–169, Cham, 2024. Springer Nature Switzerland. doi abstract bibtex 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{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"
}
Downloads: 0
{"_id":"cg9nBjyZu9Yxdp4cj","bibbaseid":"vandenhaak-wijs-huisman-vandenbrand-verifyingaradiotelescopepipelineusinghaliversolvingnonlinearandquantifierchallenges-2024","author_short":["van den Haak, L. B.","Wijs, A.","Huisman, M.","van den Brand, M."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":["van","den"],"lastnames":["Haak"],"firstnames":["Lars","B."],"suffixes":[]},{"propositions":[],"lastnames":["Wijs"],"firstnames":["Anton"],"suffixes":[]},{"propositions":[],"lastnames":["Huisman"],"firstnames":["Marieke"],"suffixes":[]},{"propositions":["van","den"],"lastnames":["Brand"],"firstnames":["Mark"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Haxthausen"],"firstnames":["Anne","E."],"suffixes":[]},{"propositions":[],"lastnames":["Serwe"],"firstnames":["Wendelin"],"suffixes":[]}],"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","bibtex":"@InProceedings{Haak24FMICS,\nauthor=\"van den Haak, Lars B.\nand Wijs, Anton\nand Huisman, Marieke\nand van den Brand, Mark\",\neditor=\"Haxthausen, Anne E.\nand Serwe, Wendelin\",\ntitle=\"Verifying a Radio Telescope Pipeline Using HaliVer: Solving Nonlinear and Quantifier Challenges\",\nbooktitle=\"Formal Methods for Industrial Critical Systems\",\nyear=\"2024\",\npublisher=\"Springer Nature Switzerland\",\naddress=\"Cham\",\npages=\"152--169\",\nabstract=\"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.\",\nisbn=\"978-3-031-68150-9\",\ndoi=\"10.1007/978-3-031-68150-9_9\"\n}\n\n","author_short":["van den Haak, L. B.","Wijs, A.","Huisman, M.","van den Brand, M."],"editor_short":["Haxthausen, A. E.","Serwe, W."],"key":"Haak24FMICS","id":"Haak24FMICS","bibbaseid":"vandenhaak-wijs-huisman-vandenbrand-verifyingaradiotelescopepipelineusinghaliversolvingnonlinearandquantifierchallenges-2024","role":"author","urls":{},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/utwente-fmt/vercors-web/master/static/references.bib","dataSources":["cCvCnPTRQYq3qPe9y"],"keywords":[],"search_terms":["verifying","radio","telescope","pipeline","using","haliver","solving","nonlinear","quantifier","challenges","van den haak","wijs","huisman","van den brand"],"title":"Verifying a Radio Telescope Pipeline Using HaliVer: Solving Nonlinear and Quantifier Challenges","year":2024}