Skip to content
Branch: master
Go to file

Latest commit


Failed to load latest commit information.
Latest commit message
Commit time

JKind for Eclipse

Lustre Plug-in for Eclipse with JKind Analysis Support

This plug-in provides a Lustre front-end in Eclipse with syntax checking, highlighting, type checking, and other syntatic checks. The plug-in also provides a convenient way to launch JKind on a Lustre file and have the results reported back in a real-time graphical display. Excel formatted counterexamples are viewable by right-clicking on individual properties.

JKind itself is now bundled into the plug-in, so no separate installation is needed.

Quick Install

Use the update site

Detailed Install

  1. Download and install Eclipse.

  2. From the Eclipse "Help" menu select "Install New Software...".

install new software

  1. In the "Available Software" dialog click the "Add..." button.


  1. In the "Add Repository" dialog enter the name JKind-Xtext and the location Click "OK".

add repository

  1. In the "Available Software" dialog open the "Uncategorized" menu and select "JKind for Eclipse". Click "Next" and follow the prompts.

select jkind for eclipse


To update the plug-in, select "Check for Updates" from the Eclipse "Help" menu.

check for updates

Usage Examples

Right click in a Lustre file to run JKind and examine the results:

Syntax checking, type checking, and other static checks are all done on the fly:

Type error

Many other Eclipse-style features are available. For example, variables and fields can be easily renamed:

Rename Element


Lustre Plug-in for Eclipse with JKind Analysis Support



You can’t perform that action at this time.