As verification efforts using interactive theorem proving grow, we are in need of certified algorithms in computer algebra to tackle problems over the real numbers. This is important because uncertified procedures can drastically increase the size of the trust base and under- mine the overall confidence established by interactive theorem provers, which usually rely on a small kernel to ensure the soundness of derived results. This thesis describes an ongoing effort using the Isabelle theorem prover to certify the cylindrical algebraic decomposition (CAD) algorithm, which has been widely implemented to solve non-linear problems in various engineering and mathematical fields. Because of the sophistication of this algorithm, people are in doubt of the correctness of its implementation when deploying it to safety-critical verification projects, and such doubts motivate this thesis. In particular, this thesis proposes a library of real algebraic numbers, whose distinguishing features include a modular architecture and a sign determination algorithm requiring only rational arithmetic. With this library, an Isabelle tactic based on univariate CAD has been built in a certificate-based way: external, untrusted code delivers solutions in the form of certificates that are checked within Isabelle. To lay the foundation for the multivariate case, I have formalised various analytical results including Cauchy's residue theorem and the bivariate case of the projection theorem of CAD. During this process, I have also built a tactic to evaluate winding numbers through Cauchy indices and verified procedures to count complex roots in some domains. The formalisation effort in this thesis can be considered as the first step towards a certified computer algebra system inside a theorem prover, so that various engineering projections and mathematical calculations can be carried out in a high-confidence framework.

Submitted by Sandra Pereira (srpereira@ufrrj.br) on 2018-08-24T14:22:59Z No. of bitstreams: 1 2010 - Regiane de Souza Costa.pdf: 976546 bytes, checksum: 76af99d4f7ecb28633203926dc58048a (MD5) / Made available in DSpace on 2018-08-24T14:22:59Z (GMT). No. of bitstreams: 1 2010 - Regiane de Souza Costa.pdf: 976546 bytes, checksum: 76af99d4f7ecb28633203926dc58048a (MD5) Previous issue date: 2010-12-10 / Funda??o Carlos Chagas Filho de Amparo ? Pesquisa do Estado do RJ, FAPERJ, Brasil. / This dissertation is based on research conducted at the Technical College of Rural University (CTUR / UFRRJ), with the participation of students in 3rd year of the Technical Course in Agricultural Structure, one of the teachers of Physical Education School and also an observer of pedagogical processes. Brings with it the main concern a critical and emancipatory Physical Education and its elements for the human / professional formation. Its objective is to investigate the manifestation of physical education as a curricular component of the Vocation Agricultural Education from CTUR. For this, it?s focused on a theoretical and methodological framework that allowed capture changes in everyday reality. Approach based on Qualitative Research in Education, and the Methodology of Action Research as its main key element. Under this reasoning was possible to know at first, such as physical education was manifested in the school years, based on the relation-goals-assessment methods. Secondly, the descriptions were used as the setting of Physical Education in previous years that were built by the group involved in research, workshops, aiming to foster a process of awareness / reflection on the plurality of interpretations that this area is able to present. The guiding themes of the workshops were based on the Matrix Reference to the New ENEM 2009, rephrasing the National Examination of Secondary Education proposed by the Ministry of Education. Combining the data obtained from the questionnaires, interviews, reports from students and the observations indicated that the ?spacetimes? teaching physical education, when treated in its many possible interpretations, relying on the criticality, presents itself as an important component for the formation of man, in a holistic manner. / Esta disserta??o est? fundamentada na pesquisa realizada no Col?gio T?cnico da Universidade Rural (CTUR/UFRRJ), contando com a participa??o de estudantes do 3? ano do Curso T?cnico em Agropecu?ria Org?nica, um dos professores de Educa??o F?sica da escola e, ainda, uma observadora dos processos pedag?gicos. Traz consigo a preocupa??o central com uma Educa??o F?sica cr?tica e emancipat?ria e seus elementos constitutivos para a forma??o humana/profissional. Apresentou como objetivo geral investigar a manifesta??o da Educa??o F?sica Escolar como componente curricular da Educa??o Profissional Agr?cola do CTUR. Para tanto, debru?ou-se sobre um aporte te?rico-metodol?gico que permitiu captar as varia??es cotidianas dispostas na realidade. Contou com a Abordagem Qualitativa de Pesquisa em Educa??o, tendo a Metodologia da Pesquisa-A??o o seu principal eixo orientador. Sob esta fundamenta??o foi poss?vel conhecer, num primeiro momento, como a Educa??o F?sica se manifestou nos anos escolares, com base na rela??o objetivos-m?todos-avalia??o. Num segundo momento, foram utilizadas as descri??es quanto ? configura??o da Educa??o F?sica nos anos anteriores para que fossem constru?das, pelo coletivo envolvido na pesquisa, oficinas tem?ticas, visando possibilitar um processo de sensibiliza??o/reflex?o diante da pluralidade de interpreta??es que esta ?rea ? capaz de apresentar. Os temas orientadores das oficinas foram baseados na Matriz de Refer?ncia para o Novo ENEM 2009, reformula??o do Exame Nacional do Ensino M?dio proposta pelo Minist?rio da Educa??o. A conjuga??o dos dados obtidos com a aplica??o dos question?rios, das entrevistas, dos relatos dos estudantes e das observa??es dos espa?ostempos pedag?gicos sinalizou que a Educa??o F?sica, quando tratada nas suas m?ltiplas possibilidades interpretativas, apoiando-se na criticidade, se apresenta como um importante componente para a forma??o do homem, numa perspectiva hol?stica.

