Esta tesis aborda la paralelización de los métodos de Krylov con reinicio para problemas de valores propios y valores singulares (SVD). Estos métodos son de naturaleza iterativa y resultan adecuados para encontrar unos pocos valores propios o singulares de problemas dispersos. El procedimiento de ortogonalización suele ser la parte más costosa de este tipo de métodos, por lo que ha recibido especial atención en esta tesis, proponiendo y validando nuevos algoritmos para mejorar sus prestaciones paralelas. La implementación se ha realizado en el marco de la librería SLEPc, que proporciona una interfaz orientada a objetos para la resolución iterativa de problemas de valores propios o singulares. SLEPc está basada en la librería PETSc, que dispone de implementaciones paralelas de métodos iterativos para la resolución de sistemas lineales, precondicionadores, matrices dispersas y vectores. Ambas librerías están optimizadas para su ejecución en máquinas paralelas de memoria distribuida y con problemas dispersos de gran dimensión. Esta implementación incorpora los métodos para valores propios de Arnoldi con reinicio explícito, de Lanczos (incluyendo variantes semiortogonales) con reinicio explícito, y versiones de Krylov-Schur (equivalente al reinicio implícito) para problemas no Hermitianos y Hermitianos (Lanczos con reinicio grueso). Estos métodos comparten una interfaz común, permitiendo su comparación de forma sencilla, característica que no está disponible en otras implementaciones. Las mismas técnicas utilizadas para problemas de valores propios se han adaptado a los métodos de Golub-Kahan-Lanczos con reinicio explícito y grueso para problemas de valores singulares, de los que no existe ninguna otra implementación paralela con paso de mensajes. Cada uno de los métodos se ha validado mediante una batería de pruebas con matrices procedentes de aplicaciones reales. Las prestaciones paralelas se han medido en máquinas tipo cluster, comprobando una buena escalabilidad inc / Tomás Domínguez, A. (2009). Implementación paralela de métodos de Krylov con reinicio para problemas de valores propios y singulares [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/5082 / Palancia

The increasing complexity of software systems has led to the development of sophisticated formal Methodologies for verifying and correcting data and programs. In general, establishing whether a program behaves correctly w.r.t. the original programmer s intention or checking the consistency and the correctness of a large set of data are not trivial tasks as witnessed by many case studies which occur in the literature. In this dissertation, we face two challenging problems of verification and correction. Specifically, verification and correction of declarative programs, and the verification and correction of Web sites (i.e. large collections of semistructured data). Firstly, we propose a general correction scheme for automatically correcting declarative, rule-based programs which exploits a combination of bottom-up as well as topdown inductive learning techniques. Our hybrid hodology is able to infer program corrections that are hard, or even impossible, to obtain with a simpler,automatic top-down or bottom-up learner. Moreover, the scheme will be also particularized to some well-known declarative programming paradigm: that is, the functional logic and the functional programming paradigm. Secondly, we formalize a framework for the automated verification of Web sites which can be used to specify integrity conditions for a given Web site, and then automatically check whether these conditions are fulfilled. We provide a rule-based, formal specification language which allows us to define syntactic as well as semantic properties of the Web site. Then, we formalize a verification technique which detects both incorrect/forbidden patterns as well as lack of information, that is, incomplete/missing Web pages. Useful information is gathered during the verification process which can be used to repair the Web site. So, after a verification phase, one can also infer semi-automatically some possible corrections in order to fix theWeb site. The methodology is based on a novel rewrit / Ballis, D. (2005). Rule-Based Software Verification and Correction [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/1948 / Palancia