RaML Resource Aware ML Nomos A language for digital contracts Marlin Automatic and interactive quantitative analysis ReSyn Resource-guided program synthesis Q-CUDA Qualitative and Quantitative Verification of CUDA Code