Remencius T.,Connexx S.r.L. |
Sillitti A.,Free University of Bozen Bolzano |
Succi G.,Innopolis University
Information Sciences | Year: 2016
Most of the research effort in the area of software analysis is focused on the perspective of the developer (as in "software developing company") and the ways how the software development process could be improved. However, that is not the only type of software assessment common in the industry. There are also assessments that are commissioned by other parties, such as the primary recipients of the software solutions or courts dealing with legal cases that are related to software products or services. This work presents one such case-study that was performed for a public administration in Italy. The paper describes the assessment itself and also points out the need for more focused research by providing a comparison between developer-oriented and customer-oriented assessment types. © 2015 Elsevier Inc. All rights reserved.
Catano N.,Innopolis University |
Rivera V.,Innopolis University
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Year: 2016
Event-B is a formal specification language and a methodology used to build software systems. Formal specifications are more useful when they can be executed. An executable formal specification provides insight on the behaviour of the system being modelled w.r.t an expected behaviour. This paper presents a tool that generates executable implementations of Event-B models. The tool is implemented as a plug-in of the Rodin platform, an Eclipse IDE that provides a set of tools to work with Event-B models. Our tool has extensively been used for generating code for Event-B models of Android applications, reactive systems, Smart Cards, searching algorithms, among others. The first author regularly uses EventB2Java in teaching to help master students of Software Engineering to get a better grasp of the behaviour of a model in Event-B and to detect inconsistencies in the model. © Springer International Publishing Switzerland 2016.
Johard L.,Innopolis University |
Ruffaldi E.,Sant'Anna School of Advanced Studies
Pattern Recognition Letters | Year: 2016
Trajectories and parameterized curves are data types of growing importance. Many measures for such data have been proposed in order to provide analogues to the mean and variance of vectors. We identify a counterintuitive oscillating behavior of dynamic time warp-based averages on certain data sets. We present an algorithm that combines ideas from both self-organizing maps and dynamic time warping that avoids these oscillations and hence promises more representative curve averages. These improvements also allow for accurate estimation of the piece-wise variance for a set of general N-dimensional trajectories. The run-time performance is demonstrated on movement data from rowing, where we are able to provide performance feedback in real-time to users in a simulator. © 2016 Elsevier B.V.
Hadian A.,Iran University of Science and Technology |
Nobari S.,Innopolis University |
Minaei-Bidgoli B.,Iran University of Science and Technology |
Qu Q.,Innopolis University
Proceedings of the ACM SIGMOD International Conference on Management of Data | Year: 2016
Real-world graphs are not always publicly available or sometimes do not meet specific research requirements. These challenges call for generating synthetic networks that follow properties of the realworld networks. Barabási-Albert (BA) is a well-known model for generating scale-free graphs, i.e graphs with power-law degree distribution. In BA model, the network is generated through an iterative stochastic process called preferential attachment. Although BA is highly demanded, due to the inherent complexity of the preferential attachment, this model cannot be scaled to generate billionnode graphs. In this paper, we propose ROLL-tree, a fast in-memory roulette wheel data structure that accelerates the BA network generation process by exploiting the statistical behaviors of the underlying growth model. Our proposed method has the following properties: (a) Fast: It performs+1000 times faster than the state-of-the-art on a single node PC; (b) Exact: It strictly follows the BA model, using an efficient data structure instead of approximation techniques; (c) Generalizable: It can be adapted for other "richget-richer" stochastic growth models. Our extensive experiments prove that ROLL-tree can effectively accelerate graph-generation through the preferential attachment process. On a commodity single processor machine, for example, ROLL-tree generates a scalefree graph of 1.1 billion nodes and 6.6 billion edges (the size of Yahoo's Webgraph) in 62 minutes while the state-of-the-art (SA) takes about four years on the same machine. © 2016 ACM.
Meyer B.,ETH Zurich |
Meyer B.,Innopolis University
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Year: 2015
Deadlocks remain one of the biggest threats to concurrent programming. Usually, the best programmers can expect is dynamic deadlock detection, which is only a palliative. Object-oriented programs, with their rich reference structure and the resulting presence of aliasing, raise additional problems. The technique developed in this paper relies on the “alias calculus” to offer a completely static and completely automatic analysis of concurrent object-oriented programs. The discussion illustrates the technique by applying it to two versions of the “dining philosophers” program, of which it proves that the first is deadlock-free and the second deadlock-prone. © Springer-Verlag Berlin Heidelberg 2015.
Brown J.A.,Innopolis University
2015 IEEE Conference on Computational Intelligence in Bioinformatics and Computational Biology, CIBCB 2015 | Year: 2015
Side Effect Machines (SEMs) have been used as a evolutionary representation in a variety of studies dealing with the classification of data for bioinformatic studies. However, up to this point there has been no formalism of the SEM in terms of its representational ability and placement within the Chomsky hierarchy; only a statement that it is a generalization of a Deterministic Finite Automation (DFA), without proof, has been provided. This paper aims to rectify that situation by presenting a formal look at SEMs in terms of the languages which they are known to accept. We give a constructive proof of how a SEM is a generalization of a DFA and are therefore able to be used to accept languages. Constructive proofs for SEMs accepting families of context-free and context-sensitive languages are also provided. © 2015 IEEE.
Brown J.A.,Innopolis University
2015 IEEE Conference on Computational Intelligence and Games, CIG 2015 - Proceedings | Year: 2015
Recent evaluations of Procedural Content Generation (PCG) methods have examined the use of personas as part of there evaluative functions. Personas, models of a user, have a number of complaints leveled against them by researchers as to their use as design tools: That there is poor empirical proof that they improve the design process, poor definitions lead to them not modeling actual uses, and they do not give any quantitative information for evaluation using a scientific approach. Examined is a framework in which a persona is not just defined as a model of a user, but is a contract list of player goals and actions available in the game. By defining a persona as a goal driven AI, it joins the idea of personas with a more qualitative evaluative method as well as not allowing developers to apply their own biases. Further, it allows for a persona to work beyond the design stage of the development, and into the maintenance stages. Taking into account game-play telemetry, it allows for personas to be used as tools for lessons learned for future developments. © 2015 IEEE.
De Carvalho D.,Innopolis University |
Tortora De Falco L.,Third University of Rome
Information and Computation | Year: 2016
We prove that given two cut-free nets of linear logic, by means of their relational interpretations one can determine: 1) whether or not the net obtained by cutting the two nets is strongly normalizable, 2) (in case it is strongly normalizable) the maximum length of the reduction sequences starting from that net. As a by-product of our semantic approach, we obtain a new proof of the conservation theorem for Multiplicative Exponential Linear Logic (MELL) which does not rely on confluence; this yields an alternative proof of strong normalization for MELL. © 2016 Elsevier Inc. All rights reserved.
Maeen S.,National Research University Higher School of Economics |
Zykov S.,Innopolis University
Procedia Computer Science | Year: 2015
This paper explains how people responding to our survey, which included users' basic information, social status, experience with social networking and attitude towards social network-integrated e-health information systems. The survey findings show that social media users need special recommendation and guidance services-especially those people located in urban centers that have busy schedules. These people prefer to receive recommendations for their minor health problems over having to go to the hospital or clinic and spend time waiting, perhaps even to return home without a proper consultation from a doctor. As a result, we propose to work on architecture for integrated social media analytics and e-health information systems. However, our findings, being the result of a controlled survey, raise issues such as respondent trust and security and privacy issues relating to healthcare. © 2015 Published by Elsevier B.V.
Naumchev A.,Innopolis University |
Meyer B.,Polytechnic of Milan
Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016 | Year: 2016
Existing techniques of Design by Contract do not allow software developers to specify complete contracts in many cases. Incomplete contracts leave room for malicious implementations. This article complements Design by Contract with a simple yet powerful technique that removes the problem without adding syntactical mechanisms. The proposed technique makes it possible not only to derive complete contracts, but also to rigorously check and improve completeness of existing contracts without instrumenting them. © 2016 IEEE.