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 118 articles )

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

1 2 3 4 5 6 next

  1. Oliveira, José N.: A relation-algebraic approach to the “Hoare logic” of functional dependencies (2014)
  2. Beckert, Bernhard; Klebanov, Vladimir: A dynamic logic for deductive verification of multi-threaded programs (2013)
  3. Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.: Loop summarization using state and transition invariants (2013)
  4. Liao, Hongwei; Wang, Yin; Cho, Hyoun Kyu; Stanley, Jason; Kelly, Terence; Lafortune, Stéphane; Mahlke, Scott; Reveliotis, Spyros: Concurrency bugs in multithreaded software: modeling and analysis using Petri nets (2013)
  5. Li, Zhao-Peng; Zhang, Yu; Chen, Yi-Yun: A shape graph logic and a shape system (2013)
  6. Popeea, Corneliu; Chin, Wei-Ngan: Dual analysis for proving safety and finding bugs (2013)
  7. Stump, Aaron; Oe, Duckki; Reynolds, Andrew; Hadarean, Liana; Tinelli, Cesare: SMT proof checking using a logical framework (2013)
  8. Ahrendt, Wolfgang; Dylla, Maximilian: A system for compositional verification of asynchronous objects (2012)
  9. Chin, Wei-Ngan; David, Cristina; Nguyen, Huu Hai; Qin, Shengchao: Automated verification of shape, size and bag properties via user-defined predicates in separation logic (2012)
  10. Christakis, Maria; Müller, Peter; Wüstholz, Valentin: Collaborative verification and testing with explicit assumptions (2012)
  11. Miné, Antoine: Inferring sufficient conditions with backward polyhedral under-approximations (2012)
  12. Thamsborg, Jacob; Birkedal, Lars; Yang, Hongseok: Two for the price of one: lifting separation logic assertions (2012)
  13. Bonacina, Maria Paola; Lynch, Christopher A.; de Moura, Leonardo: On deciding satisfiability by theorem proving with speculative inferences (2011)
  14. Cousot, Patrick; Cousot, Radhia; Logozzo, Francesco: Precondition inference from intermittent assertions and application to contracts on collections (2011)
  15. Fähndrich, Manuel; Logozzo, Francesco: Static contract checking with abstract interpretation (2011)
  16. Huang, Shan Shan; Zook, David; Smaragdakis, Yannis: Statically safe program generation with SafeGen (2011)
  17. Logozzo, Francesco: Practical verification for the working programmer with codecontracts and abstract interpretation (invited talk) (2011) ioport
  18. Male, Chris; Pearce, David J.; Potanin, Alex; Dymnikov, Constantine: Formalisation and implementation of an algorithm for bytecode verification of $\@$NonNull types (2011)
  19. Roşu, Grigore; Ellison, Chucky; Schulte, Wolfram: Matching logic: an alternative to Hoare/Floyd logic (2011)
  20. Tschannen, Julian; Furia, Carlo A.; Nordio, Martin; Meyer, Bertrand: Usable verification of object-oriented programs by combining static and dynamic techniques (2011) ioport

1 2 3 4 5 6 next