Share on Facebook Tweet on Twitter Share on LinkedIn Share by email

This is where programs begin. Jennisys is a programming language that emphasizes clean public interfaces and lets programmers describe the data structures they intend a private implementation to use. Code is underemphasized, and Jennisys attempts to synthesize code automatically from the public interface and the given data-structure description.

Source and Tool

Jennisys is available as open source in the Boogie source repository, in the Jennisys directory.  It is written in F# and it makes use of Dafny, which in turn rests on Boogie and Z3.


  • K. Rustan M. Leino
  • Aleksandar Milicevic (MIT)


  • Program Extrapolation with Jennisys.  K. Rustan M. Leino and Aleksandar Milicevic.  (This is a newer version of the Technical Report below.)  To appear, OOPSLA 2012.