A Control Flow Graph Based Approach to Make the Verification of Cyber-Physical Systems Using KeYmaera Easier
KeYmaera is an interactive theorem prover and is used to verify safety properties of cyber-physical systems (CPSs). It implements a Dynamic Logic for Hybrid Programs (HPs), while a HP models a CPS very precisely. Verifying properties of a given system in KeYmaera can become a challenge for a user si...
Saved in:
Main Authors: | Thomas Baar, Sergey Staroletov |
---|---|
Format: | Article |
Language: | English |
Published: |
Yaroslavl State University
2018-10-01
|
Series: | Моделирование и анализ информационных систем |
Subjects: | |
Online Access: | https://www.mais-journal.ru/jour/article/view/752 |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Similar Items
-
Notes on Recent Achievements in Proving Stability using KeYmaeraX
by: Thomas Baar, et al.
Published: (2021-12-01) -
Verification of data integration in an integrated system of databases on the properties of inorganic substances and materials
by: S. A. Stupnikov
Published: (2025-07-01) -
CRITERION FOR IDENTIFICATION OF THE PROBABILITY MODEL OF THE STATE OF SATELLITE COMMUNICATION CHANNELS
by: G. I. Linets, et al.
Published: (2022-08-01) -
Safety Analysis of Longitudinal Motion Controllers during Climb Flight
by: Thomas Baar, et al.
Published: (2019-12-01) -
Ethereum Smart Contracts Under Scrutiny: A Survey of Security Verification Tools, Techniques, and Challenges
by: Mounira Kezadri Hamiaz, et al.
Published: (2025-06-01)