ABSTRACT. In this tutorial, I will present SEAHORN, a software verification framework. The key distinguishing feature of SEAHORN is its modular design that separates the concerns of the syntax of the programming language, its operational semantics, and the verification semantics. SEAHORN encompasses several novelties: it (

1. encodes verification conditions using an efficient yet precise inter-procedural technique,
2. provides flexibility in the verification semantics to allow different levels of precision, 
3. leverages the state-of-the-art in software model checking and abstract interpretation for verification, and 
4. uses Horn-clauses as an intermediate language to represent verification conditions which simplifies interfacing with multiple verification tools based on Horn-clauses. 

SEAHORN provides users with a powerful verification tool and provides researchers with an extensible and customizable framework for experimenting with new software verification techniques.

ABSTRACT. In the frame of our previous experiments for proof based synthesis of sorting algorithms for lists and for binary trees, we employed certain special techniques which are able to generate multiple variants of sorting and merging, by investigating all combinations of auxiliary functions available for composing objects (lists, respectively trees). The purpose of this paper is to describe this technique and the results obtained. We present the main principles and the application of this technique to merging of sorted binary trees into a sorted one. Remarkably, merging requires a nested recursion, for which an appropriate induction principle is difficult to guess. Our method is able to find it automatically by using a general Noetherian induction and the combinatorial technique.

ABSTRACT. One of the core problems in real-time systems, finding a feasible schedule for a certain task set, is subject to alternative solutions given the various system constraints. While preemptive scheduling has benefited from a large number of significant results, the non-preemptive case has still room for improvement. This paper extends our previous results regarding the minimum number of processors required for getting a feasible schedule and the possible ways of improving the well known traditional scheduling algorithms in the case of non-preemptive, multiprocessor systems. The improvements refer to handling the situations when the already determined minimum number of processors proves insufficient, and also to extending an existing technique which allows the algorithm to overcome some stalling situations.

ABSTRACT. In this paper we sketch out a smart home system (and the reasoning mechanism behind it) designed to improve the living experience of the severly impaired, relying on logic, brain-computer interfacing (BCI) and mobile sensor agents. The exists a significant social category of people who due to either old age or conditions such as paralysis lose their ability to manage their own lives. Such persons are compelled to rely on others in order to manage their finances, expenses, daily necessities such as eating or turning on the television or dialing an emergency number. In our previous research we have described a manner in which to model emotions, as captured via BCI. Here, we extend this model to abstract and concrete concepts and employ epistemic logic and a logic of trust in order to allow communication between the person and heterogenous agents via a BCI headset. We firstly describe a formal model for expressing reasoning as captured in its cortical projection. Secondly, we describe a communication protocol that uses a logic of trust that allows the user to give commands to specific listening agents. The system should use reasoning and logic to learn from the user commands they receive and configure routines that correspond to the usual preferences and needs. Finally, the agents, on receiving and corroborating data from other sensors that relate to vital signs of the user or that otherwise identify a crisis situation, should be able to decide when to change their task priorities and the system should ad hoc self-configure in order to provide best assistance to the user.

ABSTRACT. Venn diagrams for sets are in use for more than a century. Multiset theory developed in the last decades, and although it has many applications in mathematics and computer science, remains relatively modest compared to set theory. We introduce Venn diagrams for finite multisets and show how they simplify the analysis of multisets and their submultisets. Venn diagrams are very useful in proofs involving multisets and multiset orders, especially considering the complications introduced by the multiplicity of elements in multisets.

We compare the Venn diagrams for finite multisets with the corresponding Venn diagrams for sets. Thus, we present two types of Venn diagrams for finite multisets, a simple one that looks like a diagram for sets, but with areas that are not necessarily disjoint, and a complex one (compared to sets), but with disjoint areas.

We show by examples that by using diagrams in a proof involving multisets the chance of making mistakes decreases significantly, in contradiction to the usual belief that diagrams tend to introduce errors in proofs.

ABSTRACT. In this paper, we present some stability results which are implies some fixed point theorem. We study two types of stability.

ABSTRACT. We obtain an extension of some coupled fixed point results.

ABSTRACT. The concept of local contraction was presented by Martins da Rocha and Filipe Vailakis in [Martins-da-Rocha,Filipe, Vailakis, Yiannis, Exis- tence and uniqueness of a xed point for local contractions, Econometrica, vol.78, No.3 (May, 2010) 1127-1141], meanwhile the almost contractive mappings was introduced by V. Berinde in [Berinde, V., Approximat- ing xed points of weak contractions using the Picard iteration Nonlinear Analysis Forum 9(2004) No.1, 43-53]. In this paper we want to unify these two concepts, so we dene the almost local contractions. Then we are going to study the xed points of almost local contractions. The main result of this paper state an existence theorem and also an exis- tence and uniqueness theorem for almost local contractions with constant coecient of contraction. The most general case of variable coecient of contraction is presented at the end of this work, in the existence theorem for xed points of almost local contractions.

ABSTRACT. We merge the concepts of convex contraction, due to Istratescu [Some fixed point theorems for convex contraction mappings and convex nonexpansive mappings. I. Libertas Math. 1 (1981), 151--163] and almost contraction, introduced in [Berinde, Vasile, Approximating fixed points of weak contractions using the Picard iteration. Nonlinear Anal. Forum 9 (2004), no. 1, 43--53] and thus obtain a larger class of contractive type mappings for which we state and prove some basic fixed point theorems.

ABSTRACT. Differential privacy has recently grabbed the attention of many privacy researchers. It provides a way to get useful information about sensitive data without revealing much about any one individual. It enjoys many nice compositionality properties not shared by other approaches to privacy, including, in particular, robustness against side-knowledge.
Designing differentially private mechanisms from scratch can be a challenging task. One way to make it easier to construct new differential private mechanisms is to design a system which allows more complex mechanisms (programs) to be built from differentially private building blocks in principled way, so that the resulting programs are guaranteed to be differentially private by construction. In this talk I will review the basic ideas of differential privacy and describe a new accounting principle for building differentially private programs. It is based on a simple generalisation of classic differential privacy which we call Personalised Differential Privacy, in which each individual has its own personal privacy budget. We will describe how this can be implemented in an interactive query system using the concept of lineage tracing from database theory.
(Describing joint work with Hamid Ebadi and Gerardo Schneider)

ABSTRACT. In this tutorial we focus on how to protect the confidentiality of user data in web applications in the presence of active attackers. In particular, driven by the architecture of a typical web application, we focus on the scenario where the attacker is able to inject malicious code into the application. By injecting code into the application the attacker is able to access and steal all data the application has access to, unless additional security mechanisms are put into place. The question to which we have been seeking the answer is how such mechanism might be constructed.

The tutorial is built around JSFlow [1], a security-enhanced JavaScript interpreter employing fine grained tracking of information-flow, and a simplified example web application, Hrafn, constructed to be open for various code injection  attacks, e.g., via buggy or compromised 3rd party services or via malicious user content.

Based on different practical attacks against Hrafn we illustrate the power of code injection attacks and discuss the current protection mechanism and their weaknesses. Thereafter we show how dynamic information-flow control provides a uniform line of defense against the attacks both in theory and in practice, using JSFlow. At the very end, we leave the focus on the client side to briefly discuss how information flow control can be leveraged on an application-wide level to provide confidentiality of user data.

ABSTRACT. We consider some recent iterative schemes due to Kadioglu and Yildirim (2014), Thakur et al. (2014) and Phuengrattana and Suantai (2011) for further investigations. In this paper, we compare rate of convergence among the mentioned iterative schemes when applied to well-known contraction mappings. Also, we show that all these iterative schemes are equivalent as all converge to the same fixed point of a contraction mapping. Finally we obtain some data dependence results for the mentioned iterative schemes. Mathematics Subject Classification: 47H09; 4710 Keywords: Iterative schemes; contraction mappings; strong convergence; rate of convergence; data dependence

References [1] N. Kadioglu and I. Yildirim, “Approximating fixed points of nonexpansive mappings by a faster iteration process,” http://arxiv.org/abs/1402, 2014. [2] W. Phuengrattana and S. Suantai, “On the rate of convergence of Mann, Ishikawa, Noor and SP-iterations for continuous functions on an arbitrary interval,” Journal of Computational and Applied Mathematics, vol. 235, no. 9, pp. 3006–3014, 2011. [3] D. Thakur, B. S. Thakur and M. Postolache, New iteration scheme for numerical reckoning fixed points of nonexpansive mappings, J. Inequal. Appl. 328 (2014), 15 pages.

ABSTRACT. Some new additional conditions are proposed to estimate a posteriori error and to guarantee the strong convergence of Picard and Mann iterations in the case of a strongly demicontractive mapping. The simple formulas for a posteriori error estimation are given in both cases. Results on the convergence properties state that the sequence given by each of the two considered methods converges strongly to a fixed point provided that the considered mapping is strongly demicontractive and satisfies some expansive type conditions (orbital expansive or quasi expansive).

ABSTRACT. We prove some common fixed point results in fuzzy metric spaces and derive corresponding coupled coincidence point results in this setting.

References:

J-X Fang, Common coupled fixed point theorems for hybrid $\varphi$-contractions in probabilistic and fuzzy metric spaces, to appear

V. Lakshmikantam V, L. Ciric, Coupled fixed point theorems for nonlinear contractions in partially ordered metric spaces, Nonlinear Anal 70 (2009), 4341-4349.

A. Harandi-Amini, D. Mihet, Common fixed points and coupled coincidence points in preordered fuzzy metric spaces, submitted

ABSTRACT. The purpose of this paper is to transpose some of the results regarding the coupled fixed point theory, developed by T. Gnana Bhaskar and V. Lakshmikantham, using the approaches of Hichem Ben-El-Mechaiekh and M. S. Asgari, B. Mousavi. The first approach replaces the partial ordered relation from the Ran-Reurings fixed point theorem with a transitive one, whereas the second one uses a reflexive-only relation. Our aim is to obtain some generalized theorems, containing a more simple symmetrical condition, based on these results.

ABSTRACT. This paper presents some interesting informations about the fixed point theorems for non-self multi-valued almost contractions. It starts from presenting the strict contractions and then we extend this notion to weak contractions single-valued mappings and multi-valued mappings. This helps us to introduce the non-self operators which will show us the next result: Let X be a Banach space, K a non-empty closed subset of X and let T:K→X be a non-self almost contraction. If T has the so called property (M) and satisfies Rothe’s boundary condition, the T has fixed point in K. This theorem links us to what we are going to study, i.e. non-self multi-valued almost contractions.

ABSTRACT. As a general rule, each user must provide the used tool with particular values of its input parameters. An inexperienced user may hardly figure out their values and the tool developer must define their default values in order to help her/him. The used tool implements an algorithm, based on some model of reality. The model is as good as the data, measured in the reality and on the model are close. The problem under our investigation is to determine automatically the "good" default parameters. We provide the user with an advanced analytical method to help her/him to make better decisions about the values of the required parameters.

In this paper, we present an approach to solve the problem with the help of multi-criteria optimization that is new in this formulation. We demonstrate our approach in closer details using an example from the automatic definition of optimal default parameters for real-time merging of visual objects. However, our making decisions approach is generic and may be used for any kind of such inverse problems.

ABSTRACT. Forecasting has always been of interest. Whether one’s field is finance, health or seismology, being able to predict future values based on previously gathered data proves to be invaluable when taking decisions about that future. In this paper, we research machine learning techniques for prediction on time series and choose the best models that fit our use case, Smart Farm, in which we distributedly analyze time series received from farm-monitoring sensors. On time series with short term dependencies, like temperature or pressure, we make predictions with Hidden Markov Models, whilst for those with long range dependencies, like ground wind speeds or precipitations, we use Recurrent Neural Networks with Long Short-Term Memory architecture.

ABSTRACT. In this paper we present a real-time, continuous vital signs monitoring system based on a Multi-agent architecture. Real-time remote monitoring of the patient’s vital signs and generating alerts in case of emergency situations is of great importance in healthcare. Several tiny sensors attached on the patient’s body can collect physiological measurements of vital signs, and transmit them to a remote server, from where it can be consulted by a physician. Using Wireless Body Area Networks (WBANs) technology patients can move freely and perform daily tasks while being monitored. In such systems energy is the most valuable resource. Most energy is consumed by data transmission related operations. Therefore local processing of vital signs and continuously updating vital signs thresholds, according to the activity caried by the patient, on each sensor node, and sending data only when abnormal values exceed these ranges, can significantly reduce data transmission and save battery life.

ABSTRACT. In recent years the study of the convergence of iterative methods has been widely investigated. In this talk, we want to show how the asymptotic behavior of the ratio of the coefficients involved in an iterative method influences the convergence of the algorithm itself.

ABSTRACT. By using geometric conditions on a function and its domain, we introduce an iterative sequence and prove that it converges to a fixed point of the map. Applications are also discussed.

ABSTRACT. Following Maia's fixed point theorem and Presic fixed point theorem, which are the extensions of Banach fixed point theorem, we present a Presic-Maia fixed point theorem which is a unification of these two theorems. Some new research directions are also presented.

ABSTRACT. The article approaches the issue of convergence accuracy of standard genetic algorithms using fixed point theory operates on a simplicial triangulation of searching space and then generates the integer labels at the vertices. The algorithm uses a new operator of increase the dimension used at the actualization of the population which acts on non-labeled individuals, turning them into fully labeled individuals and convergence condition of the population is reached when all simplex are fully labeled. Global optimum point was obtained by applying the Hessian matrix on fully labeled simplex. Genetic algorithm was built in C Sharp, appealing through MapleEngine.cs function in Maple program for solving mathematical equations and for easier and faster in demonstrating the efficiency and stability of the algorithm was created a friendly interface for the user. The optained results demonstrate a global optimization capability greater than the classical genetic algorithms that ensure due triangulation combined with the random local research, thus eliminating the possibility that the algorithm to stop in a local extreme point.