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

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

1 2 next

  1. de Boer, Frank S.; de Gouw, Stijn: Combining monitoring with run-time assertion checking (2014) ioport
  2. 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)
  3. Liu, Zhiming; Morisset, Charles; Wang, Shuling: A graph-based implementation for mechanized refinement calculus of OO programs (2011)
  4. Mossakowski, Till; Schröder, Lutz; Goncharov, Sergey: A generic complete dynamic logic for reasoning about purity and effects (2010)
  5. Bertot, Yves: Theorem-proving support in programming language semantics (2009)
  6. Cataño, Néstor; Barraza, Fernando; García, Daniel; Ortega, Pablo; Rueda, Camilo: A case study in JML-assisted software development (2009) ioport
  7. da Costa, Umberto Souza; Martins Moreira, Anamaria; Musicante, Martin A.; Souza Neto, Plácido A.: 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. Mossakowski, Till; Schröder, Lutz; Roggenbach, Markus; Reichel, Horst: Algebraic-coalgebraic specification in CoCASL (2006)
  13. Robby; Rodríguez, Edwin; Dwyer, Matthew B.; Hatcliff, John: Checking JML specifications using an extensible software model checking framework (2006) ioport
  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) ioport
  15. 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) ioport
  16. Marché, Claude; Paulin-Mohring, Christine: Reasoning about Java programs with aliasing and frame conditions (2005)
  17. Pierik, Cees; De Boer, Frank S.: A proof outline logic for object-oriented programming (2005)
  18. Farzan, Azadeh; Meseguer, José; Roşu, Grigore: Formal JVM code analysis in JavaFAN (2004)
  19. Jacobs, Bart: Weakest pre-condition reasoning for Java programs with JML annotations (2004)
  20. Jacobs, Bart; Oostdijk, Martijn; Warnier, Martijn: Source code verification of a secure payment applet (2004)

1 2 next