The goal of this thesis is the development of support for test generation and animation based on object-oriented specifications. We aim particularly to take advantage of state-of-the-art satisfiability solving techniques by using an appropriate representation of object-oriented data. While automated test generation seeks a large set of data to execute an implementation on, animation performs computations that comply with a specification based on user-provided input data. Animation is a valuable technique for validating specifications.As a foundation of this work, we present clarifications and a partial formalization of the Object Constraint Language (OCL) as well as some extensions in order to allow for test generation and animation based on OCL specifications.For test generation, we have implemented several enhancements to HOL-TestGen, a tool built on top of the Isabelle theorem proving system that generates tests from specifications in Higher-Order Logic (HOL). We show how SMT solvers can be used to solve various types of constraints in HOL and present a modular approach to case splitting for deriving test cases. The latter facilitates the introduction of splitting rules that are tailored to object-oriented specifications.For animation, we implemented the tool OCLexec for animating OCL specifications. OCLexec generates from operation contracts corresponding Java implementations that call an SMT-based constraint solver at runtime.

Zugl.: Leiden, Univ., Diss., 2006

Zugl.: Bremen, Univ., Diss., 2005

Techn. University, Diss., 2002--München.

We present a series of improvements to the Hybrid system, a formal theory implemented in Isabelle/HOL to support specifying and reasoning about formal systems using higher-order abstract syntax (HOAS). We modify Hybrid's type of terms, which is built definitionally in terms of de Bruijn indices, to exclude at the type level terms with `dangling' indices. We strengthen the injectivity property for Hybrid's variable-binding operator, and develop rules for compositional proof of its side condition, avoiding conversion from HOAS to de Bruijn indices. We prove representational adequacy of Hybrid (with these improvements) for a lambda-calculus-like subset of Isabelle/HOL syntax, at the level of set-theoretic semantics and without unfolding Hybrid's definition in terms of de Bruijn indices. In further work, we prove an induction principle that maintains some of the benefits of HOAS even for open terms. We also present a case study of the formalization in Hybrid of a small programming language, Mini-ML with mutable references, including its operational semantics and a type-safety property. This is the largest case study in Hybrid to date, and the first to formalize a language with mutable references. We compare four variants of this formalization based on the two-level approach adopted by Felty and Momigliano in other recent work on Hybrid, with various specification logics (SLs), including substructural logics, formalized in Isabelle/HOL and used in turn to encode judgments of the object language. We also compare these with a variant that does not use an intermediate SL layer. In the course of the case study, we explore and develop new proof techniques, particularly in connection with context invariants and induction on SL statements.

