Time filter

Source Type

Di Fratta G.,University of Bristol | Robbins J.M.,University of Bristol | Slastikov V.,University of Bristol | Zarnescu A.,University of Sussex | Zarnescu A.,Institute of Mathematics Simion Stoilow
Journal of Nonlinear Science | Year: 2015

We investigate prototypical profiles of point defects in two-dimensional liquid crystals within the framework of Landau–de Gennes theory. Using boundary conditions characteristic of defects of index k/2, we find a critical point of the Landau–de Gennes energy that is characterised by a system of ordinary differential equations. In the deep nematic regime, (Formula presented.) small, we prove that this critical point is the unique global minimiser of the Landau–de Gennes energy. For the case (Formula presented.), we investigate in greater detail the regime of vanishing elastic constant (Formula presented.), where we obtain three explicit point defect profiles, including the global minimiser. © 2015 Springer Science+Business Media New York

Popescu A.,TU Munich | Popescu A.,Institute of Mathematics Simion Stoilow | Holzl J.,TU Munich | Nipkow T.,TU Munich
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Year: 2012

We perform a formal analysis of compositionality techniques for proving possibilistic noninterference for a while language with parallel composition. We develop a uniform framework where we express a wide range of noninterference variants from the literature and compare them w.r.t. their contracts: the strength of the security properties they ensure weighed against the harshness of the syntactic conditions they enforce. This results in a simple implementable algorithm for proving that a program has a specific noninterference property, using only compositionality, which captures uniformly several security type-system results from the literature and suggests a further improved type system. All formalism and theorems have been mechanically verified in Isabelle/HOL. © 2012 Springer-Verlag Berlin Heidelberg.

Papageorgiou N.S.,National Technical University of Athens | Rdulescu V.D.,King Abdulaziz University | Rdulescu V.D.,Institute of Mathematics Simion Stoilow
Advanced Nonlinear Studies | Year: 2015

We consider a nonlinear parametric Robin problem driven by the p-Laplacian. We assume that the reaction exhibits a concave term near the origin. First we prove a multiplicity theorem producing three solutions with sign information (positive, negative and nodal) without imposing any growth condition near ±∞ on the reaction. Then, for problems with subcritical reaction, we produce two more solutions of constant sign, for a total of five solutions. For the semilinear problem (that is, for p = 2), we generate a sixth solution but without any sign information. Our approach is variational, coupled with truncation, perturbation and comparison techniques and with Morse theory.

Diaconescu R.,Institute of Mathematics Simion Stoilow | Tutu I.,Coala Normal Superioar Bucureti
Theoretical Computer Science | Year: 2011

We develop module algebra for structured specifications with model oriented denotations. Our work extends the existing theory with specification building operators for non-protecting importation modes and with new algebraic rules (most notably for initial semantics) and upgrades the pushout-style semantics of parameterized modules to capture the (possible) sharing between the body of the parameterized modules and the instances of the parameters. We specify a set of sufficient abstract conditions, smoothly satisfied in the actual situations, and prove the isomorphism between the parallel and the serial instantiation of multiple parameters. Our module algebra development is done at the level of abstract institutions, which means that our results are very general and directly applicable to a wide variety of specification and programming formalisms that are rigorously based upon some logical system. © 2011 Elsevier B.V. All rights reserved.

Vuza D.T.,Institute of Mathematics Simion Stoilow | Vladescu M.,Polytechnic University of Bucharest
Proceedings of the 2015 7th International Conference on Electronics, Computers and Artificial Intelligence, ECAI 2015 | Year: 2015

This paper presents an automated platform designed to allow a quick and accurate determination of the spatial characteristics of emitting and receiving optoelectronic devices. The platform can determine the radiation pattern of light emitting diodes (LEDs) and the sensitivity pattern of photodiodes (PDs) and phototransistors (PTs) and integrated photodetectors (IPD) as well. There are described the measurement method, the hardware that has been designed and the software that has been developed in order to achieve through an automated process the procedures needed for the spatial characterization of optoelectronic devices. © 2015 IEEE.

Popescu A.,TU Munich | Popescu A.,Institute of Mathematics Simion Stoilow | Holzl J.,TU Munich | Nipkow T.,TU Munich
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Year: 2013

We present an Isabelle formalization of probabilistic noninterference for a multi-threaded language with uniform scheduling. Unlike in previous settings from the literature, here probabilistic behavior comes from both the scheduler and the individual threads, making the language more realistic and the mathematics more challenging. We study resumption-based and trace-based notions of probabilistic noninterference and their relationship, and also discuss compositionality w.r.t. the language constructs and type-system-like syntactic criteria. The formalization uses recent development in the Isabelle probability theory library. © Springer International Publishing 2013.

Traytel D.,TU Munich | Popescu A.,TU Munich | Popescu A.,Institute of Mathematics Simion Stoilow | Blanchette J.C.,TU Munich
Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012 | Year: 2012

Interactive theorem provers based on higher-order logic (HOL) traditionally follow the definitional approach, reducing high-level specifications to logical primitives. This also applies to the support for datatype definitions. However, the internal datatype construction used in HOL4, HOL Light, and Isabelle/HOL is fundamentally noncompositional, limiting its efficiency and flexibility, and it does not cater for codatatypes. We present a fully modular framework for constructing (co)datatypes in HOL, with support for mixed mutual and nested (co)recursion. Mixed (co)recursion enables type definitions involving both datatypes and codatatypes, such as the type of finitely branching trees of possibly infinite depth. Our framework draws heavily from category theory. The key notion is that of a bounded natural functor - -an enriched type constructor satisfying specific properties preserved by interesting categorical operations. Our ideas are implemented as a definitional package in Isabelle, addressing a frequent request from users. © 2012 IEEE.

Loading Institute of Mathematics Simion Stoilow collaborators
Loading Institute of Mathematics Simion Stoilow collaborators