Symbolic heap abstraction with demand-driven axiomatization of memory invariants