Rachid Rebiha

Pós-doutorado

Formação complementar

Idiomas

Organização de eventos

Produções bibliográficas

• 2013 REBIHA, RACHID ; MATRINGE, N. ; MOURA, A. V. . Generating Asymptotically Non-terminant Initial Variable Values for Linear Diagonalizable Programs. Easychair Proceedings in Computing , v. 15, p. 81-92, 2013.

• 2012 REBIHA, RACHID ; MOURA, A. V. . Métodos Formais Algebricos para Geração de Invariantes. XXX Congresso da Sociedade Brasileira de Computação , v. 32, p. 36-42, 2012.

• 2010 Rachid Rebiha ; MATRINGE, N. ; MOURA, A. V. . Generating invariants for non-linear hybrid systems by linear algebraic methods. Lecture Notes in Computer Science , v. 6337, p. 373-389, 2010.

• REBIHA, RACHID ; MOURA, A. V. . Semantic Malware Resistance Using Inductive Invariants. The International Journal of Forensic Computer Science (Impresso) , p. 38-48, 2010.

• 2009 Rachid Rebiha ; MATRINGE, N. ; MOURA, A. V. . Morphisms for non-trivial non-linear invariant generation for algebraic hybrid systems. Lecture Notes in Computer Science , v. 5469, p. 445, 2009.

• 2009 REBIHA, RACHID ; MOURA, A. V. . Automated Malware Invariant Generation. Proceeding of the International Conference of Forensic Computer Science , v. 4, p. 7-14, 2009.

• 2008 Rachid Rebiha ; MOURA, A. V. ; MATRINGE, N. . Endomorphisms for non-trivial non-linear loop invariant generation. Lecture Notes in Computer Science , v. 5160, p. 425-439, 2008.

• REBIHA, RACHID ; MATRINGE, N. ; MOURA, A. V. . Generating Asymptotically Non-terminant Initial Variable Values for Linear Diagonalizable Programs. In: SCSS 2013. 5th International Symposium on Symbolic Computation in Software Science, 2013, Linz - Castel of Hagenberg. EPiC Series - Symbolic Computation in Software Science, 2013. v. 15. p. 81-95.

• REBIHA, RACHID ; MOURA, A. V. . Algebraic Formal Methods for Generation of Invariants,. In: CTD 2012 - XXV Concurso de Teses e Dissertações - XXXII Congresso da Sociedade Brasileira de Computação, 2012, Curitiba. CTD - CSBC 2012, 2012.

• REBIHA, RACHID ; MATRINGE, NADIR ; MOURA, ARNALDO VIEIRA . Transcendental inductive invariants generation for non-linear differential and hybrid systems. In: the 15th ACM international conference, 2012, Beijing. Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control - HSCC '12. New York: ACM Press. p. 25.

• REBIHA, RACHID ; MATRINGE, N. ; MOURA, A. V. . Generating invariants for non-linear hybrid systems by linear algebraic methods. In: 17th International Symosium on Static Analysis, 2010, Perpignan, France. Static Analysis. NewYork: Springer, 2010. v. 6337. p. 373-389.

• Rachid Rebiha ; MOURA, A. V. ; MATRINGE, N. . Morphisms for analysis of hybrid systems. In: ACM/IEEE Cyber- Physical Systems CPSWeek'09, Second International Workshop on Numerical Software Veri cation.(NSV2009) Veri cation of Cyber-Physical Software Systems, 2009, San Francisco, California. Numerical Software Veri cation, 2009. p. 135-150.

• Rachid Rebiha ; MOURA, A. V. ; MATRINGE, N. . Morphisms for non-trivial non-linear invariant generation for algebraic hybrid systems. In: 12th International Conference Hybrid Systems: Computation and Control, 2009, San Francisco, California. Hybrid Systems: Computation and Control. NewYork: Springer, 2009. v. 5469.

• REBIHA, RACHID ; MOURA, ARNALDO . Automated Malware Invariant Generation. In: The Fourth International Conference on Forensic Computer Science, 2009. Proceedings of The Fourth International Conference on Forensic Computer Science. v. 4. p. 7.

• Rachid Rebiha ; MOURA, A. V. ; MATRINGE, N. . Endomorphisms for non-trivial non-linear loop invariant generation. In: Fifth International Conf. Theoretical Aspect of Computing, 2008, Istanbul. ICTAC. NewYork: Springer, 2008. v. 5160. p. 425-439.

