LOOP

The LOOP compiler for Java and JML. This paper describes the architecture of the LOOP tool, which is used for reasoning about sequential Java. The LOOP tool translates Java and JML (a specification language tailored to Java) classes into their semantics in higher order logic. It serves as a front-end to a theorem prover in which the actual verification of the desired properties takes place. Also, the paper discusses issues related to logical theory generation.


References in zbMATH (referenced in 21 articles , 1 standard article )

Showing results 1 to 20 of 21.
Sorted by year (citations)

1 2 next

  1. da Costa, Umberto Souza; Moreira, Anamaria Martins; Musicante, Martin A.; Souza Neto, Plácido A.: JCML: A specification language for the runtime verification of Java card programs (2012)
  2. Liu, Zhiming; Morisset, Charles; Wang, Shuling: A graph-based implementation for mechanized refinement calculus of OO programs (2011)
  3. Mossakowski, Till; Schröder, Lutz; Goncharov, Sergey: A generic complete dynamic logic for reasoning about purity and effects (2010)
  4. Bertot, Yves: Theorem-proving support in programming language semantics (2009)
  5. da Costa, Umberto Souza; Martins Moreira, Anamaria; Musicante, Martin A.; Souza Neto, Plácido A.: Specification and runtime verification of Java card programs (2009)
  6. Henzinger, Thomas A.; Hottelier, Thibaud; Kovács, Laura: Valigator: A verification tool with bound and invariant generation (2008)
  7. Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto: A program logic for resources (2007)
  8. Chalin, Patrice: Are the logical foundations of verifying compiler prototypes matching user expectations? (2007)
  9. Robby; Rodríguez, Edwin; Dwyer, Matthew B.; Hatcliff, John: Checking JML specifications using an extensible software model checking framework (2006)
  10. Burdy, Lilian; Cheon, Yoonsik; Cok, David R.; Ernst, Michael D.; Kiniry, Joseph R.; Leavens, Gary T.; Leino, K.Rustan M.; Poll, Erik: An overview of JML tools and applications (2005)
  11. Burdy, Lilian; Cheon, Yoonsik; Cok, David R.; Ernst, Michael D.; Kiniry, Joseph R.; Leavens, Gary T.; Leino, K.Rustan M.; Poll, Erik: An overview of JML tools and applications (2005)
  12. Marché, Claude; Paulin-Mohring, Christine: Reasoning about Java programs with aliasing and frame conditions (2005)
  13. Pierik, Cees; De Boer, Frank S.: A proof outline logic for object-oriented programming (2005)
  14. Kreitz, Christoph: Building reliable, high-performance networks with the Nuprl proof development system (2004)
  15. Robby; Rodríguez, Edwin; Dwyer, Matthew B.; Hatcliff, John: Checking strong specifications using an extensible software model checking framework (2004)
  16. Jacobs, Bart; Poll, Erik: Coalgebras and monads in the semantics of Java (2003)
  17. Huisman, Marieke: Verification of Java’s AbstractCollection class: A case study (2002)
  18. Jacobs, Bart: A formalisation of Java’s exception mechanism (2001)
  19. Jacobs, Bart; Poll, Erik: A logic for the Java modeling language JML (2001)
  20. Meijer, Hans; Poll, Erik: Towards a full formal specification of the JavaCard API (2001)

1 2 next