Contribuições para verificação automática de applets javacard

The widespread growth in the use of smart cards (by banks, transport services, and cell phones, etc) has brought an important fact that must be addressed: the need of tools that can be used to verify such cards, so to guarantee the correctness of their software. As the vast majority of cards that are being developed nowadays use the JavaCard technology as they software layer, the use of the Java Modeling Language (JML) to specify their programs appear as a natural solution. JML is a formal language tailored to Java. It has been inspired by methodologies from Larch and Eiffel, and has been widely adopted as the de facto language when dealing with specification of any Java related program. Various tools that make use of JML have already been developed, covering a wide range of functionalities, such as run time and static checking. But the tools existent so far for static checking are not fully automated, and, those that are, do not offer an adequate level of soundness and completeness. Our objective is to contribute to a series of techniques, that can be used to accomplish a fully automated and confident verification of JavaCard applets. In this work we present the first steps to this. With the use of a software platform comprised by Krakatoa, Why and haRVey, we developed a set of techniques to reduce the size of the theory necessary to verify the specifications. Such techniques have yielded very good results, with gains of almost 100% in all tested cases, and has proved as a valuable technique to be used, not only in this, but in most real world problems related to automatic verification

Teorias f(R) de gravidade na formulação de Palatini

In this dissertation, after a brief review on the Einstein s General Relativity Theory and its application to the Friedmann-Lemaitre-Robertson-Walker (FLRW) cosmological models, we present and discuss the alternative theories of gravity dubbed f(R) gravity. These theories come about when one substitute in the Einstein-Hilbert action the Ricci curvature R by some well behaved nonlinear function f(R). They provide an alternative way to explain the current cosmic acceleration with no need of invoking neither a dark energy component, nor the existence of extra spatial dimensions. In dealing with f(R) gravity, two different variational approaches may be followed, namely the metric and the Palatini formalisms, which lead to very different equations of motion. We briefly describe the metric formalism and then concentrate on the Palatini variational approach to the gravity action. We make a systematic and detailed derivation of the field equations for Palatini f(R) gravity, which generalize the Einsteins equations of General Relativity, and obtain also the generalized Friedmann equations, which can be used for cosmological tests. As an example, using recent compilations of type Ia Supernovae observations, we show how the f(R) = R − fi/Rn class of gravity theories explain the recent observed acceleration of the universe by placing reasonable constraints on the free parameters fi and n. We also examine the question as to whether Palatini f(R) gravity theories permit space-times in which causality, a fundamental issue in any physical theory [22], is violated. As is well known, in General Relativity there are solutions to the viii field equations that have causal anomalies in the form of closed time-like curves, the renowned Gödel model being the best known example of such a solution. Here we show that every perfect-fluid Gödel-type solution of Palatini f(R) gravity with density and pressure p that satisfy the weak energy condition + p 0 is necessarily isometric to the Gödel geometry, demonstrating, therefore, that these theories present causal anomalies in the form of closed time-like curves. This result extends a theorem on Gödel-type models to the framework of Palatini f(R) gravity theory. We derive an expression for a critical radius rc (beyond which causality is violated) for an arbitrary Palatini f(R) theory. The expression makes apparent that the violation of causality depends on the form of f(R) and on the matter content components. We concretely examine the Gödel-type perfect-fluid solutions in the f(R) = R−fi/Rn class of Palatini gravity theories, and show that for positive matter density and for fi and n in the range permitted by the observations, these theories do not admit the Gödel geometry as a perfect-fluid solution of its field equations. In this sense, f(R) gravity theory remedies the causal pathology in the form of closed timelike curves which is allowed in General Relativity. We also examine the violation of causality of Gödel-type by considering a single scalar field as the matter content. For this source, we show that Palatini f(R) gravity gives rise to a unique Gödeltype solution with no violation of causality. Finally, we show that by combining a perfect fluid plus a scalar field as sources of Gödel-type geometries, we obtain both solutions in the form of closed time-like curves, as well as solutions with no violation of causality

