Parametric systems: verification and synthesis
From MaRDI portal
Abstract: In this paper we study possibilities of using hierarchical reasoning, symbol elimination and model generation for the verification of parametric systems, where the parameters can be constants or functions. Our goal is to automatically provide guarantees that such systems satisfy certain safety or invariance conditions. We analyze the possibility of automatically generating such guarantees in the form of constraints on parameters. We illustrate our methods on several examples
Recommendations
- Hierarchical reasoning and model generation for the verification of parametric hybrid systems
- Hierarchical reasoning for the verification of parametric systems
- scientific article; zbMATH DE number 1796136
- Parameterized synthesis with safety properties
- Model checking and abstraction to the aid of parameterized systems (a survey)
Cited in
(9)- Parameterized synthesis with safety properties
- Universal invariant checking of parametric systems with quantifier-free SMT reasoning
- On invariant synthesis for parametric systems
- Parsimonious, Simulation Based Verification of Linear Systems
- Hierarchical reasoning and model generation for the verification of parametric hybrid systems
- Parameterized Synthesis
- Correct Hardware Design and Verification Methods
- Hierarchical reasoning for the verification of parametric systems
- On symbol elimination and uniform interpolation in theory extensions
This page was built for publication: Parametric systems: verification and synthesis
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5134273)
