CMU-CS-14-140
Computer Science Department
School of Computer Science, Carnegie Mellon University


CMU-CS-14-140

A Hierarchy of Proof Rules for
Checking Differential Invariance of Algebraic Sets

Khalil Ghorbal, Andrew Sogokon*, André Platzer

November 2014

CMU-CS-14-140.pdf


To appear in the
Proceedings of the 16th International Conference on
Verification, Model Checking, and Abstract Interpretation (VMCAI 2015),
12-14 January 2015, Mumbai, India.


Keywords: Algebraic invariant, deductive power, hierarchy, proof rules, differential equation, abstraction, continuous dynamics, formal verification, hybrid system

This paper presents a theoretical and experimental comparison of sound proof rules for proving invariance of algebraic sets, that is, sets satisfying polynomial equalities, under the flow of polynomial ordinary differential equations. Problems of this nature arise in formal verification of continuous and hybrid dynamical systems, where there is an increasing need for methods to expedite formal proofs. We study the trade-off between proof rule generality and practical performance and evaluate our theoretical observations on a set of heterogeneous benchmarks. The relationship between increased deductive power and running time performance of the proof rules is far from obvious; we discuss and illustrate certain classes of problems where this relationship interesting.

31 pages

*University of Edinburgh, LFCS, School of Informatics, Edinburgh, Scotland

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by [email protected]