Verification of real-time systems using linear relation analysis
Linear Relation Analysis [11] is an abstract interpretation devoted to the automatic discovery of invariant linear inequalities among numerical variables of a program. In this paper, we apply such an analysis to the verification of quantitative time properties of two kinds of systems: synchronous programs and linear hybrid systems.
abstract interpretation hybrid systems convex polyhedra real time systems synchronous languages