Changes between Version 12 and Version 13 of JINO-2

Timestamp:

Jan 9, 2013, 3:44:48 PM (5 years ago)

Author:

frederic.loulergue@…

Comment:

--

JINO-2

@@ -15 +15 @@
 === Verification ===
 
-* 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.
+* 10h45-11h30 Yohan Boichut (LIFO, Université d'Orléans), '''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.
 
 * 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. 
@@ -39 +39 @@
 == Organisateurs ==
 
-* Frédéric Loulergue (LIFO)
-* Nicolas Dugué (LIFO)
+* Frédéric Loulergue (LIFO, Université d'Orléans)
+* Nicolas Dugué (LIFO, Université d'Orléans)