2012 | OriginalPaper | Buchkapitel
A Comparison of Intermediate Verification Languages: Boogie and Sireum/Pilar
verfasst von : Loren Segal, Patrice Chalin
Erschienen in: Verified Software: Theories, Tools, Experiments
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Use of contract-based specification languages is slowly increasing. This advancement has been due in part to the growing efficiency and usefulness of Intermediate Verification Languages (IVLs) which abstract the low level details of program verification and act as a backbone for higher level tools. This paper looks at two mature IVLs, Boogie and Sireum/Pilar, and provides a comparative study of their features in order to offer resources for tool developers and IVL designers. As validation for this comparison, we introduce two tools,
ruby
2
boogie
and
ruby
2
pilar
, to illustrate the translation from Ruby to Boogie and Pilar.