Open AccessARCH-COMP21 Category Report: Hybrid Systems Theorem Proving
Author(s) -
Stefan Mitsch,
Xiangyu Jin,
Bohua Zhan,
Shuling Wang,
Naijun Zhan
Publication year - 2021
Publication title -
epic series in computing
Language(s) - English
Resource type - Conference proceedings
ISSN - 2398-7340
DOI - 10.29007/35cf
Subject(s) - automated theorem proving , programming language , computer science , hybrid system , scripting language , semantics (computer science) , set (abstract data type) , parametric statistics , benchmark (surveying) , proof assistant , equational logic , proof theory , theoretical computer science , algorithm , mathematics , mathematical proof , machine learning , rewriting , statistics , geometry , geodesy , geography
This paper reports on the Hybrid Systems Theorem Proving (HSTP) category in the ARCH-COMP Friendly Competition 2021. The characteristic features of the HSTP cate- gory remain as in the previous editions [MST+18, MST+19, MMJ+20], it focuses on flexi- bility 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 verifica- tion from proof hints, proof checking from scripted tactics. This instance of the competition introduces extensions to the scripting language, a comparison of the influence of arithmetic backend versions on verification performance in KeYmaera X, as well as improvements in the HHL Prover.