As of **version 1.0** Pegasus implements a number of methods for generating inductive invariants
for continuous systems.

The method of barrier certificates is
a popular and promising technique for safety verification of continuous
systems. It employs Lyapunov-like differential inequalities and typically
requires a *polynomial template* which is then transformed into a
constraint problem in the template coefficient variables. If the constraint is
feasible, a real-valued polynomial
$B\left(\mathbf{x}\right)$
can be synthesized from the feasible point, with the property that
$B\left(\mathbf{x}\right)\le 0$
defines a continuous invariant of the system which separates the initial states
of the system from states that are deemed unsafe. There are many different
flavors of barrier certificates in the verification literature. A systematic
development of the barrier certificate method and its integration with a sound
theorem proving system is one of the goals behind developing Pegasus. As part
of this effort, a generalization called vector barrier certificates
was developed at the *Logical Systems Lab* in collaboration with *Inria*,
which is based on the theory of *comparison systems* and serves to organize
existing notions of barrier certificates under a unified framework.

Polynomials
$p$
satisfying the differential equation
$p\text{'}=\alpha p$
where
$\alpha $
is also a polynomial are known as Darboux polynomials, named after Gaston Darboux who introduced them as a tool to study integrability.

First integrals, also known as *conserved quantities*, or *constants of motion*, are functions
of state whose value remains constant as the system evolves. In other words, a first integral is a function
whose time derivative is zero. In general, first integrals can be very complicated functions and can be
extremely difficult to find. However, searching for *polynomial* first integrals is straightforward
and can be achieved using a polynomial template and a solver for systems of linear equations.

Qualitative abstraction of continuous systems is related to *predicate abstraction*. It produces a
*discrete abstraction* by partitioning the state space of a continuous system using predicates
that represent significant ``qualitative information'' about the system. If the set of predicates used
for the abstraction is ``good'', many interesting properties about the behavior of the continuous
system may be proved.
The idea of qualitative abstraction originally emerged in the field of Artificial Intelligence in the
1980s and was used for *qualitative simulation* and *qualitative reasoning* about physical systems. Later
work in this field in the 1990s considered verification of termporal properties of physical systems
as an application of this technique. Within the verification community, qualitative abstraction was
advanced in the work of A. Tiwari and was employed in tools such as HybridSAL from SRI International
to enable model checking hybrid systems.

Pegasus implements *strategies* that generate invariants by combining invariant generation methods in a *differential saturation loop*, refining the evolution constraint at each step.