This course will introduce the fundamental theory in computer-aided verification and synthesis for building provably dependable computer systems. The topics covered include logic specifications, modeling formalisms, verification techniques, and inductive synthesis strategies. A special focus of the course is on interplay between deductive reasoning (logical inference and constraint solving) and inductive inference (learning from data). We will also survey applications of these techniques to a wide range of problems in hardware, software, cyber-physical systems, robotics, and biology.