![(please configure the [header_logo] section in trac.ini)](http://traclifo.univ-orleans.fr/INEX/chrome/site/lifo.png)
Changes between Version 11 and Version 12 of JINO-2
- Timestamp:
- Jan 9, 2013, 3:43:54 PM (5 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
JINO-2
v11 v12 13 13 * 10h30-10h45 '''Accueil et introduction''' / '''Welcome''' 14 14 15 * 10h45-11h30 Nicolas Dugué (LIFO, Université d'Orléans), Anthony Perez (LIFO, Université d'Orléans) '''Detecting social capitalists on Twitter using similarity measures'''[[BR]]Social networks such as Twitter or Facebook are part of the phenomenon called Big Data, a term used to describe very large and complex data sets. To represent these networks, the connections between users can be easily represented using (directed) graphs. In this presentation, we are mainly focused on two different aspects of social network analysis. First, our goal is to find an efficient and high-level way to store and process a social network graph, using reasonable computing resources (processor and memory). We believe that this is an important research interest, since it provides a more democratic method to deal with large graphs. Next, we turn our attention to the study of social capitalists, a specific kind of users on Twitter. Roughly speaking, such users try to gain visibility by following other users regardless of their contents. Using two similarity measures called overlap index and ratio, we show that such users may be detected and classified very efficiently. 15 === Verification === 16 16 17 * 10h45-11h30 Yohan Boichut (LIFO), '''Equational Abstraction Refinement for Certified Tree Regular Model Checking'''[[BR]]In !MapReduce applications, a large part of the software stack is written in Java and run by JVMs. Tree Regular Model Checking (TRMC) is the name of a family of techniques for analyzing infinite-state systems in which states are represented by trees and sets of states by tree automata. They are well suited to verify properties of Java programs and thus !MapReduce applications. The central problem is to decide whether a set of bad states belongs to the set of reachable states. An obstacle is that this set is in general neither regular nor computable in finite time. This paper proposes a new Counter Example Guided Abstraction Refinement (CEGAR) algorithm for TRMC. Our approach relies on a new equational-abstraction based completion algorithm to compute a regular overapproximation of the set of reachable states in finite time. This set is represented by R/E-automata, a new extended tree automaton formalism whose structure can be exploited to detect and remove false positives in an efficient manner. Our approach has been implemented in TimbukCEGAR, a new toolset that is capable of analyzing Java programs by exploiting an elegant translation from the Java byte code to term rewriting systems. Experiments show that TimbukCEGAR outperforms existing CEGAR-based completion algorithms. Contrary to existing TRMC toolsets, the answers provided by TimbukCEGAR are certified by Coq, which means that they are formally proved correct.[[BR]]This is a joint work with Benoit Boyer, Thomas Genet and Axel Legay. 17 18 18 * 11h30-12h15 Raphaël Fournier-S'niehotta (LIP6, Paris) '''Detection and analysis of pedophile activity in P2P networks'''19 * 11h30-12h15 Matthieu Lemerre (CEA LIST), Nikolai Kosmatov (CEA LIST), and Céline Alec (CEA LIST), '''Verified Secure Kernels and Hypervisors for the Cloud'''[[BR]]Cloud-computing systems share hardware resources (CPU time and memory) between mutually untrusted applications. As such, they must provide isolation barriers between these applications, but must also secure resource sharing such that applications cannot stop, slow down, or provoke incorrect resource accounting of other applications. These isolation barriers are implemented by a trusted operating system kernel, which must be built according to security principles. Confidence in the system can be further increased with the help of tools for formal verification and proof of programs. Using these tools is eased because thorough application of security principles leads to a small system, but still poses many challenges for formal verification, like concurrency and the need to model the behavior of the hardware. This paper shows how modern tools for proof of programs can be applied to verification of secure kernels and hypervisors for the Cloud. We illustrate this approach on a critical module of a prototype Cloud hypervisor, called Anaxagoros, using the Frama-C software verification platform. 19 20 20 21 * 12h15-14h00 '''Déjeuner''' / '''Lunch''' 21 22 22 * 14h00-15h00 Zhenjiang Hu (National Institute for Informatics, Tokyo, Japan), '''A GTA Library for Systematic Parallel Programming with !MapReduce'''[[BR]]!MapReduce, being inspired by the map and reduce primitives available in many functional languages, is the de facto standard for large scale data-intensive parallel programming. Although it has succeeded in popularizing the use of the two primitives for hiding the details of parallel computation, little effort has been made to emphasize the programming methodology behind, which has been intensively studied in the functional programming and program calculation fields. In this talk, I'd show that !MapReduce can be equipped with a programming theory in calculational form. By integrating the generate-and-test programing (GTA) paradigm and semirings for aggregation of results, we propose a novel parallel programming framework for !MapReduce, and demonstrate how the framework can be efficiently implemented as a library to support parallel programming on Hadoop. This is a joint work with Kento Emoto, Sebastian Fischer, and Yu Liu. 23 === Programming Models and Environments === 23 24 24 * 15h00-15h45 Frédéric Loulergue (LIFO, Université d'Orléans), '''Towards a Verified GTA Library in Coq'''[[BR]]This is a joint work with Kento Emoto, Julien Tesson, and Frédéric Dabrowski. 25 * 14h00-15h00 Zhenjiang Hu (National Institute for Informatics, Tokyo, Japan), '''A GTA Library for Systematic Parallel Programming with !MapReduce'''[[BR]]!MapReduce, being inspired by the map and reduce primitives available in many functional languages, is the de facto standard for large scale data-intensive parallel programming. Although it has succeeded in popularizing the use of the two primitives for hiding the details of parallel computation, little effort has been made to emphasize the programming methodology behind, which has been intensively studied in the functional programming and program calculation fields. In this talk, I'd show that !MapReduce can be equipped with a programming theory in calculational form. By integrating the generate-and-test programing (GTA) paradigm and semirings for aggregation of results, we propose a novel parallel programming framework for !MapReduce, and demonstrate how the framework can be efficiently implemented as a library to support parallel programming on Hadoop.[[BR]]This is a joint work with Kento Emoto, Sebastian Fischer, and Yu Liu. 26 27 * 15h00-15h45 Frédéric Loulergue (LIFO, Université d'Orléans), '''Towards a Verified GTA Library in Coq'''[[BR]]The goal of this work is threefold. First we aim at modelling the algebraic structures used in the GTA framework and prove the lemma used to calculate programs from their GTA from inside the Coq proof assistant. Second we aim at providing some automation inside Coq to ease the definition of applications, with the formal verification that they actually fullfill the requirements of the GTA framework. Third we aim at providing the way to extract automatically actual parallel functional programs and MapReduce programs from these Coq developments. This talk will present the current status of this work-in-progress.[[BR]]This is a joint work with Kento Emoto, Julien Tesson, and Frédéric Dabrowski. 25 28 26 29 * 15h45-16h15 '''Pause''' / '''Coffee Break''' 27 30 28 * 16h15-17h00 Matthieu Lemerre (CEA LIST), Nikolai Kosmatov (CEA LIST), and Céline Alec (CEA LIST), '''Verified Secure Kernels and Hypervisors for the Cloud'''[[BR]]Cloud-computing systems share hardware resources (CPU time and memory) between mutually untrusted applications. As such, they must provide isolation barriers between these applications, but must also secure resource sharing such that applications cannot stop, slow down, or provoke incorrect resource accounting of other applications. These isolation barriers are implemented by a trusted operating system kernel, which must be built according to security principles. Confidence in the system can be further increased with the help of tools for formal verification and proof of programs. Using these tools is eased because thorough application of security principles leads to a small system, but still poses many challenges for formal verification, like concurrency and the need to model the behavior of the hardware. This paper shows how modern tools for proof of programs can be applied to verification of secure kernels and hypervisors for the Cloud. We illustrate this approach on a critical module of a prototype Cloud hypervisor, called Anaxagoros, using the Frama-C software verification platform. 31 === Data Analysis of Cloud and P2P Applications === 29 32 30 * 17h00-17h45 33 * 16h15-17h00 Raphaël Fournier-S'niehotta (LIP6, Paris) '''Detection and analysis of pedophile activity in P2P networks''' 34 35 * 17h00-17h45 Nicolas Dugué (LIFO, Université d'Orléans), Anthony Perez (LIFO, Université d'Orléans) '''Detecting social capitalists on Twitter using similarity measures'''[[BR]]Social networks such as Twitter or Facebook are part of the phenomenon called Big Data, a term used to describe very large and complex data sets. To represent these networks, the connections between users can be easily represented using (directed) graphs. In this presentation, we are mainly focused on two different aspects of social network analysis. First, our goal is to find an efficient and high-level way to store and process a social network graph, using reasonable computing resources (processor and memory). We believe that this is an important research interest, since it provides a more democratic method to deal with large graphs. Next, we turn our attention to the study of social capitalists, a specific kind of users on Twitter. Roughly speaking, such users try to gain visibility by following other users regardless of their contents. Using two similarity measures called overlap index and ratio, we show that such users may be detected and classified very efficiently. 31 36 32 37 * 17h45-18h00 '''Conclusion''' … … 34 39 == Organisateurs == 35 40 36 * Frédéric Loulergue 37 * Nicolas Dugué 41 * Frédéric Loulergue (LIFO) 42 * Nicolas Dugué (LIFO)
