We develop tools for the analysis and verification of safety and security properties in mobile code (e.g., Java or Python), in cryptographic communication protocols (e.g., those based on elliptic curves or post-quantum cryptography), or in generic software systems (e.g., poor management of shared resources). The benefit provided by VRAIN at UPV in this regard is the development of advanced techniques for reducing the solution search space, which has been integrated into various applications developed in research centres around the world.