Pegasus is a tool for generating continuous invariants for systems described
by polynomial ordinary differential equations. It is integrated with the KeYmaera X
theorem prover for hybrid systems and implements a number of methods for invariant generation.
Pegasus provides a framework for combining techniques for invariant generation into more
powerful strategies. The ultimate purpose is to improve the level of proof automation
in KeYmaera X and other deductive verification frameworks for hybrid systems.
In order to use Pegasus, one needs to have access to Mathematica and Matlab,
as well as a working installation of KeYmaera X.
Installation instructions:
Pegasus is implemented in Mathematica and is (optionally) able to make use of MATLAB for additional computations.
The simplest way to get started is:
 Ensure Mathematica version 10+ is installed on your system.
 Download and follow the installation instructions for KeYmaera X.
Pegasus works out of the box with KeYmaera X once Mathematica is configured properly.
To enable additional Pegasus functionality with MATLAB, additional packages are required.
 Ensure MATLAB version 2016+ is installed on your system.

Download MATLink from http://matlink.org/ and follow the "Link with MATLAB" instructions for your OS. Briefly:
 Run the following in Mathematica:
SystemOpen@FileNameJoin[{$UserBaseDirectory, "Applications"}]
and extract the contents of the downloaded MATLink into the folder opened by the above command (on Unixlike systems this folder is usually /home/.Mathematica/Applications, but the value of $UserBaseDirectory varies on different systems; see documentation).

Run the following in Mathematica:
Needs["MATLink`"]
OpenMATLAB[]

Go to http://matlink.org/troubleshooting/ for troubleshooting if the above commands return errors.
 Download SeDuMi and SOSTOOLS (on MacOS use tbxmanager to install SeDuMi; otherwise there is a missing dependency to some native .dylib),
 Unzip and add all subfolders to the MATLAB path by navigating to the MATLAB window menu and selecting Home > Set Path. Use "Add with Subfolders" and select the folders containing the unzipped SeDuMi and SOSTOOLS files, e.g.
/usr0/home/username/.Mathematica/Applications/SeDuMi_1_3
/usr0/home/username/.Mathematica/Applications/SOSTOOLS.303
Make sure to save your changes in order to add these folders to the path permanently.
Running Pegasus separately can be achieved by navigating to keymaeraxcore/src/main/resources/Pegasus inside the folder containing the KeYmaera X source directory. The file Pegasus.m serves as the main package from which invariant generation strategies may be called. Various examples of invariant generation using this file are contained in the Tests/ subfolder. Keep in mind that by running Pegasus separately using Mathematica one only obtains invariant candidates, whereas KeYmaera X additionally formally proves the invariance property of these candidates.
In Mathematica, an input problem for Pegasus takes the form of a continuous Hoare triple:
{precondition, {vector_field, state_variables, evolution_constraint}, postcondition}
where precondition, postcondition and evolution_constraint are firstorder formulas of real arithmetic, state_variables is a finite list of the system's state variables (e.g. {x,y,z}), and vector_field is a list of equal size containing polynomials in those variables (corresponding to the righthand side of the system of ODEs). For instance, when calling from a notebook file in the Test/ subfolder in the Pegasus main directory:
In[1] = SetDirectory[ParentDirectory[NotebookDirectory[]]] 
In[2] = Needs["Pegasus`", FileNameJoin[{Directory[], "Pegasus.m"}]] 
In[3] = InvGen[{(2 + x)^2 + y^2 <= 1/5  (2 + x)^2 + (2 + y)^2 <= 1/3, {{4 y, x}, {x, y}, True}, y <= 4 && y >= 4 && x^2 + y^2 > 1/3}] 
In the illustration of this verification problem below, the unsafe sets are shown in light red and the initial states in light green:
The output is a nested list, whose first formal entry is the invariant candidate (other entries in the list serve to facilitate proof construction within KeYmaera X and may be ignored when using Pegasus separately).
Out[4] = {{106345581/44105831 < x^2+4 y^2 < 784012261/25449817,{{x^2+4 y^2 < 784012261/25449817,kyx`ProofHint==kyx`FirstIntegral},{x^2+4 y^2 > 106345581/44105831,kyx`ProofHint==kyx`FirstIntegral}}},True}
When drawn, the invariant looks as follows (shown in light blue):
Some of the invariant generation methods currently implemented in Pegasus include:
 Barrier certificates (of various flavors),
 Darboux polynomials,
 Qualitative analysis.
Pegasus implements strategies that generate invariants by combining invariant generation methods in a differential saturation loop, refining the evolution constraint at each step.
Contributors: Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer.