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 25 articles , 1 standard article )

Showing results 1 to 20 of 25.
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. Cataño, Néstor; Barraza, Fernando; García, Daniel; Ortega, Pablo; Rueda, Camilo: A case study in JML-assisted software development (2009)
  6. da Costa, Umberto Souza; Martins Moreira, Anamaria; Musicante, Martin A.; Souza Neto, Plácido A.: Specification and runtime verification of Java card programs (2009)
  7. Da Costa, Umberto Souza; Moreira, Anamaria Martins; Musicante, Martin A.; Neto, Plácido A.Souza: Specification and runtime verification of Java card programs (2009)
  8. Henzinger, Thomas A.; Hottelier, Thibaud; Kovács, Laura: Valigator: A verification tool with bound and invariant generation (2008)
  9. Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto: A program logic for resources (2007)
  10. Chalin, Patrice: Are the logical foundations of verifying compiler prototypes matching user expectations? (2007)
  11. Kieburtz, Richard B.: Programmed strategies for program verification. (2007)
  12. Robby; Rodríguez, Edwin; Dwyer, Matthew B.; Hatcliff, John: Checking JML specifications using an extensible software model checking framework (2006)
  13. 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)
  14. 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)
  15. Marché, Claude; Paulin-Mohring, Christine: Reasoning about Java programs with aliasing and frame conditions (2005)
  16. Pierik, Cees; De Boer, Frank S.: A proof outline logic for object-oriented programming (2005)
  17. Kreitz, Christoph: Building reliable, high-performance networks with the Nuprl proof development system (2004)
  18. Robby; Rodríguez, Edwin; Dwyer, Matthew B.; Hatcliff, John: Checking strong specifications using an extensible software model checking framework (2004)
  19. Jacobs, Bart; Poll, Erik: Coalgebras and monads in the semantics of Java (2003)
  20. Rauch, Nicole; Wolff, Burkhart: Formalizing java’s two’s-complement integral type in Isabelle/HOL. (2003)

1 2 next