I am looking for books that focus on proving algorithms correct in a rigorous manner without any hand-waving. Also, the book should not introduce notation intuitively without a proper explanation.
The book's main focus should be correctness not complexity.
As a general guideline I think that CLRS is too informal and doesn't fit my requirements.
If you want to eliminate any hand-waving, then use a mechanized theorem prover. A significant book series in this area that's also available online is Benjamin Pierce's Software Foundations series. This series teaches you how to use the proof assistant Coq, the system used for (among many other things) formally verifying the CompCert C compiler, for computer science problems including algorithm verification. From there Coq libraries like YNot and the research/publications around them would be a place to look.
There are also mechanized theorem provers or related tools that take different approaches. Things like Frama-C, Why3, Alloy, Spin, Ada SPARK, the $\mathbb{K}$ Framework, NuPRL, Isabelle/HOL, Twelf, TLAPS, Welder/Inox and many others. These approach different aspects of the problem with different approaches and different levels of ambition and usability. For example, to prove something about a program, you need to have a semantics for the programming language. Simplifying the creation of programming language semantics is the goal of the $\mathbb{K}$ framework meanwhile Ada SPARK is a large fragment of Ada with a formal semantics. Specifying the semantics of C and assembly in Coq was a huge part of the CompCert project. Given a semantics, you then need some way of giving a specification of your program and generally connecting the source code. Frama-C does this for C (and there are variations in that suite for other languages). Of course, stating what you expect is different from proving that it holds. Proof assistants like Coq, Twelf, Isabelle/HOL, and TLAPS allow very complicated theorems to be proven but require a fairly high level of expertise to use in real world cases. These also take different approaches using either constructive type theory, classical higher-order logic, or set theory. In many cases, what needs to be proven is relatively simple and can be fully automated. Tools like Welder/Inox coordinate automatic theorem provers to deal with these. Sometimes its just too expensive/difficult to get (and crucially maintain) a full proof of correctness. Model checkers like Spin and Alloy can be used to exhaustively check the state space of the program (or an abstraction thereof) at least to some depth. These can often find defects, and in some cases may be able to fully check the state space. These are much easier to use but they don't give the same guarantees and can take huge amounts of computation. In practice, they are often used to verify protocols rather than the actual code to minimize the state space. A different approach to trying to prove code correct is to extract the program from a proof. NuPRL is one of the oldest, still living systems that focuses on this approach, but this can be done with Isabelle/HOL and Coq as well. Some systems like Why3, Welder, and Isabelle are more frameworks meant to help join tools together. There are many other alternatives to the tools that I've listed in each of their niches.
Here are some titles that come to mind, in almost-random order, each with a different slant. The one that perhaps meets your requirements most closely is Dijkstra's book. The others focus more on verification of programs than on the programs themselves; or, as in Lynch's book, they focus on a class of algorithms.
Dijkstra, A Discipline of Programming
Apt, de Boer, Olderog, Verification of Sequential and Concurrent Programs
Nielson, Nielson, Hankin, Principles of Program Analysis
Herlihy, Shavit, The Art of Multiprocessor Programming
Gries, The Science of Programming
Monin, Understanding Formal Methods
I'm suspect I forgot some important book, but this may give you a starting point.
This is probably better as a comment, but certainly too long.
I honestly think what you are looking for doesn't exist. Computer science, especially at the undergraduate level, has really become a vocational discipline. Most (undergraduate) students go into it for the purpose of getting software engineering jobs. The theoretical hurdles are usually regarded with some disdain (proofs tend to make folks cringe).
As a result, (undergraduate) CS texts have become more relaxed on the rigor. The Ullman-Hopcroft Automata Theory texts illustrate this point well. The first edition was far more rigorous and comprehensive than the third edition, which includes applications such as parsing HTML. A common criticism is that "all the good stuff" was taken out in writing the third edition.
Algorithms and complexity also go hand-in-hand. For decidable problems, the brute force and ignorance approach is usually enough to obtain a solution. For mathematicians, this may be enough for proofs (e.g., constructive proofs in graph theory). Computer scientists demand more in terms of algorithm efficiency. From a practical perspective, we want a computer program to be able to spit out a solution. From a theoretical perspective, demonstrating an algorithm correctly solves the problem within certain resource bounds enables us to classify computational problems into complexity classes.
Regarding references, I might suggest the following:
-Kleinberg and Tardos (https://www.amazon.com/Algorithm-Design-Jon-Kleinberg/dp/0321295358/). Both authors are top notch theorists. (Tardos was actually a Babai student as an undergrad, and Babai is certainly a stickler for the details.) The comments on Amazon suggest a great deal of mathematical rigor and emphasis on good algorithm design techniques. The table of contents looks solid to me.
-Sedgewick (https://www.amazon.com/Algorithms-4th-Robert-Sedgewick/dp/032157351X). A friend of mine went through Sedgewick's Coursera course and had excellent things to say. Based on his recommendation, Sedgewick may be worth considering. I'm not sure if it has the desired level of rigor.
More advanced texts on randomized algorithms or approximation algorithms may also have the desired level of rigor. Again, these are more advanced techniques, so perhaps not desirable as a starting point.
I hope this helps!
I think you are probably looking for: Algorithms A Top-Down Approach. Citted from the Preface of this book:
This book is motivated in part by the author’s belief that people do not fully understand an algorithm until they are able to prove its correctness. For this reason, all of Chapter 2 and much of Chapter 4 are devoted to techniques for proving correctness.
