Houdini, an annotation assistant for ESC/Java

DOI10.1007/3-540-45251-6_29MaRDI QIDQ2763999zbMATH OpenFDO

Authors Cormac Flanagan, K. Rustan M. Leino

Publication date 22 January 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2021/20210500

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Computing methodologies and applications (68U99)

Recommendations

• JAVAVIS: Automatic program visualization with object and sequence diagrams using the Java debug interface (JDI)
• On the visualization of Java programs

Cited in

(32)

• Annotation inference for modular checkers
• Automated verification of functional correctness of race-free GPU programs
• A learning-based approach to synthesizing invariants for incomplete verification engines
• Learning inductive invariants by sampling from frequency distributions
• Unbounded procedure summaries from bounded environments
• Loop summarization using state and transition invariants
• Programming by predicates: a formal model for interactive synthesis
• Automatic inference of access permissions
• Guiding Craig interpolation with domain-specific abstractions
• ExplainHoudini: making Houdini inference transparent
• Houdini
• Predicate abstraction for program verification
• Inferring Loop Invariants Using Postconditions
• CHASE: A static checker for JML's assignable clause
• Verifying array manipulating programs with full-program induction
• From invariant checking to invariant inference using randomized search
• Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
• Mathematics of Program Construction
• Modular inference of subprogram contracts for safety checking
• SMT-based verification of program changes through summary repair
• Invariant inference with provable complexity from the monotone theory
• SAT-based invariant inference and its relation to concept learning
• RHLE: modular deductive verification of relational \(\forall \exists\) properties
• Data-Driven Invariant Learning for Probabilistic Programs
• Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
• Maximizing branch coverage with constrained Horn clauses
• \textsc{Sorcar}: property-driven algorithms for learning conjunctive invariants
• Global guidance for local generalization in model checking
• Verifying relative safety, accuracy, and termination for program approximations
• Data-driven invariant learning for probabilistic programs
• Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists
• An integrated approach to high integrity software verification

Describes a project that uses

Uses Software

• Mercator

This page was built for publication: Houdini, an annotation assistant for ESC/Java

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2763999)