The Extended Static Checker for Java version 2 (ESC/Java2) is a programming tool that attempts to find common run-time errors in JML-annotated Java programs by static analysis of the program code and its formal annotations. Users can control the amount and kinds of checking that ESC/Java2 performs by annotating their programs with specially formatted comments called pragmas

References in zbMATH (referenced in 137 articles )

Showing results 21 to 40 of 137.
Sorted by year (citations)
  1. Böhme, Sascha; Moskal, Michał: Heaps and data structures: a challenge for automated provers (2011)
  2. Bonacina, Maria Paola; Lynch, Christopher A.; de Moura, Leonardo: On deciding satisfiability by theorem proving with speculative inferences (2011)
  3. Cousot, Patrick; Cousot, Radhia; Logozzo, Francesco: Precondition inference from intermittent assertions and application to contracts on collections (2011)
  4. Fähndrich, Manuel; Logozzo, Francesco: Static contract checking with abstract interpretation (2011)
  5. Huang, Shan Shan; Zook, David; Smaragdakis, Yannis: Statically safe program generation with SafeGen (2011)
  6. Lahiri, Shuvendu K.; Vanegue, Julien: ExplainHoudini: making Houdini inference transparent (2011)
  7. Liu, Yijing; Qiu, Zongyan; Long, Quan: WP semantics and behavioral subtyping (2011)
  8. Logozzo, Francesco: Practical verification for the working programmer with codecontracts and abstract interpretation (invited talk) (2011) ioport
  9. Male, Chris; Pearce, David J.; Potanin, Alex; Dymnikov, Constantine: Formalisation and implementation of an algorithm for bytecode verification of (@)NonNull types (2011)
  10. Roşu, Grigore; Ellison, Chucky; Schulte, Wolfram: Matching logic: an alternative to Hoare/Floyd logic (2011)
  11. Tschannen, Julian; Furia, Carlo A.; Nordio, Martin; Meyer, Bertrand: Usable verification of object-oriented programs by combining static and dynamic techniques (2011) ioport
  12. Beckert, Bernhard; Moskal, Michal: Deductive verification of system software in the verisoft XT project (2010) ioport
  13. Böhme, Sascha; Moskal, Michał; Schulte, Wolfram; Wolff, Burkhart: HOL-Boogie -- an interactive prover-backend for the verifying C compiler (2010)
  14. Buss, Marcio; Brand, Daniel; Sreedhar, Vugranam; Edwards, Stephen A.: A novel analysis space for pointer analysis and its application for bug finding (2010)
  15. de Moura, Leonardo; Bjørner, Nikolaj: Bugs, moles and skeletons: symbolic reasoning for software development (2010)
  16. du Bousquet, Lydie; Ledru, Yves; Maury, Olivier; Oriat, Catherine; Lanet, Jean-Louis: Reusing a JML specification dedicated to verification for testing, and vice-versa: Case studies (2010) ioport
  17. Furia, Carlo Alberto; Meyer, Bertrand: Inferring loop invariants using postconditions (2010)
  18. Hoenicke, Jochen; Leino, K. Rustan M.; Podelski, Andreas; Schäf, Martin; Wies, Thomas: Doomed program points (2010)
  19. James, Perry R.; Chalin, Patrice: Faster and more complete extended static checking for the Java modeling language (2010)
  20. Kreiker, Jörg; Seidl, Helmut; Vojdani, Vesal: Shape analysis of low-level C with overlapping structures (2010)