Research in the PPLV group spans from fundamental work in logic and the semantics of programs to automated tools for verification and program analysis. Its goal is to produce mathematically rigorous concepts and techniques that aid in the construction and analysis of computer systems. Mechanised program verification, in particular, has seen a surge of interest in the research community in the past decade. This has been triggered by practical advances where in special domains -- in avionics code and in device drivers and other small systems programs -- we have seen fully automated verification of selected properties such as memory safety and termination and API protocol conformance. Our work on Separation Logic and the Space Invader tool, and on SLAM and Terminator, has played a part in this resurgence. We believe that these advances are suggestive of much more, of more general practical impact for verification and program analysis across the spectrum of computer systems. The recent work on automatic verification can be seen as part of a larger trend in applied logic, where mathematical logic is moving from being a conceptual mathematical tool to a collection of techniques which can be used by practicing engineers and scientists in solving the concrete problems that they face. Building on our core focus on program analysis, part of the aim of the PPLV group is applied logic outreach, in such areas as AI and security and biology and economics.