The reliable functioning of safety-critical IT systems depends heavily on the correct execution of program code. Deductive program verification can be performed to provide a high level of correctness guarantees for computer programs. There is a plethora of different programming languages in use, and new languages oriented for high reliability scenarios are still being invented. It can be difficult to devise for each such language a full-fledged logical system supporting the verification of programs, and to prove the soundness and completeness of the logical system with respect to the formal semantics of the language. Language-independent verification techniques offer sound verification procedures parameterized over the formal semantics of programming languages. The specialization of the verification procedure with the formal semantics of a concrete programming language directly gives rise to a verification procedure for the language. In this article, we propose a language-independent verification technique based on big-step operational semantics. The technique features a unified procedure for the sound reasoning about program structures that potentially causes unbounded behavior, such as iteration and recursion. In particular, we employ a functional formalization of big-step semantics to support the explicit representation of the computation performed by the sub-structures of a program. This representation enables the exploitation of the auxiliary information provided for these sub-structures in the unified reasoning process. We prove the soundness and relative completeness of the proposed technique, evaluate the technique using verification examples in imperative and functional programming languages, and mechanize all the formal results and verification examples in the Coq proof assistant. The development provides a basis for the implementation of a language-independent program verifier in a proof assistant based on big-step operational semantics.