The soaring number of autonomous robots are bringing to prominence the insidiousness and potential impact of their faults. In turn, these faults highlight the limitations of existing program analysis techniques, which are being challenged not just by the immense input space, but also by the integration of cyber and physical semantics, the multiple sources of uncertainty, and the incorporation of machine learning components. In this talk I will provide an overview of some mobile robotic platforms and frameworks that we have targeted to ground our research efforts in addressing these challenges, the range of properties that those systems are meant to satisfy from robustness to ethical concerns, and the body of techniques we have developed to address those challenges that span from type analysis to oracle analysis, and from DNN verification to trajectory and environment generation.