Abstract
This paper reports on the Hybrid Systems Theorem Proving (HSTP) category in the ARCH-COMP Friendly Competition 2022. The characteristic features of the HSTP category remain as in the previous editions [MST+ 18, MST+ 19, MMJ+ 20], it focuses on flexibility of programming languages as structuring principles for hybrid systems, unambiguity and precision of program semantics, and mathematical rigor of logical reasoning principles. The benchmark set includes nonlinear and parametric continuous and hybrid systems and hybrid games, each in three modes: fully automatic verification, semi-automatic verification from proof hints, proof checking from scripted tactics. This instance of the competition focuses on presenting the differences between the provers on a subset of the benchmark examples.
| Originalsprog | Engelsk |
|---|---|
| Tidsskrift | EPiC Series in Computing |
| Vol/bind | 90 |
| Sider (fra-til) | 185-203 |
| DOI | |
| Status | Udgivet - 2022 |
| Begivenhed | 9th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH 2022 - Munich, Tyskland Varighed: 5 sep. 2022 → 5 sep. 2022 |
Konference
| Konference | 9th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH 2022 |
|---|---|
| Land/Område | Tyskland |
| By | Munich |
| Periode | 05/09/2022 → 05/09/2022 |
Bibliografisk note
Funding Information:Acknowledgments. This material is based upon work supported by the AFOSR under grant number FA9550-16-1-0288, and by the United States Air Force and DARPA under Contract No. FA8750-18-C-0092. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the United States Air Force and DARPA. We thank the entire Logical Systems Lab at Carnegie Mellon University for their many contributions and suggestions to KeYmaera X and its associated tools. Alexander Bentkamp is supported by a Chinese Academy of Sciences President’s International Fellowship for Postdoctoral Researchers under grant No. 2021PT0015. Xiangyu Jin, Bohua Zhan, Huanhuan Sheng and Shuling Wang are funded partly by NSFC under grant No. 61625206, 61732001, 62032024 and 61972385. Jonathan Julián Huerta y Munive is supported by a Novo Nordisk Fonden Start Package Grant (NNF20OC0063462).
Publisher Copyright:
© 2022, EasyChair. All rights reserved.