Houdini
From MaRDI portal
Cited in
(51)- Code2Inv
- iDFlakies
- RHLE Benchmarks
- Programming by predicates: a formal model for interactive synthesis
- From invariant checking to invariant inference using randomized search
- Loop summarization using state and transition invariants
- Predicate abstraction for program verification
- Verifying array manipulating programs with full-program induction
- Automatic inference of access permissions
- A learning-based approach to synthesizing invariants for incomplete verification engines
- Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
- Inferring Loop Invariants Using Postconditions
- Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists
- ExplainHoudini: making Houdini inference transparent
- Learning inductive invariants by sampling from frequency distributions
- Verifying relative safety, accuracy, and termination for program approximations
- SPARK
- Daikon
- Modular inference of subprogram contracts for safety checking
- An integrated approach to high integrity software verification
- UFO
- ACL2s
- SPEED
- eVolCheck
- InvGen
- libalf
- TVLA
- Traffic 4
- Mercator
- SymDiff
- CSSV
- c2i
- ExplainHoudini
- VS3
- CodeHint
- SyPet
- ACCEPT
- Chisel
- EnerJ
- FlexJava
- FlashExtract
- Green
- BlinkFill
- Jass
- ANNA
- Rely
- Automated verification of functional correctness of race-free GPU programs
- Specification and verification challenges for sequential object-oriented programs
- CLN2INV
- Guiding Craig interpolation with domain-specific abstractions
- Class invariants as abstract interpretation of trace semantics
This page was built for software: Houdini
