Optimizations for Embedded Systems imply ad-hoc tunings and performance improvements, as well as development of specific algorithms and data structures, well suited for embedded platforms. This work first focuses on efficient and accurate implementation of visual search algorithms on embedded GPUs adopting the OpenGL ES and OpenCL languages. Considering embedded GPUs that support only low precision computations, we discuss the problems arising during the design phase, and we detail our implementation choices, focusing on two well-known key-point detectors SIFT and ALP. We illustrate how to re-engineering standard Gaussian Scale Space computations to mobile multi-core parallel GPUs using the OpenGL ES language transforming standard, i.e., single (or double) precision floating-point computations, to reduced-precision GPU arithmetic without precision loss. We also concentrate on an efficient and accurate OpenCL implementation of the main MPEG Compact Descriptors for Visual Search (CDVS) stages. We introduce new techniques to adapt sequential algorithms to parallel processing. Furthermore, to reduce the memory accesses, and efficiently distribute the OpenCL kernels workload, we use new approaches to store and retrieve CDVS information on proper GPU data structures. Secondly, we focus on improving the scalability of formal verification algorithms for Embedded System design models. We address the problem of reducing the size of Craig interpolants generated within inner steps of SAT-based Unbounded Model Checking. Craig interpolants are obtained from refutation proofs of unsatisfiable SAT runs, in terms of and/or circuits of linear size, w.r.t. the proof. We also consider the issue of property grouping, property decomposition, and property coverage in model checking problems. Property grouping, i.e., clustering, is a valuable solution whenever (very) large sets of properties have to be proven for a given model. On the other hand, property decomposition can be effective whenever a given property turns-out (or it is expected) to be “hard-to-prove”. Overall, experimental results are promising and demonstrate that our solutions have a speed-up over the existing ones and can be really beneficial if appropriately integrated in a new environment.