Software systems are increasingly involved in our daily life tasks, making their failures potentially damaging both in economic and human terms. As a result, proving the correctness of software is widely thought to be one of the most central challenges for computer science. Model checking is an award-winning (Turing award, 2007) technique for formally and automatically verifying systems, often capable to guarantee the correctness of non-trivial and practical programs. However, model checking is undecidable in the general case. Even when properly restricted to the decidable fragment, the algorithms face strong scalability issues preventing them to converge to the solution. The goal of this thesis is to address such scalability issues in two orthogonal ways. First, the design of parallel solving techniques that exploit the massive amount of computational power offered by distributed computing environments. Second, the design of a modelling technique for effective verification of the new emergent technology of smart contracts running on blockchain systems. The parallel solving research efforts consider both bounded and induction-based unbounded model checking, respectively achieved by instantiating multi-agent solving for the T-DPLL and IC3 algorithms. Multi-agent techniques leverage on the diversification and cooperation among sequential solvers executed in parallel. Diversification is achieved with different parallel search heuristics, and cooperation is performed with the exchange of information both during solving time and via upfront agreements. The effectivenesses of various multi-agent settings are empirically evaluated using the purpose-built multi-agent framework SMTS. Verification approaches for emerging technologies tend to either reuse tools for existing languages that often result in inefficient and even unsound models, or to apply generic techniques which typically require human intervention to succeed. This thesis provides a new direct modelling approach using constrained Horn clauses for the emerging technology of smart contracts. Such approach allows automatic solving exploiting the proposed efforts in improving inductive solvers scalability, and guarantees soundness for the safety proofs. Additionally, the smart-contracts-specific task of measuring the amount of computation needed to execute a transaction, i.e. gas consumption, is considered in this thesis proposing an algorithmic solution. The effectiveness of the modelling technique is empirically evaluated over smart contracts deployed in the Ethereum blockchain using an implementation inside the official compiler for the smart contracts language Solidity that relies on the IC3 algorithm.