A Method for Invariant Generation for Polynomial Continuous Systems
- Submitting institution
-
University of Edinburgh
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 59038554
- Type
- E - Conference contribution
- DOI
-
10.1007/978-3-662-49122-5_13
- Title of conference / published proceedings
- Verification, Model Checking, and Abstract Interpretation : 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings
- First page
- 268
- Volume
- 9583
- Issue
- -
- ISSN
- 0302-9743
- Open access status
- Out of scope for open access requirements
- Month of publication
- December
- Year of publication
- 2015
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
3
- Research group(s)
-
C - Foundations of Computation
- Citation count
- 18
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Improved automatic invariant generation techniques are key to broadening the practical capabilities of formal verification tools for checking safety properties of continuous and hybrid dynamical systems. Experiments on a set of 100 problems demonstrate that the novel approach presented can exhibit order-of-magnitude performance improvement over naive techniques. The reported work was developed into a central component of the invariant generation tool Pegasus, which won the Best Tool Paper Award at Formal Methods 2019. Pegasus is integrated with KeYmaera X, the current leading theorem prover for formal semi-automated reasoning about continuous and hybrid systems.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -