Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B

Event-B is a formal method for modeling and verification of discrete transition systems. Event-B development yields proof obligations that must be verified (i.e. proved valid) in order to keep the produced models consistent. Satisfiability Modulo Theory solvers are automated theorem provers used to verify the satisfiability of logic formulas considering a background theory (or combination of theories). SMT solvers not only handle large firstorder formulas, but can also generate models and proofs, as well as identify unsatisfiable subsets of hypotheses (unsat-cores). Tool support for Event-B is provided by the Rodin platform: an extensible Eclipse based IDE that combines modeling and proving features. A SMT plug-in for Rodin has been developed intending to integrate alternative, efficient verification techniques to the platform. We implemented a series of complements to the SMT solver plug-in for Rodin, namely improvements to the user interface for when proof obligations are reported as invalid by the plug-in. Additionally, we modified some of the plug-in features, such as support for proof generation and unsat-core extraction, to comply with the SMT-LIB standard for SMT solvers. We undertook tests using applicable proof obligations to demonstrate the new features. The contributions described can potentially affect productivity in a positive manner.

Síntese de ferritas de cobalto e níquel dopadas com zinco e caracterização de suas propriedades eletromagnéticas

This work shows that the synthesis by combustion is a prominent alternative to obtain ceramic powders of higher oxides, nanostructured and of high purity, as the ferrites of formulas Co(1-x)Zn(x)Fe2O4 e Ni(1-x)Zn(x)Fe2O4 with x ranging from 0.2 mols, in a range from 0.2 ≤ x ≥ 1.0 mol, that presents magnetic properties in coexistence of ferroelectric and ferrimagnetic states, which can be used in antennas of micro tapes and selective surfaces of low frequency in a range of miniaturized microwaves, without performance loss. The obtainment occurred through the combustion process, followed by appropriate physical processes and ordered to the utilization of the substrate sinterization process, it gave us a ceramic material, of high purity degree in a nanometric scale. The Vibrating Sample Magnetometer (VSM) analysis showed that those ferritic materials presents parameters, as materials hysteresis, that have own behavior of magnetic materials of good quality, in which the magnetization states can be suddenly changed with a relatively small variation of the field intensity, having large applications on the electronics field. The X-ray Diffraction (XRD) analysis of the ceramic powders synthesized at 900 °C, characterize its structural and geometrical properties, the crystallite size and the interplanar spacing. Other analysis were developed, as Scanning Electron Microscopy (SEM), X-ray Fluorescence (XRF), electric permittivity and the tangent loss, in high frequencies, through the equipment ZVB - 14 Vector Network Analyzer 10 MHz-14 GHz, of ROHDE & SCHWART.

Manutenção da Heterozigosidade em populações de plantas autógamas

Neste trabalho objetivou-se verificar, teoricamente , a possibilidade de manutenção de heterozigotos, em populações de plantas autógamas, na presença e na ausência de seleção dependente de frequência (SDF). Considerou-se apenas um loco com dois alelos. Utilizou-se a dedução algébrica de formulas referentes a alguns modelos de populações e um programa para simular a sucessão das gerações em uma calculadora científica avançada. Comparou-se os resultados do modelo com os dados obtidos experimentalmente por Allard e Workman (1963) e por Harding, Allard e Smeltzer (1966). Os coeficientes de determinação foram 0,9653 e 0,9166 para a primeira e a segunda comparação, respectivamente. Estes coeficientes indicam que o modelo D representa de modo bastante fidedigno as variações observadas em populações experimentais de plantas predominantemente autógamas

Formulação e caracterização de matérias-primas para revestimento cerâmico Semi-Poroso com adição de chamote de telhas

The ceramics industry in Piauí is nowadays with 55 industries where 11 are in Teresina which is the mainstream of the state, producing 55 million shingles; in which 10 % is of this production is wasted being sometimes thrown on the margins of rivers, roads and highways provoking an environmental degradation. The main goal of this work is to verify the potential of producing semi porous ceramic using grog of shingles, on the first part of this work bodies-of-proof were produced from a basic formula of an industry, doping it with 5 %, 10 %, 15 % and 20 % in mass and in the second part of this work some bodies-of-proof were produced from a formula where one raw material was substituted by 50 % of grog and another substituting it all by grog, bodies-of-proof made of a basic formula previously announced was used for experiment control.The grog and the raw materials were characterized by: particle size analysis , thermal differential analysis, X ray diffraction , X ray fluorescence, an thermal gravimetric analysis and rational analyses. The bodies-of-proof were sintetisized in an industrial oven obeying the normal cycle adopted by an industry, with peak temperatures of 1135 oC and a fast burning cycle of 25 minutes having as energetic fuel liquefied petroleum gas . The pieces that were obtained by this were submersed in rehearsed physics of: water absorption of, apparent specific mass, apparent porosity, lineal retraction, rupture tension to the flexural and dilatometry; mineralogical analysis for X ray diffraction; and microstructural for electronic microscope of sweeping. For all the formulas with addition of grog, superior priorities to the requested by the requirements for semi porous and for the formula to F2-2,5 superior priorities to standard formulas which justifies the incorporation of the shingles in mass for the semi porous ceramic