• REBIHA, R.ACHID ; CIAMPAGLIA, GIOVANNI L. . An Ant Colony Verification Algorithm. In: Seventh International Conference on Intelligent Systems Design and Applications (ISDA 2007), 2007, Rio de Janeiro. Seventh International Conference on Intelligent Systems Design and Applications (ISDA 2007). p. 901.

• Rachid Rebiha . Termination Program Proof and the Brouwer's fixed point theorem. 2013. (Apresentação de Trabalho/Seminário).

• Rachid Rebiha . Transcendental Inductive Invariants Generation for Non-linear Differential and Hybrid Systems.. 2012. (Apresentação de Trabalho/Conferência ou palestra).

• Rachid Rebiha . Algebraic Formal Methods for Generation of Invariants. 2012. (Apresentação de Trabalho/Conferência ou palestra).

• Rachid Rebiha . 'Métodos Formais Algebricos para Geração de Invariantes' Phd Defense. 2011. (Apresentação de Trabalho/Outra).

• Rachid Rebiha . 'Algebraic Formal Methods for Invariant Generation'. Phd Dissertation Defense, University of Lugano, Switzerland. 2011. (Apresentação de Trabalho/Outra).

• Rachid Rebiha . ``Generating Invariants for Non-linear Hybrid Systems by Linear Algebraic Methods''. 2010. (Apresentação de Trabalho/Conferência ou palestra).

• Rachid Rebiha . ``Morphisms for Analysis of Hybrid Systems''.. 2009. (Apresentação de Trabalho/Conferência ou palestra).

• Rachid Rebiha . ``Morphisms for Non-trivial Non-linear Invariant Generation for Algebraic Hybrid Systems''. 2009. (Apresentação de Trabalho/Conferência ou palestra).

• Rachid Rebiha . 'Automated Malware Invariant Generation'. 2009. (Apresentação de Trabalho/Conferência ou palestra).

• Rachid Rebiha . 'Endomorphisms for non-trivial non-linear loop invariant generation'. 2008. (Apresentação de Trabalho/Conferência ou palestra).

• Rachid Rebiha . 'Algebraic Formal Methods I : Invariant Generation for Program Verification and Security'. 2008. (Apresentação de Trabalho/Seminário).

• Rachid Rebiha . 'Invariant Generation for Host-Based Intrusion Detection'. USI Faculty of Informatics, University of Lugano, Switzerland, 2007.. 2007. (Apresentação de Trabalho/Seminário).

• Rachid Rebiha . 'Quasi-Static Binary analysis: Guarded Model for Host-Based Intrusion Detection'. 2007. (Apresentação de Trabalho/Seminário).

• Rachid Rebiha . 'Program and Memory Heap Verification by Infinite Model Checking: Segmentation Fault and Memory Leak Checking with Recursive Data Structures'. 2007. (Apresentação de Trabalho/Seminário).

• Rachid Rebiha . 'An Extensible LTL Model Checking Library and Transition-based Generalized Buchi Automata'. 2007. (Apresentação de Trabalho/Seminário).

• Rachid Rebiha . 'Automatic Memory Heap Verification'. 2007. (Apresentação de Trabalho/Seminário).

• Rachid Rebiha . 'Formal Verification with CTL* and (Propositional-) Fixed point Theory'. 2006. (Apresentação de Trabalho/Seminário).

• Rachid Rebiha . 'Model Checking, Verification and Analysis of Memory Heap and Programs with Recursive Data Structures'. 2004. (Apresentação de Trabalho/Seminário).

• Rachid Rebiha . 'Infinit Model Checking and Verification of Memory Heap and Programs with Recursive Data Structures'. 2004. (Apresentação de Trabalho/Seminário).

• Rachid Rebiha . 'An Extensible LTL Model Checking Library and Transition-based Generalized Buchi Automata'. 2003. (Apresentação de Trabalho/Seminário).

• Rachid Rebiha . 'LTL Model Checking Library and Transition-based Generalized Buchi Automata'. 2003. (Apresentação de Trabalho/Outra).

Outras produções

Projetos de pesquisa

