Skip to content

Home

Jump to bottom
Iconmaster edited this page Oct 27, 2016 · 4 revisions

Welcome to the WhyR wiki!

What Is WhyR?

WhyR is a tool to convert programs written in LLVM IR into a model for an SMT solver. It translates programs into models, and also allows you to write annotations for the code, which is translated to goals. In addition, annotations can be automatically generated, using WhyR's runtime error annotation generation (aka RTE generation). Currently, the Why3 language is WhyR's output format.

Documentation

  • Installing WhyR
  • [Writing WhyR annotations](WhyR Metadata)
  • [Semantics of WhyR annotations](Annotation Syntax)
  • [Contributing to the project](Contributing To WhyR)

Take a look at the sidebar for more documentation on how to use WhyR.

This material is based upon work supported by the National Science Foundation under Grant No. ACI-1314674. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.

Clone this wiki locally