Well... yes actually, if every path “through” the program is tested. But that means, every possible path through the entire space of all possible states the program can have, including all variables. Even for a very simple statically compiled program – say, an old Fortran number cruncher – that's not feasible, though it can at least be imaginable: if you have just two integer variables, you're basically dealing with all possible ways to connect points on a two-dimensional grid; it actually looks a lot like Travelling Salesman. For n such variables, you're dealing with an n-dimensional space, so for any real program, the task is completely untractable.
Worse: for serious stuff, you have not just a fixed number of primitive variables, but create variables on the fly in function calls, or have variable-size variables... or anything like that, as possible in a Turing-complete language. That makes the state space infinite-dimensional, shattering all hopes of full coverage, even given absurdly powerful testing equipment.
That said... actually things aren't quite so bleak. It is possible to proove entire programs to be correct, but you'll have to give up a few ideas.
First: it's highly advisable to switch to a declarative languange. Imperative languages, for some reason, have always been by far the most popular, but the way they mix together algorithms with real-world interactions makes it extremely difficult to even say what you mean by “correct”.
Much easier in purely functional programming languages: these have a clear distinction between the real interesting properties of mathematical functions, and the fuzzy real-world interactions you can't really say anything about. For the functions, it is very easy to specify “correct behavior”: if for all possible inputs (from the argument types) the corresponding desired result comes out, then the function behaves correctly.
Now, you say that's still intractable... after all, the space of all possible arguments is in general also infinite-dimensional. True – though for a single function, even naïve coverage testing leads you way further than you could ever hope for in an imperative program! However, there is an incredible powerful tool that changes the game: universal quantification / parametric polymorphism. Basically, this allows you to write functions on very general kinds of data, with the guarantee that if it works for a simple example of the data, it will work for any possible input at all.
At least theoretically. It's not easy to find the right types that are really so general that you can completely proove this – usually, you need a dependently-typed language, and these tend to be rather difficult to use. But writing in a functional style with parametric polymorphism alone already boosts your “security level” enourmously – you won't necessarily find all bugs, but you'll have to hide them quite well so the compiler doesn't spot them!