We present a series of improvements to the Hybrid system, a formal theory implemented in Isabelle/HOL to support specifying and reasoning about formal systems using higher-order abstract syntax (HOAS). We modify Hybrid's type of terms, which is built definitionally in terms of de Bruijn indices, to exclude at the type level terms with `dangling' indices. We strengthen the injectivity property for Hybrid's variable-binding operator, and develop rules for compositional proof of its side condition, avoiding conversion from HOAS to de Bruijn indices. We prove representational adequacy of Hybrid (with these improvements) for a lambda-calculus-like subset of Isabelle/HOL syntax, at the level of set-theoretic semantics and without unfolding Hybrid's definition in terms of de Bruijn indices. In further work, we prove an induction principle that maintains some of the benefits of HOAS even for open terms. We also present a case study of the formalization in Hybrid of a small programming language, Mini-ML with mutable references, including its operational semantics and a type-safety property. This is the largest case study in Hybrid to date, and the first to formalize a language with mutable references. We compare four variants of this formalization based on the two-level approach adopted by Felty and Momigliano in other recent work on Hybrid, with various specification logics (SLs), including substructural logics, formalized in Isabelle/HOL and used in turn to encode judgments of the object language. We also compare these with a variant that does not use an intermediate SL layer. In the course of the case study, we explore and develop new proof techniques, particularly in connection with context invariants and induction on SL statements.

We present a series of improvements to the Hybrid system, a formal theory implemented in Isabelle/HOL to support specifying and reasoning about formal systems using higher-order abstract syntax (HOAS). We modify Hybrid's type of terms, which is built definitionally in terms of de Bruijn indices, to exclude at the type level terms with `dangling' indices. We strengthen the injectivity property for Hybrid's variable-binding operator, and develop rules for compositional proof of its side condition, avoiding conversion from HOAS to de Bruijn indices. We prove representational adequacy of Hybrid (with these improvements) for a lambda-calculus-like subset of Isabelle/HOL syntax, at the level of set-theoretic semantics and without unfolding Hybrid's definition in terms of de Bruijn indices. In further work, we prove an induction principle that maintains some of the benefits of HOAS even for open terms. We also present a case study of the formalization in Hybrid of a small programming language, Mini-ML with mutable references, including its operational semantics and a type-safety property. This is the largest case study in Hybrid to date, and the first to formalize a language with mutable references. We compare four variants of this formalization based on the two-level approach adopted by Felty and Momigliano in other recent work on Hybrid, with various specification logics (SLs), including substructural logics, formalized in Isabelle/HOL and used in turn to encode judgments of the object language. We also compare these with a variant that does not use an intermediate SL layer. In the course of the case study, we explore and develop new proof techniques, particularly in connection with context invariants and induction on SL statements.

We present a series of improvements to the Hybrid system, a formal theory implemented in Isabelle/HOL to support specifying and reasoning about formal systems using higher-order abstract syntax (HOAS). We modify Hybrid's type of terms, which is built definitionally in terms of de Bruijn indices, to exclude at the type level terms with `dangling' indices. We strengthen the injectivity property for Hybrid's variable-binding operator, and develop rules for compositional proof of its side condition, avoiding conversion from HOAS to de Bruijn indices. We prove representational adequacy of Hybrid (with these improvements) for a lambda-calculus-like subset of Isabelle/HOL syntax, at the level of set-theoretic semantics and without unfolding Hybrid's definition in terms of de Bruijn indices. In further work, we prove an induction principle that maintains some of the benefits of HOAS even for open terms. We also present a case study of the formalization in Hybrid of a small programming language, Mini-ML with mutable references, including its operational semantics and a type-safety property. This is the largest case study in Hybrid to date, and the first to formalize a language with mutable references. We compare four variants of this formalization based on the two-level approach adopted by Felty and Momigliano in other recent work on Hybrid, with various specification logics (SLs), including substructural logics, formalized in Isabelle/HOL and used in turn to encode judgments of the object language. We also compare these with a variant that does not use an intermediate SL layer. In the course of the case study, we explore and develop new proof techniques, particularly in connection with context invariants and induction on SL statements.