Recent developments on SMT solvers have become crucial to make program analysis techniques effective in practice. Despite their success, scalability is still an issue when applying these methods to large fragments of code. In order to address this problem, we propose a template-based (also known as constraint-based) approach using Max-SMT solvers. In particular, we present an automated compositional program verification technique for safety properties based on conditional inductive invariants. Our bottom-up program verification framework synthesizes and propagates preconditions of small program parts as postconditions for preceding program parts. The method recovers from failures when some precondition is not proved. In this talk we will provide an overview of the Max-SMT solving techniques and their application to compositional program analysis. These techniques have successfully been implemented within the VeryMax tool which currently can check safety, reachability and termination properties of C++ code.