skip to main content
10.1145/1292597.1292598acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
Article

Jessie: an intermediate language for Java and C verification

Published: 02 October 2007 Publication History

Abstract

The Why platform is aimed at proving behavioral properties of both Java and C source code. Both C and Java source are indeed first translated into an intermediate language called Jessie, designed for verification purposes. We present the various features of this language, we show why those features are suitable for verification, and finally how C and Java are translated into it.

Reference

[1]
Jean-Christophe Filliâtre and Claude Marché. The Why/Krakatoa/Caduceus platform for deductive program verification. In Werner Damm and Holger Hermanns, editors, 19th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Berlin, Germany, July 2007. Springer.

Cited By

View all
  • (2022)Dijkstra’s Legacy on Program VerificationEdsger Wybe Dijkstra10.1145/3544585.3544593(105-140)Online publication date: 12-Jul-2022
  • (2014)Formal Verification of kLIBC with the WP Frama-C Plug-inProceedings of the 6th International Symposium on NASA Formal Methods - Volume 843010.1007/978-3-319-06200-6_29(343-358)Online publication date: 29-Apr-2014
  • (2010)Program verification in SPARK and ACSLProceedings of the 15th Ada-Europe international conference on Reliable Software Technologies10.1007/978-3-642-13550-7_7(97-110)Online publication date: 14-Jun-2010

Index Terms

  1. Jessie: an intermediate language for Java and C verification

      Recommendations

      Comments

      Information & Contributors

      Information

      Published In

      cover image ACM Conferences
      PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verification
      October 2007
      76 pages
      ISBN:9781595936776
      DOI:10.1145/1292597
      Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

      Sponsors

      Publisher

      Association for Computing Machinery

      New York, NY, United States

      Publication History

      Published: 02 October 2007

      Permissions

      Request permissions for this article.

      Check for updates

      Author Tags

      1. behavioral properties
      2. verification
      3. verification conditions generator

      Qualifiers

      • Article

      Conference

      ICFP07
      Sponsor:

      Acceptance Rates

      PLPV '07 Paper Acceptance Rate 6 of 8 submissions, 75%;
      Overall Acceptance Rate 18 of 25 submissions, 72%

      Upcoming Conference

      POPL '26

      Contributors

      Other Metrics

      Bibliometrics & Citations

      Bibliometrics

      Article Metrics

      • Downloads (Last 12 months)1
      • Downloads (Last 6 weeks)0
      Reflects downloads up to 14 Feb 2025

      Other Metrics

      Citations

      Cited By

      View all
      • (2022)Dijkstra’s Legacy on Program VerificationEdsger Wybe Dijkstra10.1145/3544585.3544593(105-140)Online publication date: 12-Jul-2022
      • (2014)Formal Verification of kLIBC with the WP Frama-C Plug-inProceedings of the 6th International Symposium on NASA Formal Methods - Volume 843010.1007/978-3-319-06200-6_29(343-358)Online publication date: 29-Apr-2014
      • (2010)Program verification in SPARK and ACSLProceedings of the 15th Ada-Europe international conference on Reliable Software Technologies10.1007/978-3-642-13550-7_7(97-110)Online publication date: 14-Jun-2010

      View Options

      Login options

      View options

      PDF

      View or Download as a PDF file.

      PDF

      eReader

      View online with eReader.

      eReader

      Figures

      Tables

      Media

      Share

      Share

      Share this Publication link

      Share on social media