• 2013 - Atual

  M etodos Formais Alg ebricos para Veri fica ção de Programas, Descrição: Esta projeto FAPESP-BEPE visa, primordialmente, investigar a redu ção de problemas de an alise est atica de programas (i.e., gera ção de invariantes, an alise automatizada de termina ção de programas, etc) para problemas da Alg ebra Lineare. Na linha de novos m etodos te oricos para an alise est atica de sistemas complexos, nossas investiga ções se voltarão para o desenvolvimento de algor itmos associados efi cazes. Poder amos fundamentar t ecnicas ineditas e e ficientes que venham a formar o n ucleo de novos algor tmos para a automa ção de processos dedutivos, e de novos algor itmos para veri fica ção de modelos complexos, de propriedades de seguran ca e de vivacidade (i.e termina ção). Ter amos que desenvolver os m etodos computacionais capazes de automatizar a descoberta das rela ções entre as vari aveis de um programa, o qual pode conter la cos, chamadas de sistema e de fun ções. A generaliza ção dos resultados te oricos hoje em uso em t ecnicas de prova autom atica de termina ção, e o desenvolvimento de m etodos computationais e ficazes para an alise est atica de termina ção de programas, determina um dos desafi os e objetivos principais do nosso projeto. Continuando nossas pesquisas atuais, vamos abordar conjecturas bem conhecidas, sobre an alise de termina ção de programas em um n ivel te orico e pr atico. Investiga ções iniciais nesse sentido j a se mostraram bastante promissoras e j a somos capazes de lidar com sistemas complexos que vão al em dos limites alcan cados hoje por outros m etodos. Propomo-nos investigar e desenvolver m etodos pioneiros, usando condi ções necess arias e su cientes de alg ebra linear, que provam termina ção, gerem bases de invariantes e exibem novas representa ções simb olicas para an alise de acessibilidade (estados alcan c aveis). Logrando este intuito, poder amos ultrapassar as de ci^encias dos mais modernos m etodos de veri ca c~ao de programas hoje conhecidos, permitindo, tambem, a gera c~ao e ciente de invariantes para sistemas h bridos e embarcados. Os algoritmos alg ebricos que temos em vista apresentam complexidades signi cativamente inferiores aqueles que suportam as demais abordagens usadas hoje.. , Situação: Em andamento; Natureza: Pesquisa. , Integrantes: Rachid Rebiha - Integrante / Arnaldo Vieira Moura - Coordenador / Nadir Matringe - Integrante., Financiador(es): Fundação de Amparo à Pesquisa do Estado de São Paulo - Bolsa.

• 2011 - Atual

  M etodos Formais Alg ebricos para Gera ção de Invariantes, Verificação e Segurança, Descrição: Este P os-doutorado com a FAPESP no Instituto de Computação visa, primordialmente, investigar a redu ção de problemas de an alise est atica de programas (i.e. gera ção de invariantes, an alise automatizada de termina ção de programas, etc) para problemas de Algebra Linear. Na linha de novos m etodos est aticos para an alise est atica de sistemas complexos, nossas investiga cões se voltarão para o desenvolvimento de algoritmos associados e ficazes. Pretendemos fundamentar t ecnicas in editas e e ficientes que venham a formar o n ucleo de novos algoritmos para automa ção de processos dedutivos, e de novos algoritmos para veri fica ção de modelos complexos, para verifi ca ção de propriedades de seguran ça e de propriedades de vivacidade. Poderemos desenvolver m etodos computacionais capazes de automatizar a descoberta de rela ções entre as vari aveis de um programa, o qual pode conter la cos, chamadas de sistemas e de fun ções. A generaliza ção dos resultados te oricos hoje em uso em t ecnicas de prova autom atica de terminação, e o desenvolvimento de m etodos computacionais e ficientes para an alise est atica de termina ção de programas, determinam um dos desafios e objetivos principais do nosso projeto. Sob outro ponto de vista, pretendemos ampliar o dom nio de aplica ções da gera ção de invariantes para a area de seguran ca.. , Situação: Em andamento; Natureza: Pesquisa. , Integrantes: Rachid Rebiha - Integrante / Arnaldo Vieira Moura - Coordenador., Financiador(es): Fundação de Amparo à Pesquisa do Estado de São Paulo - Bolsa.

