Houdini

Houdini, an annotation assistant for ESC/Java. A static program checker that performs modular checking can check one program module for errors without needing to analyze the entire program. Modular checking requires that each module be accompanied by annotations that specify the module. To help reduce the cost of writing specifications, this paper presents Houdini, an annotation assistant for the modular checker ESC/Java. To infer suitable ESC/Java annotations for a given program, Houdini generates a large number of candidate annotations and uses ESC/Java to verify or refute each of these annotations. The paper describes the design, implementation, and preliminary evaluation of Houdini.


References in zbMATH (referenced in 21 articles , 1 standard article )

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

1 2 next

  1. Neider, Daniel; Madhusudan, P.; Saha, Shambwaditya; Garg, Pranav; Park, Daejun: A learning-based approach to synthesizing invariants for incomplete verification engines (2020)
  2. Peleg, Hila; Itzhaky, Shachar; Shoham, Sharon; Yahav, Eran: Programming by predicates: a formal model for interactive synthesis (2020)
  3. He, Shaobo; Lahiri, Shuvendu K.; Rakamarić, Zvonimir: Verifying relative safety, accuracy, and termination for program approximations (2018)
  4. Jhala, Ranjit; Podelski, Andreas; Rybalchenko, Andrey: Predicate abstraction for program verification (2018)
  5. Kojima, Kensuke; Imanishi, Akifumi; Igarashi, Atsushi: Automated verification of functional correctness of race-free GPU programs (2018)
  6. Leroux, Jérôme; Rümmer, Philipp; Subotić, Pavle: Guiding Craig interpolation with domain-specific abstractions (2016)
  7. Sharma, Rahul; Aiken, Alex: From invariant checking to invariant inference using randomized search (2016)
  8. Garg, Pranav; Löding, Christof; Madhusudan, P.; Neider, Daniel: Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists (2015)
  9. Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.: Loop summarization using state and transition invariants (2013)
  10. Ferrara, Pietro; Müller, Peter: Automatic inference of access permissions (2012)
  11. Lahiri, Shuvendu K.; Vanegue, Julien: ExplainHoudini: making Houdini inference transparent (2011)
  12. Furia, Carlo Alberto; Meyer, Bertrand: Inferring loop invariants using postconditions (2010)
  13. Moy, Yannick; Marché, Claude: Modular inference of subprogram contracts for safety checking (2010)
  14. Lahiri, Shuvendu K.; Qadeer, Shaz: Complexity and algorithms for monomial and clausal predicate abstraction (2009)
  15. Logozzo, Francesco: Class invariants as abstract interpretation of trace semantics (2009)
  16. Leavens, Gary T.; Leino, K. Rustan M.; Müller, Peter: Specification and verification challenges for sequential object-oriented programs (2007)
  17. Ireland, Andrew; Ellis, Bill J.; Cook, Andrew; Chapman, Roderick; Barnes, Janet: An integrated approach to high integrity software verification (2006)
  18. Burdy, Lilian; Cheon, Yoonsik; Cok, David R.; Ernst, Michael D.; Kiniry, Joseph R.; Leavens, Gary T.; Leino, K. Rustan M.; Poll, Erik: An overview of JML tools and applications (2005) ioport
  19. Burdy, Lilian; Cheon, Yoonsik; Cok, David R.; Ernst, Michael D.; Kiniry, Joseph R.; Leavens, Gary T.; Leino, K. Rustan M.; Poll, Erik: An overview of JML tools and applications (2005) ioport
  20. Li, Harry C.; Krishnamurthi, Shriram; Fisler, Kathi: Modular verification of open features using three-valued model checking (2005) ioport

1 2 next