This tutorial provides a comprehensive overview of neural network verification through the lens of the Branch-and-Bound (BaB) framework. We introduce our novel approach that combines a suspiciousness order over subproblems in BaB-based verification with advanced search techniques, such as Monte Carlo Tree Search and Simulated Annealing. By doing this, we reshape the order of visiting different sub-problems in BaB-based verification, such that we can efficiently find a counterexample to refute the specification if it exists, or reach the verification conclusion after traversing all the subproblems. Additionally, we showcase that our strategy is also applicable to incremental verification, a strategy to accelerate verification by reusing historical verification results, which is useful in the context of, e.g., network quantization and repair. Targeted at researchers and practitioners bridging software engineering and deep learning, the tutorial also includes a hands-on session demonstrating practical implementation with our open-source tool. Attendees will gain valuable insights into both the theoretical foundations and practical applications necessary for building robust neural network verifiers.