swMATH9786MaRDI QIDQ21765FDOQ21765
Author name not available (Why is that?)
Official website: http://loris-7.ddns.comp.nus.edu.sg/~project/hip/index.html
Cited In (64)
- A learning-based approach to synthesizing invariants for incomplete verification engines
- StarFinder
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
- Nested antichains for WS1S
- Disproving inductive entailments in separation logic via base pair approximation
- Enhancing symbolic execution of heap-based programs with separation logic for test input generation
- Automata-based verification of programs with tree updates
- Completeness for recursive procedures in separation logic
- Automated Verification of Shape and Size Properties Via Separation Logic
- Symbolic execution proofs for higher order store programs
- Lightweight Separation
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Verification of heap manipulating programs with ordered data by extended forest automata
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- Completeness and expressiveness of pointer program verification by separation logic
- SeLoger
- Verifying pointer safety for programs with unknown calls
- FMona
- COMBINE
- TASC
- MONA
- TestEra
- Crowfoot
- VeriFast
- SLAyer
- Smallfoot
- Toolchain
- FixBag
- VeriSmall
- jStar
- GanttProject
- Juggrnaut
- TweetNaCl
- THOR
- coreStar
- Cyclist
- Antichains
- Caper
- Infer
- Tractability of separation logic with inductive definitions: beyond lists
- Charge!
- GRASShopper
- Bears
- Slide
- Omega++
- Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure
- Automated cyclic entailment proofs in separation logic
- JaCoCo
- QSYM
- A relational shape abstract domain
- JBSE
- Automated mutual induction proof in separation logic
- A complete decision procedure for linearly compositional separation logic with data constraints
- Forest automata for verification of heap manipulation
- Featherweight VeriFast
- Beyond Shapes: Lists with Ordered Data
- Crowfoot: A Verifier for Higher-Order Store Programs
- VST-Floyd: a separation logic tool to verify correctness of C programs
- Invariants synthesis over a combined domain for automated program verification
- Reasoning about block-based cloud storage systems via separation logic
- Certified reasoning with infinity
- Lazy automata techniques for WS1S
- Unified reasoning about robustness properties of symbolic-heap separation logic
This page was built for software: HIP
