Infer
From MaRDI portal
Cited in
(37)- Juliet Test Suite
- Predator
- A decision procedure for separation logic in SMT
- SLAyer
- HIP
- Smallfoot
- VeriSmall
- Automatically proving termination and memory safety for programs with pointer arithmetic
- ModuRes
- Fugue
- Ctrl
- Clara
- IKOS
- THOR
- A complete decision procedure for linearly compositional separation logic with data constraints
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- Temporary read-only permissions for separation logic
- Unified reasoning about robustness properties of symbolic-heap separation logic
- Sparrow
- Cyclist
- coreStar
- Featherweight VeriFast
- Caper
- Fran
- Charge!
- GRASShopper
- Slide
- Separation logics and modalities: a survey
- Incremental and modular context-sensitive analysis
- Decidability for entailments of symbolic heaps with arrays
- On temporal and separation logics
- Tractability of separation logic with inductive definitions: beyond lists
- IncA
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- Program Verification with Separation Logic
- SeLoger
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
This page was built for software: Infer