• 2007 - 2011

  M étodos Formais Alg ébricos para Gera ção de Invariantes, Descrição: É bem sabido que a automação e a eficácia de métodos de verificação formal de softwares, sistemas embarcados ou sistemas híbridos, depende da facilidade com que invariantes precisas possam ser geradas automaticamente a partir do código fonte. Uma invariante é uma propriedade, especificada sobre um local específico do código fonte, e que sempre se verifica a cada execução de um sistema. Apesar dos progressos enormes ao longo dos anos, o problema da geração de invariantes ainda está em aberto para tanto programas não-lineares discretos, como para sistemas não-lineares híbridos. Apresentamos novos métodos computacionais que podem automatizar a descoberta e o fortalecimento de relações não-lineares entre as variáveis de um programa que contém laços não-lineares, ou seja, programas que exibem relações polinomiais multivariadas e manipulações fracionárias. Além disso, a maioria dos sistemas de segurança críticos, tais como aviões, automóveis, produtos químicos, usinas de energia e sistemas biológicos, operam semanticamente como sistemas híbridos não-lineares. Nesse trabalho, apresentamos poderosos métodos computacionais que são capazes de gerar bases de ideais polinomiais de invariantes não-lineares para sistemas híbridos não-lineares. Em segundo lugar, apresentamos métodos pioneiros de verificação que automaticamente gerem bases de invariantes expressas por séries de potências multi-variáveis e por funções transcendentais. Verificamos que as séries de potência geradas para invariantes são, muitas vezes, compostas pela expansão de algumas funções transcendentais bem conhecidas, tais como ``log'' e ``exp''. Assim, apresentam uma forma analisável fechada que facilita o uso de invariantes na verificação de propriedades de segurança. Para cada problema de geração de invariantes estabelecemos condições suficientes, muito gerais, que garantem a existência e permitem o cálculo dos ideais invariantes polinomiais para situações que não podem ser tratadas pelas abordagens de geração de invariantes hoje conhecidas. Ao reduzir os problemas de geração de invariante somos capazes de ultrapassar as deficiências dos mais modernos métodos de geração de invariante hoje. Tais métodos algébricos lineares apresentam complexidades computacionais significativamente inferiores àquelas exigidas pelos os fundamentos matemáticos das abordagens usadas hoje. Finalmente, estendemos o domínio de aplicações, acessíveis através de métodos de geração de invariantes, para a área de segurança. Mais precisamente, fornecemos uma plataforma extensível baseada em invariantes pré-computadas que seriam usadas como assinaturas semânticas para análise de intrusos (``malwares'') e deteção dos ataques de intrusões mais virulentos. Nós fornecemos uma poderosa base teórica para a concepção de plataformas estáticas e dinâmicas que podem apresentar uma arquitetura adequada para análise de malware em profundidade automática. Nós mostramos como métodos formais envolvendo análise estáticos e dinâmica de programas pode ser usado para construir essas arquiteturas. Propomos uma nova abordagem para a detecção e identificação de malware, gerando automaticamente invariantes diretamente a partir do código de malware específico. Tais invariantes que chamamos de malware-invariantes, pode, então, ser usado como assinaturas da semânticas do comportamente do malware contornando dificuldades atendidas por outras abordagens recentes para detecção e clasificação de malware. Mais importante, estes invariantes permaneceriam inalterados na maioria das versões ofuscados do código. Seguindo a concepção de tais plataformas, propomos sistemas de detecção de intrusão, usando modelos gerados automaticamente, onde as chamadas de sistema e de funções são vigiados pela avaliação de invariantes, pré-calculadas para denunciar qualquer desvio observado durante a execução da aplicação.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Doutorado: (1) . , Integrantes: Rachid Rebiha - Integrante / Arnaldo Vieira Moura - Coordenador., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa.

