jStar: Towards practical verification for Java. In this paper we introduce a novel methodology for verifying a large set of Java programs which builds on recent theoretical developments in program verification: it combines the idea of abstract predicate families and the idea of symbolic execution and abstraction using separation logic. The proposed technology has been implemented in a new automatic verification system, called jStar, which combines theorem proving and abstract interpretation techniques. We demonstrate the effectiveness of our methodology by using jStar to verify example programs implementing four popular design patterns (subject/observer, visitor, factory, and pooling). Although these patterns are extensively used by object-oriented developers in real-world applications, so far they have been highly challenging for existing object-oriented verification techniques.

References in zbMATH (referenced in 27 articles )

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

1 2 next

  1. Hóu, Zhé; Goré, Rajeev; Tiu, Alwen: Automated theorem proving for assertions in separation logic with all connectives (2015)
  2. Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
  3. Reus, Bernhard; Charlton, Nathaniel; Horsfall, Ben: Symbolic execution proofs for higher order store programs (2015)
  4. Amighi, Afshin; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva-Stojanovski, Marina: Verification of concurrent systems with VerCors (2014)
  5. Brotherston, James; Kanovich, Max: Undecidability of propositional separation logic and its neighbours (2014)
  6. de Boer, Frank S.; de Gouw, Stijn: Combining monitoring with run-time assertion checking (2014)
  7. Lee, Wonyeol; Park, Sungwoo: A proof system for separation logic with magic wand (2014)
  8. Nordio, Martin; Calcagno, Cristiano; Meyer, Bertrand: Certificates and separation logic (2014)
  9. Banerjee, Anindya; Naumann, David A.: Local reasoning for global invariants. II: Dynamic boundaries (2013)
  10. Charlton, Nathaniel; Reus, Bernhard: Specification patterns for reasoning about recursion through the store (2013)
  11. Li, Zhao-Peng; Zhang, Yu; Chen, Yi-Yun: A shape graph logic and a shape system (2013)
  12. Brotherston, James: Bunched logics displayed (2012)
  13. Stewart, Gordon; Beringer, Lennart; Appel, Andrew W.: Verified heap theorem prover by paramodulation (2012)
  14. Thamsborg, Jacob; Birkedal, Lars; Yang, Hongseok: Two for the price of one: lifting separation logic assertions (2012)
  15. Brotherston, James; Distefano, Dino; Petersen, Rasmus Lerchedahl: Automated cyclic entailment proofs in separation logic (2011)
  16. Calcagno, Cristiano; Distefano, Dino; O’Hearn, Peter W.; Yang, Hongseok: Compositional shape analysis by means of bi-abduction (2011)
  17. Charlton, Nathaniel; Reus, Bernhard: Specification patterns and proofs for recursion through the store (2011)
  18. Cook, Byron; Haase, Christoph; Ouaknine, Joël; Parkinson, Matthew; Worrell, James: Tractable reasoning in a fragment of separation logic (2011)
  19. Fähndrich, Manuel; Logozzo, Francesco: Static contract checking with abstract interpretation (2011)
  20. Roşu, Grigore; Ellison, Chucky; Schulte, Wolfram: Matching logic: an alternative to Hoare/Floyd logic (2011)

1 2 next