Program　invariants　such　as　loop　invariants　and　method　specifications　(　a.k.a.　procedural　summaries)　are　key　components　in　program　verification.　Such　invariants　are　usually　manually　specified　by　users　before　passed　as　inputs　to　a　program　verifier.　The　process　of　manually　annotating　programs　with　such　invariants　is　tedious　and　error-prone　and　can　significantly　hinder　the　level　of　automation　in　program　verification.　Although　invariant　synthesis　techniques　have　made　noticeable　progress　in　reducing　the　burden　of　user　annotations;　when　it　comes　to　automated　verification　of　memory　safety　and　functional　correctness　for　heap-manipulating　programs,　it　remains　a　rather　challenging　task　to　discover　program　specifications　and　invariants　automatically,　due　to　the　complexity　of　aliasing　and　mutability　of　data　structures.　In　this　paper,　we　present　invariant　synthesis　algorithms　for　the　following　scenarios:　i)　to　synthesise　a　missing　loop　invariant,　ii)　to　refine　given　pre/post　shape　templates　to　complete　pre/post-conditions,　iii)　to　infer　a　missing　precondition,　iv)　to　calculate　a　missing　postcondition,　given　a　precondition.　The　proposed　analyses　are　based　on　abstract　interpretation　and　are　built　over　an　abstract　domain　combining　separation,　numerical　and　multi-set　(bag)　information.　Our　inference　mechanisms　are　equipped　with　newly　designed　abstraction,　join,　widening　and　abduction　operations.　Initial　prototypical　experiments　have　shown　that　they　are　viable　and　powerful　enough　to　discover　interesting　useful　invariants　for　non-trivial　programs.　©　2013　Springer-Verlag.