OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse

David R. Cok

doi:10.4204/eptcs.149.8

journal article Apr 26, 2014

OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse

David R. Cok

Electronic Proceedings in Theoretical Computer Science Vol. 149 pp. 79-92 · Open Publishing Association

View at Publisher Save 10.4204/eptcs.149.8

Topics

No keywords indexed for this article. Browse by subject →

References

34

[1]

Barnett "Weakest-precondition of unstructured programs" (2005) 10.1145/1108792.1108813

[2]

Barnett "The Spec# Programming System: An Overview" (2005) 10.1007/978-3-540-30569-9_3

[3]

(2007) 10.1007/978-3-540-69061-0

[4]

Blanc "An Overview of the Leon Verification System: Verification by Translation to Recursive Functions" (2013) 10.1145/2489837.2489838

[5]

Burdy "Preliminary Design of BML: A Behavioral Interface Specification Language for Java Bytecode" (2007) 10.1007/978-3-540-71289-3_18

[6]

Chalin "JML support for primitive arbitrary precision numeric types: Definition and semantics" Journal of Object Technology (2004) 10.5381/jot.2004.3.6.a3

[7]

Chalin "Reassessing JML's logical foundation" Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs (FTfJP05), Glasgow, Scotland (2005)

[8]

Chalin "Non-null references by default in Java: Alleviating the nullity annotation burden" (2007) 10.1007/978-3-540-73589-2_12

[9]

Chalin "Reducing the use of nullable types through non-null by default and monotonic non-null." IET Software (2008) 10.1049/iet-sen:20080010

[10]

Chrzaszcz "BML and Related Tools" (2009) 10.1007/978-3-642-04167-9_14

[11]

Cok "Improved usability and performance of SMT solvers for debugging specifications" International Journal on Software Tools for Technology Transfer (STTT) (2010) 10.1007/s10009-010-0138-x

[12]

Cok "Reasoning with specifications containing method calls in JML and first-order provers" (2004)

[13]

Cok "Adapting JML to generic types and Java 1.6" SAVCBS'08 (2008)

[14]

Cok "jSMTLIB: Tutorial, Validation and Adapter Tools for SMT-LIBv2" (2011) 10.1007/978-3-642-20398-5_36

[15]

Cok "SPEEDY: An Eclipse-based IDE for invariant inference" Electronic Proceedings in Theoretical Computer Science (EPTCS) (2014) 10.4204/eptcs.149.5

[16]

Cok "ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2, including a case study involving the use of the tool to verify portions of an Internet voting tally system" (2005) 10.1007/b105030

[17]

Darvas "Reasoning About Method Calls in Interface Specifications" Journal of Object Technology (2006) 10.5381/jot.2006.5.5.a3

[18]

De Moura "Z3: An Efficient SMT Solver" (2008)

[19]

Dietl "Generic Universe Types" (2007) 10.1007/978-3-540-73589-2_3

[20]

Ernst "The Daikon system for dynamic detection of likely invariants" Science of Computer Programming (2007) 10.1016/j.scico.2007.01.015

[21]

Filliâtre "Why3 — Where Programs Meet Provers" (2013) 10.1007/978-3-642-37036-6_8

[22]

Flanagan "Extended Static Checking for Java" (2002) 10.1145/512529.512558

[23]

Flanagan "Avoiding exponential explosion: generating compact verification conditions" SIGPLAN Not. (2001) 10.1145/373243.360220

[24]

Le Goues "The Boogie Verification Debugger (Tool Paper)" (2011) 10.1007/978-3-642-24690-6_28

[25]

Leavens "JML: A Notation for Detailed Design" (1999) 10.1007/978-1-4615-5229-1_12

[26]

Leino "Data Groups: Specifying the Modification of Extended State" (1998) 10.1145/286942.286953

[27]

Leino "Efficient weakest preconditions" Inf. Process. Lett. (2005) 10.1016/j.ipl.2004.10.015

[28]

Leino "Dafny: An Automatic Program Verifier for Functional Correctness" (2010) 10.1007/978-3-642-17511-4_20

[29]

Leino "A verification methodology for model fields" (2006) 10.1007/11693024_9

[30]

Leino "The Dafny Integrated Development Environment" Electronic Proceedings in Theoretical Computer Science (EPTCS) (2014) 10.4204/eptcs.149.2

[31]

Meyer (1988)

[32]

Papi "Practical pluggable types for Java" (2008) 10.1145/1390630.1390656

[33]

Shaner "Modular verification of higher-order methods with mandatory calls specified by model programs" (2007) 10.1145/1297027.1297053

[34]

Zimmerman "JMLUnit: The Next Generation" (2011) 10.1007/978-3-642-18070-5_13

Metrics

49

Citations

34

References

Details

Published: Apr 26, 2014
Vol/Issue: 149
Pages: 79-92

Authors

D

David R. Cok

GrammaTech, Inc.

Cite This Article

David R. Cok (2014). OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse. Electronic Proceedings in Theoretical Computer Science, 149, 79-92. https://doi.org/10.4204/eptcs.149.8

OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse

You May Also Like