Tool-supported invariant-based programming

The development of correct programs is a core problem in computer science. Although formal verification methods for establishing correctness with mathematical rigor are available, programmers often find these difficult to put into practice. One hurdle is deriving the loop invariants and proving that the code maintains them. So called correct-by-construction methods aim to alleviate this issue by integrating verification into the programming workflow. Invariant-based programming is a practical correct-by-construction method in which the programmer first establishes the invariant structure, and then incrementally extends the program in steps of adding code and proving after each addition that the code is consistent with the invariants. In this way, the program is kept internally consistent throughout its development, and the construction of the correctness arguments (proofs) becomes an integral part of the programming workflow. A characteristic of the approach is that programs are described as invariant diagrams, a graphical notation similar to the state charts familiar to programmers. Invariant-based programming is a new method that has not been evaluated in large scale studies yet. The most important prerequisite for feasibility on a larger scale is a high degree of automation. The goal of the Socos project has been to build tools to assist the construction and verification of programs using the method. This thesis describes the implementation and evaluation of a prototype tool in the context of the Socos project. The tool supports the drawing of the diagrams, automatic derivation and discharging of verification conditions, and interactive proofs. It is used to develop programs that are correct by construction. The tool consists of a diagrammatic environment connected to a verification condition generator and an existing state-of-the-art theorem prover. Its core is a semantics for translating diagrams into verification conditions, which are sent to the underlying theorem prover. We describe a concrete method for 1) deriving sufficient conditions for total correctness of an invariant diagram; 2) sending the conditions to the theorem prover for simplification; and 3) reporting the results of the simplification to the programmer in a way that is consistent with the invariantbased programming workflow and that allows errors in the program specification to be efficiently detected. The tool uses an efficient automatic proof strategy to prove as many conditions as possible automatically and lets the remaining conditions be proved interactively. The tool is based on the verification system PVS and i uses the SMT (Satisfiability Modulo Theories) solver Yices as a catch-all decision procedure. Conditions that were not discharged automatically may be proved interactively using the PVS proof assistant. The programming workflow is very similar to the process by which a mathematical theory is developed inside a computer supported theorem prover environment such as PVS. The programmer reduces a large verification problem with the aid of the tool into a set of smaller problems (lemmas), and he can substantially improve the degree of proof automation by developing specialized background theories and proof strategies to support the specification and verification of a specific class of programs. We demonstrate this workflow by describing in detail the construction of a verified sorting algorithm. Tool-supported verification often has little to no presence in computer science (CS) curricula. Furthermore, program verification is frequently introduced as an advanced and purely theoretical topic that is not connected to the workflow taught in the early and practically oriented programming courses. Our hypothesis is that verification could be introduced early in the CS education, and that verification tools could be used in the classroom to support the teaching of formal methods. A prototype of Socos has been used in a course at Åbo Akademi University targeted at first and second year undergraduate students. We evaluate the use of Socos in the course as part of a case study carried out in 2007.

Group-invariant solutions of semilinear Schrodinger equations in multi-dimensions

Symmetry group methods are applied to obtain all explicit group-invariant radial solutions to a class of semilinear Schr¨odinger equations in dimensions n = 1. Both focusing and defocusing cases of a power nonlinearity are considered, including the special case of the pseudo-conformal power p = 4/n relevant for critical dynamics. The methods involve, first, reduction of the Schr¨odinger equations to group-invariant semilinear complex 2nd order ordinary differential equations (ODEs) with respect to an optimal set of one-dimensional point symmetry groups, and second, use of inherited symmetries, hidden symmetries, and conditional symmetries to solve each ODE by quadratures. Through Noether’s theorem, all conservation laws arising from these point symmetry groups are listed. Some group-invariant solutions are found to exist for values of n other than just positive integers, and in such cases an alternative two-dimensional form of the Schr¨odinger equations involving an extra modulation term with a parameter m = 2−n = 0 is discussed.

Size invariant measures of association: characterization and difficulties

A measure of association is row-size invariant if it is unaffected by the multiplication of all entries in a row of a cross-classification table by a same positive number. It is class-size invariant if it is unaffected by the multiplication of all entries in a class (i.e., a row or a column). We prove that every class-size invariant measure of association as-signs to each m x n cross-classification table a number which depends only on the cross-product ratios of its 2 x 2 subtables. We propose a monotonicity axiom requiring that the degree of association should increase after shifting mass from cells of a table where this mass is below its expected value to cells where it is above .provided that total mass in each class remains constant. We prove that no continuous row-size invariant measure of association is monotonic if m ≥ 4. Keywords: association, contingency tables, margin-free measures, size invariance, monotonicity, transfer principle.

Invariant discretizations of partial differential equations

Un algorithme permettant de discrétiser les équations aux dérivées partielles (EDP) tout en préservant leurs symétries de Lie est élaboré. Ceci est rendu possible grâce à l'utilisation de dérivées partielles discrètes se transformant comme les dérivées partielles continues sous l'action de groupes de Lie locaux. Dans les applications, beaucoup d'EDP sont invariantes sous l'action de transformations ponctuelles de Lie de dimension infinie qui font partie de ce que l'on désigne comme des pseudo-groupes de Lie. Afin d'étendre la méthode de discrétisation préservant les symétries à ces équations, une discrétisation des pseudo-groupes est proposée. Cette discrétisation a pour effet de transformer les symétries ponctuelles en symétries généralisées dans l'espace discret. Des schémas invariants sont ensuite créés pour un certain nombre d'EDP. Dans tous les cas, des tests numériques montrent que les schémas invariants approximent mieux leur équivalent continu que les différences finies standard.

