Polynomial function intervals for floating-point software verification

The focus of our work is the verification of tight functional properties of numerical programs, such as showing that a floating-point implementation of Riemann integration computes a close approximation of the exact integral. Programmers and engineers writing such programs will benefit from verification tools that support an expressive specification language and that are highly automated. Our work provides a new method for verification of numerical software, supporting a substantially more expressive language for specifications than other publicly available automated tools. The additional expressivity in the specification language is provided by two constructs. First, the specification can feature inclusions between interval arithmetic expressions. Second, the integral operator from classical analysis can be used in the specifications, where the integration bounds can be arbitrary expressions over real variables. To support our claim of expressivity, we outline the verification of four example programs, including the integration example mentioned earlier. A key component of our method is an algorithm for proving numerical theorems. This algorithm is based on automatic polynomial approximation of non-linear real and real-interval functions defined by expressions. The PolyPaver tool is our implementation of the algorithm and its source code is publicly available. In this paper we report on experiments using PolyPaver that indicate that the additional expressivity does not come at a performance cost when comparing with other publicly available state-of-the-art provers. We also include a scalability study that explores the limits of PolyPaver in proving tight functional specifications of progressively larger randomly generated programs. © 2014 Springer International Publishing Switzerland.

JCML: A specification language for the runtime verification of Java Card programs

COSTA, Umberto Souza; MOREIRA, Anamaria Martins; MUSICANTE, Matin A.; SOUZA NETO, Plácido A. JCML: A specification language for the runtime verification of Java Card programs. Science of Computer Programming. [S.l]: [s.n], 2010.

Specification and Runtime Verification of Java Card Programs

COSTA, Umberto Souza da; MOREIRA, Anamaria Martins; MUSICANTE, Martin A. Specification and Runtime Verification of Java Card Programs. Electronic Notes in Theoretical Computer Science. [S.l:s.n], 2009.

JCML: A specification language for the runtime verification of Java Card programs

COSTA, Umberto Souza; MOREIRA, Anamaria Martins; MUSICANTE, Matin A.; SOUZA NETO, Plácido A. JCML: A specification language for the runtime verification of Java Card programs. Science of Computer Programming. [S.l]: [s.n], 2010.

Specification and Runtime Verification of Java Card Programs

COSTA, Umberto Souza da; MOREIRA, Anamaria Martins; MUSICANTE, Martin A. Specification and Runtime Verification of Java Card Programs. Electronic Notes in Theoretical Computer Science. [S.l:s.n], 2009.

Event-Code Interaction Directed Test Cases

The Graphical User Interface (GUI) is an integral component of contemporary computer software. A stable and reliable GUI is necessary for correct functioning of software applications. Comprehensive verification of the GUI is a routine part of most software development life-cycles. The input space of a GUI is typically large, making exhaustive verification difficult. GUI defects are often revealed by exercising parts of the GUI that interact with each other. It is challenging for a verification method to drive the GUI into states that might contain defects. In recent years, model-based methods, that target specific GUI interactions, have been developed. These methods create a formal model of the GUI’s input space from specification of the GUI, visible GUI behaviors and static analysis of the GUI’s program-code. GUIs are typically dynamic in nature, whose user-visible state is guided by underlying program-code and dynamic program-state. This research extends existing model-based GUI testing techniques by modelling interactions between the visible GUI of a GUI-based software and its underlying program-code. The new model is able to, efficiently and effectively, test the GUI in ways that were not possible using existing methods. The thesis is this: Long, useful GUI testcases can be created by examining the interactions between the GUI, of a GUI-based application, and its program-code. To explore this thesis, a model-based GUI testing approach is formulated and evaluated. In this approach, program-code level interactions between GUI event handlers will be examined, modelled and deployed for constructing long GUI testcases. These testcases are able to drive the GUI into states that were not possible using existing models. Implementation and evaluation has been conducted using GUITAR, a fully-automated, open-source GUI testing framework.

Development of JADE, a new software for the verification and validation of nuclear data libraries

Nuclear cross sections are the pillars onto which the transport simulation of particles and radiations is built on. Since the nuclear data libraries production chain is extremely complex and made of different steps, it is mandatory to foresee stringent verification and validation procedures to be applied to it. The work here presented has been focused on the development of a new python based software called JADE, whose objective is to give a significant help in increasing the level of automation and standardization of these procedures in order to reduce the time passing between new libraries releases and, at the same time, increasing their quality. After an introduction to nuclear fusion (which is the field where the majority of the V\&V action was concentrated for the time being) and to the simulation of particles and radiations transport, the motivations leading to JADE development are discussed. Subsequently, the code general architecture and the implemented benchmarks (both experimental and computational) are described. After that, the results coming from the major application of JADE during the research years are presented. At last, after a final discussion on the objective reached by JADE, the possible brief, mid and long time developments for the project are discussed.

O livro como recurso didatico no ensino do futebol

Universidade Estadual de Campinas. Faculdade de Educação Física

Estado nutricional e qualidade de vida de escolares de 7 a 10 anos de idade de municípios da Região Metropolitana de Campinas

Universidade Estadual de Campinas. Faculdade de Educação Física

Proposta e verificação da validade de testes de limiar anaerobico para natação do nado crawl

Universidade Estadual de Campinas . Faculdade de Educação Física

Canoagem velocidade : dinamica das cargas de treinamento no macrociclo e a dinamica da alteração de marcadores funcionais externos

Universidade Estadual de Campinas . Faculdade de Educação Física

Aplicação da escala de qualidade de vida em crianças de 07 a 12 anos praticantes de atividade fisica em academia e suas relações com a aptidão fisica

Universidade Estadual de Campinas . Faculdade de Educação Física

Validade de equipamento eletronico informatizado para analise de movimentos tecnicos do voleibol : um estudo na categoria juvenil

Universidade Estadual de Campinas . Faculdade de Educação Física

Teste de banco com carga continua para analise do volume de oxigenio (VO2) predito e analisado por tempo de esforço em pessoas treinadas (TRD), ativas (ATV) e destreinadas (DTR) a partir dos 13 anos : proposta de validação

Universidade Estadual de Campinas . Faculdade de Educação Física

Obtaining and stability verification of superconducting phases of the Nb-Al and Nb-Sn systems by mechanical alloying and low-temperature heat treatments

The development of Nb(3)Al and Nb(3)Sn superconductors is of great interest for the applied superconductivity area. These intermetallics composites are obtained normally by heat treatment reactions at high temperature. Processes that allow formation of the superconducting phases at lower temperatures (<1000 degrees C), particularly for Nb(3)Al, are of great interest. The present work studies phase formation and stability of Nb(3)Al and Nb(3)Sn superconducting phases using mechanical alloying (high energy ball milling). Our main objective was to form composites near stoichiometry, which could be transformed into the superconducting phases using low-temperature heat treatments. High purity Nb-Sn and Nb-Al powders were mixed to generate the required superconducting phases (Nb-25at.%Sn and Nb-25at.%Al) in an argon atmosphere glove-box. After milling in a Fritsch mill, the samples were compressed in a hydraulic uniaxial press and encapsulated in evacuated quartz tubes for heat treatment. The compressed and heat treated samples were characterized using X-ray diffractometry. Microstructure and chemical analysis were accomplished using scanning electron microscopy and energy dispersive spectrometry. Nb(3)Al XRD peaks were observed after the sintering at 800 degrees C for the sample milled for 30 h. Nb(3)Sn XRD peaks could be observed even before the heat treatment. (C) 2009 Elsevier B.V. All rights reserved.