LOOP
| swMATH ID: | 10292 |
| Software Authors: | van den Berg, Joachim; Jacobs, Bart |
| Description: | 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. |
| Homepage: | http://link.springer.com/chapter/10.1007/3-540-45319-9_21 |
| Related Software: | JML; PVS; KRAKATOA; ESC/Java; Eiffel; Coq; KeY; Spec#; Jass; SPIN; SIMPLIFY; Isabelle/HOL; SPARK; Haskell; LARCH; JCML; Z; Daikon; Why3; Caduceus |
| Cited in: | 24 Documents |
Standard Articles
| 1 Publication describing the Software, including 1 Publication in zbMATH | Year |
|---|---|
|
The LOOP compiler for Java and JML. Zbl 0978.68708 van den Berg, Joachim; Jacobs, Bart |
2001
|
all
top 5
Cited by 43 Authors
Cited in 5 Serials
| 4 | The Journal of Logic and Algebraic Programming |
| 3 | Theoretical Computer Science |
| 2 | Formal Aspects of Computing |
| 1 | Science of Computer Programming |
| 1 | Journal of Functional Programming |
Cited in 2 Fields
| 24 | Computer science (68-XX) |
| 2 | Mathematical logic and foundations (03-XX) |