• 2006 - 2007

  Static Analysis for Malware and Intrusion Detection, Descrição: International Fellow Researcher at Stanford Research Institute , California US National project, Laboratório de Segurança e Laboratório de Ciencia da Computação. A visita ao SRI e o trabalho lá desenvolvido, em parte, colaboraram para criar o recente "Malware Thread Center", localizado no mesmo SRI. Eu propus sistemas de deteção de intrusões baseado em "Host" por meio de modelos gerados automaticamente, desde que as chamadas ao sistema operacional sejam autorizadas pela validação de invariantes pré-computadas. Desta forma, poderemos detectar quaisquer desvios observados durante a execução da aplicação. Mais precisamente, fornecemos um modelo baseada em invariantes pré-computadas que seriam usadas como assinaturas semânticas para análise de intrusos e deteção dos ataques de intrusões mais virulentos. Nosso sistema de deteção de intrusão tem um grau muito elevado de automação, fornece uma protecção contra uma ampla classe de ataques ("mimicry attacks", "non-control-data flow attacks", ... ) anteriormente indetectáveis automaticamente. O nosso método é muito mais seguro, enquanto que a sobrecarga é reduzida drasticamente em comparação com modelos do estado da arte (Dyck Model, ...). Além disso, nossos métodos não da alarme falso, porque se um invariante é violado nós temos uma prova matemática de um comportamento anormal emitido por uma intrusão. Em muitos casos, o nosso modelo é preciso o suficiente para que seja possível verificar automaticamente a presença de erros de lógica de aplicação e de vulnerabilidades. Esta característica está ausente em qualquer outra abordagem de detecção de intrusão.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Doutorado: (1) . , Integrantes: Rachid Rebiha - Coordenador / Hassan Saidi - Integrante / Steve Dowson - Integrante.

• 2005 - 2006

  Formal Methods for Program Verification and Security Using Predicate Abstraction, Descrição: Propusemos novos métodos formais baseados em técnicas de captação de predicados, a fim de associar algoritmo que permite a verificação automática de software de grande porte. Para cada tipo de propoerties identificamos a lógica do direito de considerar e de notícias Associated métodos computacionais para o problema resultou. Estamos focados na análise estática e verificação automática da grande programa escrito em C e C + +. Também ampliamos nossas abordagens para a validação e verificação automática de software baseada em componentes.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Doutorado: (1) . , Integrantes: Rachid Rebiha - Integrante / Fernando Pedone - Coordenador / Natasha Sharigyna - Integrante.