Fundamentação cinética da estatística não gaussiana : efeitos em politrópicas

Considering a non-relativistic ideal gas, the standard foundations of kinetic theory are investigated in the context of non-gaussian statistical mechanics introduced by Kaniadakis. The new formalism is based on the generalization of the Boltzmann H-theorem and the deduction of Maxwells statistical distribution. The calculated power law distribution is parameterized through a parameter measuring the degree of non-gaussianity. In the limit = 0, the theory of gaussian Maxwell-Boltzmann distribution is recovered. Two physical applications of the non-gaussian effects have been considered. The first one, the -Doppler broadening of spectral lines from an excited gas is obtained from analytical expressions. The second one, a mathematical relationship between the entropic index and the stellar polytropic index is shown by using the thermodynamic formulation for self-gravitational systems

Termoestatística quântica: uma abordagem via estatísticas não-gaussianas

Considering a quantum gas, the foundations of standard thermostatistics are investigated in the context of non-Gaussian statistical mechanics introduced by Tsallis and Kaniadakis. The new formalism is based on the following generalizations: i) Maxwell- Boltzmann-Gibbs entropy and ii) deduction of H-theorem. Based on this investigation, we calculate a new entropy using a generalization of combinatorial analysis based on two different methods of counting. The basic ingredients used in the H-theorem were: a generalized quantum entropy and a generalization of collisional term of Boltzmann equation. The power law distributions are parameterized by parameters q;, measuring the degree of non-Gaussianity of quantum gas. In the limit q

Uma justificava da validade do teorema fundamental da álgebra para o ensino médio

Among several theorems which are taught in basic education some of them can be proved in the classroom and others do not, because the degree of difficulty of its formal proof. A classic example is the Fundamental Theorem of Algebra which is not proved, it is necessary higher-level knowledge in mathematics. In this paper, we justify the validity of this theorem intuitively using the software Geogebra. And, based on [2] we will present a clear formal proof of this theorem that is addressed to school teachers and undergraduate students in mathematics

A relação de Euler para poliedros

In this paper we analyze the Euler Relation generally using as a means to visualize the fundamental idea presented manipulation of concrete materials, so that there is greater ease of understanding of the content, expanding learning for secondary students and even fundamental. The study is an introduction to the topic and leads the reader to understand that the notorious Euler Relation if inadequately presented, is not sufficient to establish the existence of a polyhedron. For analyzing some examples, the text inserts the idea of doubt, showing cases where it is not fit enough numbers to validate the Euler Relation. The research also highlights a theorem certainly unfamiliar to many students and teachers to research the polyhedra, presenting some very simple inequalities relating the amounts of edges, vertices and faces of any convex polyhedron, which clearly specifies the conditions and sufficient necessary for us to see, without the need of viewing the existence of the solid screen. And so we can see various polyhedra and facilitate understanding of what we are exposed, we will use Geogebra, dynamic application that combines mathematical concepts of algebra and geometry and can be found through the link http://www.geogebra.org

Connection coefficients and zeros of orthogonal polynomials

We discuss an old theorem of Obrechkoff and some of its applications. Some curious historical facts around this theorem are presented. We make an attempt to look at some known results on connection coefficients, zeros and Wronskians of orthogonal polynomials from the perspective of Obrechkoff's theorem. Necessary conditions for the positivity of the connection coefficients of two families of orthogonal polynomials are provided. Inequalities between the kth zero of an orthogonal polynomial p(n)(x) and the largest (smallest) zero of another orthogonal polynomial q(n)(x) are given in terms of the signs of the connection coefficients of the families {p(n)(x)} and {q(n)(x)}, An inequality between the largest zeros of the Jacobi polynomials P-n((a,b)) (x) and P-n((alpha,beta)) (x) is also established. (C) 2001 Elsevier B.V. B.V. All rights reserved.

