In this talk, we present our recent and ongoing work on constraint-based approach to relational and temporal verification of infinite-state programs. We advocate a class of predicate Constraint Satisfaction Problems called pfwCSP that extends the well-studied class of Constrained Horn Clauses (CHCs) with non-Horn clauses, functionality, and well-foundedness constraints on predicate variables. We then present reductions from relational verification problems to pfwCSP that can handle hyperproperties beyond k-safety such as generalized non-interference and co-termination. Furthermore, we introduce a new class $\mu$CLP of constraint logic programs with arbitrarily nested inductive and co-inductive predicates that is capable of modularly encoding temporal verification problems such as termination/non-termination, LTL, CTL, and even the full modal $\mu$-calculus model checking. For automated verification, we present a reduction from $\mu$CLP to pfwCSP and a CEGIS-based constraint solver for pfwCSP.