Invariant density for a class of initial distributions under quadratic mapping

For the discrete-time quadratic map xt+1=4xt(1-xt) the evolution equation for a class of non-uniform initial densities is obtained. It is shown that in the t to infinity limit all of them approach the invariant density for the map.

Invariant Characterization of Neural Systems

It is shown that the invariant integral, viz., the Kolmogorov second entropy, is eminently suited to characterize EEG quantitatively. The estimation obtained for a "clinically normal" brain is compared with a previous result obtained from the EEG of a person under epileptic seizure.

Cooling and heating by adiabatic magnetization in Ni50Mn34In16 magnetic shape-memory alloy

We report on measurements of the adiabatic temperature change in the inverse magnetocaloric Ni50Mn34In16 alloy. It is shown that this alloy heats up with the application of a magnetic field around the Curie point due to the conventional magnetocaloric effect. In contrast, the inverse magnetocaloric effect associated with the martensitic transition results in the unusual decrease of temperature by adiabatic magnetization. We also provide magnetization and specific heat data which enable to compare the measured temperature changes to the values indirectly computed from thermodynamic relationships. Good agreement is obtained for the conventional effect at the second-order paramagnetic-ferromagnetic phase transition. However, at the first-order structural transition the measured values at high fields are lower than the computed ones. Irreversible thermodynamics arguments are given to show that such a discrepancy is due to the irreversibility of the first-order martensitic transition.

Form-invariant bivariate weighted models

In this paper the class of continuous bivariate distributions that has form-invariant weighted distribution with weight function w(x1, x2) ¼ xa1 1 xa2 2 is identified. It is shown that the class includes some well known bivariate models. Bayesian inference on the parameters of the class is considered and it is shown that there exist natural conjugate priors for the parameters

State-of-the-Art: Transformation Invariant Descriptors

As the popularity of digital videos increases, a large number illegal videos are being generated and getting published. Video copies are generated by performing various sorts of transformations on the original video data. For effectively identifying such illegal videos, the image features that are invariant to various transformations must be extracted for performing similarity matching. An image feature can be its local feature or global feature. Among them, local features are powerful and have been applied in a wide variety of computer vision aplications .This paper focuses on various recently proposed local detectors and descriptors that are invariant to a number of image transformations.

Rotation Invariant Real-time Face Detection and Recognition System

In this report, a face recognition system that is capable of detecting and recognizing frontal and rotated faces was developed. Two face recognition methods focusing on the aspect of pose invariance are presented and evaluated - the whole face approach and the component-based approach. The main challenge of this project is to develop a system that is able to identify faces under different viewing angles in realtime. The development of such a system will enhance the capability and robustness of current face recognition technology. The whole-face approach recognizes faces by classifying a single feature vector consisting of the gray values of the whole face image. The component-based approach first locates the facial components and extracts them. These components are normalized and combined into a single feature vector for classification. The Support Vector Machine (SVM) is used as the classifier for both approaches. Extensive tests with respect to the robustness against pose changes are performed on a database that includes faces rotated up to about 40 degrees in depth. The component-based approach clearly outperforms the whole-face approach on all tests. Although this approach isproven to be more reliable, it is still too slow for real-time applications. That is the reason why a real-time face recognition system using the whole-face approach is implemented to recognize people in color video sequences.

Rotation Invariant Object Recognition from One Training Example

Local descriptors are increasingly used for the task of object recognition because of their perceived robustness with respect to occlusions and to global geometrical deformations. Such a descriptor--based on a set of oriented Gaussian derivative filters-- is used in our recognition system. We report here an evaluation of several techniques for orientation estimation to achieve rotation invariance of the descriptor. We also describe feature selection based on a single training image. Virtual images are generated by rotating and rescaling the image and robust features are selected. The results confirm robust performance in cluttered scenes, in the presence of partial occlusions, and when the object is embedded in different backgrounds.

Matching Interest Points Using Projective Invariant Concentric Circles

We present a new method to perform reliable matching between different images. This method exploits a projective invariant property between concentric circles and the corresponding projected ellipses to find complete region correspondences centered on interest points. The method matches interest points allowing for a full perspective transformation and exploiting all the available luminance information in the regions. Experiments have been conducted on many different data sets to compare our approach to SIFT local descriptors. The results show the new method offers increased robustness to partial visibility, object rotation in depth, and viewpoint angle change.

Scale-invariant moving finite elements for nonlinear partial differential equations in two dimensions

A scale-invariant moving finite element method is proposed for the adaptive solution of nonlinear partial differential equations. The mesh movement is based on a finite element discretisation of a scale-invariant conservation principle incorporating a monitor function, while the time discretisation of the resulting system of ordinary differential equations is carried out using a scale-invariant time-stepping which yields uniform local accuracy in time. The accuracy and reliability of the algorithm are successfully tested against exact self-similar solutions where available, and otherwise against a state-of-the-art h-refinement scheme for solutions of a two-dimensional porous medium equation problem with a moving boundary. The monitor functions used are the dependent variable and a monitor related to the surface area of the solution manifold. (c) 2005 IMACS. Published by Elsevier B.V. All rights reserved.