• 2005 - 2006

  Automated Verification and Model Checking of Large Programs Using SAT-Based Decision Procedures, Descrição: Propusemos técnicas de verificação de propriedade sobre modelos, a fim de lidar com a análise estática e verificaiton de propriedade ("safety") of largas programas escrito em C / C + +. Nossa abordagem é baseada em novas técnicas de refinamento de abstração automatizados para verificação do modelo ("Automated abstraction refinement for model checking3) . Em outras palavras, as propriedades a ser verificadas eo codigo fonte do programa são representados em termos de fórmulas booleanos. Neste processo de decisão os predicados envolvidos são obtidos utilizando technicas de Counterexample-guided abstraction refinement. Nós reduzimos o problema de verificação de propriedades sobre o código fonte C para problemas de decisão SAT, utilizando SAT solvers e SMT (SAT Modulo Teoria) ferramentas.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Doutorado: (4) . , Integrantes: Rachid Rebiha - Integrante / Natasha Sharigyna - Coordenador / Daniel Kroening - Integrante.

• 2003 - 2004

  Análise Estática e Verificação Automática de Software com Alocação de Memória Dinâmica e Estruturas de Dados Dinâmicas., Descrição: Eu era um pesquisador assistente no Departamento de Otimiza ção das Performances e Seguran ças dos Processos, na EDF Recherche et Developpement (Eletricidade e Energia Francesa; Ministerio Francesa da Pesquisa, Industria e Ministerio da Energia) em m etodos formais, veri fica ção e seguran ca dos sistemas criticos. Membro do Grupo de Pesquisa Otimiza ção e Seguran ca da Produ ção de Energia (OPP11). Fui selecionado para participar em um projet Nacional entre a EDF e o CEA (Centro de Energia At omica) para desenvolver metodologias efi cientes e novos para a verifi ca ção e an alise est atica do sistem. O primeiro objetivo foi aplicar tal estrutura para estudos de caso em programa criticos para a seguran c~a e a funcionalidade cr tica de alguns sistemas para EDF. Eu era o l der do projeto para este ano e forneceulhes solu c~oes te orica e tecnol ogicas. Al em disso, eu os levou a colaborar com os laborat orios apropriados, de modo a aprofundar estas pesquisas. Este trabalho foi ben e co e algumas das escolhas que fiz sendo fundamental para o sistema de veri fica ção usados pela EDF - Pesquisa & Desenvolvimento. Palavras chaves: Metodos Formais, Verificaçao automatica de Programas, Model Checking, Theorem Proving, Tests Generations, Static and Dynamic Analysis.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Rachid Rebiha - Coordenador / Alain Ourganlian - Integrante / David Novak - Integrante / Alain Finkel - Integrante., Financiador(es): EDF Electricite et Energie de France Recherche et Developpement - Outra.

• 2003 - 2004

  Formal Methods for Program with Dynamic Data Structures and Memory Heap Verification, Descrição: Propusemos novos métodos formais, a fim de ser capaz de lidar com a verificação automática de programas complexos usando estruturas de dados recusive e alocação de memória dinâmica. Por exemplo, nós fomos capazes de fornecer uma nova abordagem que permita a verificação estática automático (análise estática significa análise sem executar o código) de falha de segmentação, vazamento de memória (e outras propriedades de "safety", ...) sobre os programas que utilizam por examplo ponteiros, estruturas de dados recursivas, ... . Fomos capazes de reduzir o problema da verificação deste tipo de propriedade para o problema de acessibilidade em sistemas de contador. Nós desenvolvemos novas técnicas usando ferramentas de verificação do modelo infinito.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Doutorado: (1) . , Integrantes: Rachid Rebiha - Coordenador / Jean Michel Couvreur - Integrante / Alain Finke - Integrante / David Novack - Integrante., Financiador(es): Association Nationale de la Recherche et de la Technologie - Bolsa.

• 2002 - 2003

  LTL Model Checking Techniques for Distributed Systems using Transition-Based Buchi Automata, Descrição: Olhamos para o domínio das técnicas de verificação de modelos para sistemas distribuídos.Propusemos novos abordagens teóricos , novas técnicas , algoritmos e heurísticas para a verificação de automatica de model para propriedades espressadas em Logica Temporais Linear ( LTL) e implementou -los no Software resultando que chamamos "Spot" . Spot é uma grande biblioteca de verificação de modelo muito bem conceptualizada, orientado a objetos e escrito em C + + . Ele implementa nossas métodos e oferece um conjunto de blocos / módulos para compor vários de nossos algoritmos e construir um ferramento de verificação automatica de modelo considerando vários tipos de sistemas. Nesta abordagem , a verificação é dividido da seguinte forma: (1) o cálculo do espaço de estados , (2) a tradução da fórmula negada em um omega- autômato, (3 ) "on- the-fly" produtos sincronizados desses objetos ( considerando vários modelos e fórmulas) ," on- the-fly EmptinessCheck" dos produtos resultantes . Propusemos novos algoritmos diferentes para realizar os três últimos passos ( e mais ), mas eles podem também ser combinadas de forma diferente. Além disso, a primeira etapa pode ser efectuada por meio de ferramentas esterno. Desta forma, não impomos qualquer formalismo de alto nível. Assim, por exemplo , se você criou seu próprio formalismo de modelagem e ter um programa que é capaz de calcular o espaço de estados de um modelo , então você pode ligar o seu programa com o Spot ( InterfacingSpot ) a fim de verificar Ltl-Formula em seu modelo. A biblioteca usa um tipo especial de autômatos chamados Transition-based Generalized Büchi Automata ( TGBA ). Estes são "Omega-Automata" com etiquetas em transições, e vários conjuntos de aceitação de transições . Comparado a Automata de Büchi mais tradicional, TGBA permitir LtlFormulae a ser representado de forma mais concisa . Tudas as estruturas (estados, relação detransições, formulas, ...) sao implementados com Binary Decision Diagram (BDD), isso também garante o nivel de eficiência do Software. As técnicas heurísticas e comparações com outras ferramentas têm sido publicados recentemente , enquanto que a biblioteca resultante ainda é mantido , desenvolvido e utilizado, no LiP6 Laboratório de Informática de Paris VI , da Universidade de Paris 6 - Pierre et Marie Currie, Paris e no LRDE Laboratório de Pesquisa & Desenvolvimento EPITA (Escola de Engeneria de Informática e Avanços Tecnológicos de Paris).. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Mestrado acadêmico: (2) Doutorado: (2) . , Integrantes: Rachid Rebiha - Coordenador / Alexandre Duret-Lutz - Integrante / Denis Poitrennaud - Integrante / jean Michel Ilie - Integrante., Financiador(es): Laboratoire Informatiques de Paris 6 - Auxílio financeiro.

Prêmios