ESC/Java

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

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

1 2 3 ... 5 6 7 next

  1. Letan, Thomas; Régis-Gianas, Yann; Chifflier, Pierre; Hiet, Guillaume: Modular verification of programs with effects and effects handlers (2021)
  2. Burel, Guillaume; Bury, Guillaume; Cauderlier, Raphaël; Delahaye, David; Halmagrand, Pierre; Hermant, Olivier: First-order automated reasoning with theories: when deduction modulo theory meets practice (2020)
  3. Ahrendt, Wolfgang; Chimento, Jesús Mauricio; Pace, Gordon J.; Schneider, Gerardo: Verifying data- and control-oriented properties combining static and runtime verification: theory and tools (2017)
  4. Feldman, Yotam M. Y.; Padon, Oded; Immerman, Neil; Sagiv, Mooly; Shoham, Sharon: Bounded quantifier instantiation for checking inductive invariants (2017)
  5. Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey: Horn clause solvers for program verification (2015)
  6. Tschannen, J.; Furia, CA; Nordio, M.; Polikarpova, N.: AutoProof: Auto-active Functional Verification of Object-oriented Programs (2015) arXiv
  7. Oliveira, José N.: A relation-algebraic approach to the “Hoare logic” of functional dependencies (2014)
  8. Beckert, Bernhard; Klebanov, Vladimir: A dynamic logic for deductive verification of multi-threaded programs (2013)
  9. Ke, Wei; Liu, Zhiming; Wang, Shuling; Zhao, Liang: A graph-based generic type system for object-oriented programs (2013)
  10. Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.: Loop summarization using state and transition invariants (2013)
  11. 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)
  12. Li, Zhao-Peng; Zhang, Yu; Chen, Yi-Yun: A shape graph logic and a shape system (2013)
  13. Popeea, Corneliu; Chin, Wei-Ngan: Dual analysis for proving safety and finding bugs (2013)
  14. Stump, Aaron; Oe, Duckki; Reynolds, Andrew; Hadarean, Liana; Tinelli, Cesare: SMT proof checking using a logical framework (2013)
  15. Ahrendt, Wolfgang; Dylla, Maximilian: A system for compositional verification of asynchronous objects (2012)
  16. 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)
  17. Christakis, Maria; Müller, Peter; Wüstholz, Valentin: Collaborative verification and testing with explicit assumptions (2012)
  18. Miné, Antoine: Inferring sufficient conditions with backward polyhedral under-approximations (2012)
  19. Thamsborg, Jacob; Birkedal, Lars; Yang, Hongseok: Two for the price of one: lifting separation logic assertions (2012)
  20. Böhme, Sascha; Moskal, Michał: Heaps and data structures: a challenge for automated provers (2011)

1 2 3 ... 5 6 7 next