Logo des Repositoriums

Auflistung nach Schlagwort "Theorem Proving"

1 - 3 von 3
  • Konferenzbeitrag
    Formal Verification of Intelligent Hybrid Systems that are modeled with Simulink and the Reinforcement Learning Toolbox
    (Software Engineering 2023, 2023) Adelt, Julius; Liebrenz, Timm; Herber, Paula
    Reinforcement Learning (RL) is a powerful technique to control intelligent hybrid systems (HS) in dynamic and uncertain environments. However, formally guaranteeing safe behavior of intelligent HS is hard because formal descriptions are often not available in industrial design processes and hard to obtain for RL. Furthermore, the intertwined discrete and continuous behavior of hybrid systems results in limited scalability of automatic verification methods, such as model checking. This makes deductive verification desirable. In this paper, we summarize our approach for deductive verification of intelligent HS with embedded RL components that are modeled with Simulink and the RL Toolbox. This paper was originally published at the Formal Methods conference 2021 (FM21) [ALH21].
  • Zeitschriftenartikel
    Higher-order theorem proving and its applications
    (it - Information Technology: Vol. 61, No. 4, 2019) Steen, Alexander
    Automated theorem proving systems validate or refute whether a conjecture is a logical consequence of a given set of assumptions. Higher-order provers have been successfully applied in academic and industrial applications, such as planning, software and hardware verification, or knowledge-based systems. Recent studies moreover suggest that automation of higher-order logic, in particular, yields effective means for reasoning within expressive non-classical logics, enabling a whole new range of applications, including computer-assisted formal analysis of arguments in metaphysics. My work focuses on the theoretical foundations, effective implementation and practical application of higher-order theorem proving systems. This article briefly introduces higher-order reasoning in general and presents an overview of the design and implementation of the higher-order theorem prover Leo-III. In the second part, some example applications of Leo-III are discussed.
  • Workshopbeitrag
    Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY
    (Software Engineering and Software Management 2019, 2019) Knüppel, Alexander; Thüm, Thomas; Pardylla, Carsten Immanuel; Schaefer, Ina
    As formal verification of software systems is a complex task comprising many algorithms and heuristics, modern theorem provers offer numerous parameters that are to be selected by a user to control how a piece of software is verified. Evidently, the number of parameters even increases with each new release. One challenge is that default parameters are often insufficient to close proofs automatically and are not optimal in terms of verification effort. The verification phase becomes hardly accessible for non-experts, who typically must follow a time-consuming trial-and-error strategy to choose the right parameters even for trivial pieces of software. To aid users of deductive verification, we apply machine learning techniques to empirically investigate which parameters and combinations thereof impair or improve provability and verification effort. We exemplify our procedure on the deductive verification system KeY 2.6.1 and specified extracts of OpenJDK, and formulate 53 hypotheses of which only three have been rejected. We identified parameters that represent a trade-off between high provability and low verification effort, enabling the possibility to prioritize the selection of a parameter for either direction. Our insights give tool builders a better understanding of their control parameters and constitute a stepping stone towards automated deductive verification and better applicability of verification tools for non-experts.