Landau and Kolmogoroff type polynomial inequalities

Let 0

On the behaviour of zeros of Jacobi polynomials

Denote by x(n,k)(alpha, beta) and x(n,k) (lambda) = x(n,k) (lambda - 1/2, lambda - 1/2) the zeros, in decreasing order, of the Jacobi polynomial P-n((alpha, beta))(x) and of the ultraspherical (Gegenbauer) polynomial C-n(lambda)(x), respectively. The monotonicity of x(n,k)(alpha, beta) as functions of a and beta, alpha, beta > - 1, is investigated. Necessary conditions such that the zeros of P-n((a, b)) (x) are smaller (greater) than the zeros of P-n((alpha, beta))(x) are provided. A. Markov proved that x(n,k) (a, b) < x(n,k)(α, β) (x(n,k)(a, b) > x(n,k)(alpha, beta)) for every n is an element of N and each k, 1 less than or equal to k less than or equal to n if a > alpha and b < β (a < alpha and b > beta). We prove the converse statement of Markov's theorem. The question of how large the function could be such that the products f(n)(lambda) x(n,k)(lambda), k = 1,..., [n/2] are increasing functions of lambda, for lambda > - 1/2, is also discussed. Elbert and Siafarikas proved that f(n)(lambda) = (lambda + (2n(2) + 1)/ (4n + 2))(1/2) obeys this property. We establish the sharpness of their result. (C) 2002 Elsevier B.V. (USA).

Uma caracterização de grafos imersíveis

Este trabalho é motivado pelo resultado de Berge, que é uma generalização do teorema de Tutte o qual expressamos na forma: Dado o grafo G de ordem |V(G)| eni(G) o número de arestas em um emparelhamento máximo, existe um conjunto X de vértices de G tal que |V(G)|+|X| - ômega(G\X) - 2n(G)=0, onde ômega(G\X) é o número de componentes de ordem ímpar de G\X. Tal expressão chamamos a equação de Tutte-Berge associada de G, e escrevemos simplesmente T(G; X)=0. Os grafos podem ser classificados a partir das soluções da equação de Tutte-Berge. Um grafo G é chamado imersível se, e somente se, T(G; X)=0 possui pelo menos um conjunto solução não vazio de vértices, e G é denominado não imersível se, e somente se, o conjunto vazio é a única solução de T(G; X)=0. O resultado principal deste artigo é a caracterização de grafos imersíveis pelos conjuntos antifatores completos, além disso, provamos que os grafos fatoráveis estão contidos na classe dos imersíveis.

Bi-Lipschitz A-triviality of map germs and Newton filtrations

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Dynamics at infinity and other global dynamical aspects of Shimizu-Morioka equations

Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)

LOSS of EXPONENTIAL STABILITY FOR A THERMOELASTIC SYSTEM WITH MEMORY

Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)

Global dynamics of stationary solutions of the extended Fisher-Kolmogorov equation

Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)

Vector and axial-vector correlators in a non-local chiral quark model

The behavior of the non-perturbative parts of the isovector-vector and isovector and isosinglet axial-vector correlators at Euclidean momenta is studied in the framework of a covariant chiral quark model with non-local quark-quark interactions. The gauge covariance is ensured with the help of the P-exponents, with the corresponding modification of the quark-current interaction vertices taken into account. The low- and high-momentum behavior of the correlators is compared with the chiral perturbation theory and with the QCD operator product expansion, respectively. The V-A combination of the correlators obtained in the model reproduces quantitatively the ALEPH and OPAL data on hadronic tau decays, transformed into the Euclidean domain via dispersion relations. The predictions for the electromagnetic pi(+/-) - pi(0) mass difference and for the pion electric polarizability are also in agreement with the experimental values. The topological susceptibility of the vacuum is evaluated as a function of the momentum, and its first moment is predicted to be chi'(0) approximate to (50 MeV)(2). In addition, the fulfillment of the Crewther theorem is demonstrated.