Hierarchic Superposition with Weak Abstraction

Baumgartner, Peter; Waldmann, Uwe

doi:10.1007/978-3-642-38574-2_3

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

Hierarchic Superposition with Weak Abstraction

MPS-Authors

/persons/resource/persons45689

Waldmann, Uwe
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Baumgartner, P., & Waldmann, U. (2013). Hierarchic Superposition with Weak Abstraction. In M. P. Bonacina (Ed.), Automated Deduction - CADE-24 (pp. 39-57). Berlin: Springer. doi:10.1007/978-3-642-38574-2_3.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0024-6C42-F

Abstract

In this paper we study possibilities of using methods for hierarchical reasoning in local theory extensions for the analysis and verification of parametric hybrid systems, where the parameters can be either constants or functions. Our goal is to automatically provide guarantees that such systems satisfy certain safety or invariance conditions. We first analyze the possibility of automatically generating such guarantees in the form of constraints on parameters, then show that we can also synthesise so-called criticality functions, typically used for proving stability and/or safety of hybrid systems. We illustrate our methods on several examples.