Global society increasingly relies on devices controlled by software, from TV sets to vehicle braking systems. It is considered a "fact-of-life" that software contains errors, which can come at great cost, such as the Mars Polar Lander crash or the 1992 failure of the London Ambulance Dispatch Service. In a 2008 study, the US NIST agency estimates faulty software costs the US economy $59.5bn annually. Classically software is tested by running it under as many difficult situations as possible. However, it is not feasible to run a program under all environments. Hence, testing relies on the perspicacity of the testing engineer who must carefully choose environments that may expose flaws. Modern computers increase performance by allowing many computer programs to run concurrently. Anticipating the interactions of even as a little as two programs is an extremely difficult task, and errors are often difficult to replicate and diagnose. Furthermore, the efficiency of hardware is often increased by permitting behaviours a software developer would not expect. An alternative approach to ensuring correctness is model-checking. Model-checking attempts to use fully automatic techniques to prove that a program behaves as expected under all conditions. This area has flourished recently, including a 2007 Turing Award for Clarke, Emerson and Sifakis, who transformed the technique from a theoretical pursuit into an industrially applicable product. Model-checking is embraced by companies like Microsoft (to improve its Windows OS) and Altran-Praxis (for safety-critical software). However, model-checkers must rely on simplified models of computer programs to guarantee results, leading to many correct programs being labelled erroneous. This is a design choice, following the argument that it it better to raise a false alarm, than let an error pass by. However, a large number of false alarms damage reliability and usability --- a software developer will not study reported errors carefully if the majority are, in fact, not errors at all. This is a real problem in the large scale deployment of such tools. The goal of this fellowship is to increase the precision of verification tools --- reducing the number of false alarms --- while retaining the efficiency of current techniques, resulting in model-checking tools that are more reliable and usable. During this fellowship, we will construct a state-of-the-art verification framework, unifying several prototypical tools and requiring novel model-checking techniques, and permitting new ideas to be experimented with quickly. The framework will be tested on real-world software to ensure its usability and reliability. It will accurately model difficult programming paradigms, such as modern concurrent behaviours and "higher-order" constructs (increasingly embraced by state-of-the-art programming languages). The research will be carried out at Imperial College London, and will bring together researchers at Oxford University, Universite Paris-Est, and Universite Paris-Diderot as well as the CARP project, based across several universities and companies world-wide, and researchers at Microsoft Research, Cambridge.