Dec 2010
Algorithme Evolutionnaire à Etats pour la résolution
du problème des Fusiliers
15/12/10 18:02 |
Stages 2010/11
| Permalien
Laboratoire : I3S, Sophia Antipolis
Equipe : TEA
Contact : Philippe Collard (philippe point collard arobase unice point fr)
Co-encadrant : Sébastien Vérel
Contexte :
Objectifs :
Bibliographie
Equipe : TEA
Contact : Philippe Collard (philippe point collard arobase unice point fr)
Co-encadrant : Sébastien Vérel
Contexte :
La synchronisation d'une ligne d'automates,
problème connu sous le nom de problème des
fusiliers, a donné lieu à de nombreux travaux. Le
problème a été proposé par J. Myhill en 1957 comme
ceci : ''Comment synchroniser une ligne de
fusiliers de façon à ce qu'ils se mettent à tirer
ensemble, alors que l'ordre donne par un général
depuis l'un des deux bords de l'escadron met un
certain temps à se propager?''. Chaque fusilier est
représenté par une cellule d'un l'automate
cellulaire et peut se trouver dans différentes
états, les plus importants étant : l'état latent
(quiescent ou de repos), l'état de départ (général)
qui donne l'ordre et l'état de feu
(synchronisation). Le but du problème est de
trouver les fonctions de transition qui vont
permettre d'obtenir une configuration dans laquelle
toutes les cellules se trouvent ensemble et pour la
premi√®re fois dans l'état feu.
J. Mazoyer a trouvé une solution à ce problème lorsque le nombre d'états est 6. De très récents travaux encourageants ont tenté de résoudre le problème pour 5 états en l'exprimant comme un problème d'optimisation et en le résolvant à l'aide d'algorithmes d'optimisation stochatiques tels que le recuit simulé ou les algorithmes évolutionnaires.
J. Mazoyer a trouvé une solution à ce problème lorsque le nombre d'états est 6. De très récents travaux encourageants ont tenté de résoudre le problème pour 5 états en l'exprimant comme un problème d'optimisation et en le résolvant à l'aide d'algorithmes d'optimisation stochatiques tels que le recuit simulé ou les algorithmes évolutionnaires.
Objectifs :
Dans ce stage, il s'agira de résoudre le problème
d'optimisation induit par le problème des fusiliers
à 5 états à l'aide de l'algorithme évolutionnaire à
états (SEA). Le SEA est un algorithme adaptatif
hybride parallèle.
Le but de ce travail est de proposer et d'analyser un algorithme stochastique efficace de résolution du problème des fusiliers à 5 états. Il s'agira d'abord de développer un algorithme évolutionnaire hybride basé sur des algorithmes de recherche locale (recuit simulé, tabu search). Puis ensuite, de les combiner dans au sein de l'algorithme évolutionnaire à état qui permet un contrôle adaptatif parallèle des paramètres des précédentes algorithmes.
Le but de ce travail est de proposer et d'analyser un algorithme stochastique efficace de résolution du problème des fusiliers à 5 états. Il s'agira d'abord de développer un algorithme évolutionnaire hybride basé sur des algorithmes de recherche locale (recuit simulé, tabu search). Puis ensuite, de les combiner dans au sein de l'algorithme évolutionnaire à état qui permet un contrôle adaptatif parallèle des paramètres des précédentes algorithmes.
Bibliographie
- J.B.Yunès, Synchronisation et automates
cellulaires: la ligne de fusiliers, Thèse (1993)
- Exposé sur les algorithmes de résolution du problème des fusiliers à 5 états, FRAC 2007
- S. Verel, M. Clergue, P. Collard, States based Evolutionary Algorithm, PPSN, 2010.
- Exposé sur les algorithmes de résolution du problème des fusiliers à 5 états, FRAC 2007
- S. Verel, M. Clergue, P. Collard, States based Evolutionary Algorithm, PPSN, 2010.
Emergence de frontières dans un système complexe
15/12/10 14:55 |
Stages 2010/11
| Permalien
Laboratoire : I3S, Sophia Antipolis
Equipe : TEA
Contact : Philippe Collard (philippe point collard arobase unice point fr)
Co-encadrant : Sébastien Vérel
Contexte :
Sujet :
Bibliographie :
- Gauvin, L., Vannimenus, J., and Nadal, J., Phase diagram of a schelling segregation model, European Physical Journal B 70 (2009) 293-304.
- Pham, D., From Agent-Based Computational Economics towards Cognitive Economics, in Bourgine P., Nadal J.P eds : Cognitive Economics : An Interdisciplinary Approach (Springer verlag, 2004).
- Schelling, T. C., Micromotives and macrobehavior (WW Norton and Co, N.Y, 1978).
- Wilensky, U., Center for connected learning and computer-based modeling (1999), http://ccl.northwestern.edu/netlogo/.
Equipe : TEA
Contact : Philippe Collard (philippe point collard arobase unice point fr)
Co-encadrant : Sébastien Vérel
Contexte :
La notion d'entité autonome (i.e. ensemble
d'agents) est centrale dans les sciences des
systèmes complexes ; aussi pour reconnaître l'unité
de telles entités, il faut être capable de
distinguer entre un intérieur et un extérieur.
C'est la notion de frontière qui permet une telle
différenciation : son rôle est double, elle permet
à la fois de séparer et de favoriser les échanges.
Une frontière est le lieu de tous les contacts et interactions entre des agents opposés ; on peut observer des dimensions différentes selon que l'on considère la notion classique de frontière géographique ou la séparation qui émerge de relations sociales. Une frontière géographique apparaît comme un front, tandis que pour une frontière sociale la représentation sous la forme d'une «ligne» devient caduc et nous avons donc à réfléchir à des nouvelles formes.
Une frontière est le lieu de tous les contacts et interactions entre des agents opposés ; on peut observer des dimensions différentes selon que l'on considère la notion classique de frontière géographique ou la séparation qui émerge de relations sociales. Une frontière géographique apparaît comme un front, tandis que pour une frontière sociale la représentation sous la forme d'une «ligne» devient caduc et nous avons donc à réfléchir à des nouvelles formes.
Sujet :
Il s'agira de proposer un modèle spatial qui
permettra d'étudier via une simulation orientée
agents l'émergence de frontières dans une variété
de systèmes complexes ségrégationnistes.
On pourra s'inspirer du modèle de Schelling où coexiste des communautés d'agents, chacun pouvant se déplacer selon la présence ou l'absence d'agents d'un groupe opposé dans son voisinage.
L'objectif sera de simuler, observer et analyser ces frontières ; cela nécessitera la définition préalable de propriétés qui permettront de caractériser et comparer des frontiéres.
Dans un tel modèle générique, selon la tolérance/grégarisme, la densité d'agents et la topologie du réseau de voisinage, on peut espérer voir émerger une grande variété de frontières malgré le fait que certaines présentent certaines caractéristiques en commun.
On pourra s'inspirer du modèle de Schelling où coexiste des communautés d'agents, chacun pouvant se déplacer selon la présence ou l'absence d'agents d'un groupe opposé dans son voisinage.
L'objectif sera de simuler, observer et analyser ces frontières ; cela nécessitera la définition préalable de propriétés qui permettront de caractériser et comparer des frontiéres.
Dans un tel modèle générique, selon la tolérance/grégarisme, la densité d'agents et la topologie du réseau de voisinage, on peut espérer voir émerger une grande variété de frontières malgré le fait que certaines présentent certaines caractéristiques en commun.
Bibliographie :
- Gauvin, L., Vannimenus, J., and Nadal, J., Phase diagram of a schelling segregation model, European Physical Journal B 70 (2009) 293-304.
- Pham, D., From Agent-Based Computational Economics towards Cognitive Economics, in Bourgine P., Nadal J.P eds : Cognitive Economics : An Interdisciplinary Approach (Springer verlag, 2004).
- Schelling, T. C., Micromotives and macrobehavior (WW Norton and Co, N.Y, 1978).
- Wilensky, U., Center for connected learning and computer-based modeling (1999), http://ccl.northwestern.edu/netlogo/.
Réductions de graphes de régulation préservant les
comportements
15/12/10 14:17 |
Stages 2010/11
| Permalien
Laboratoire : I3S, Sophia Antipolis
Equipe : BIOINFO
Contact : Gilles Bernot (gilles point bernot arobase unice point fr)
Co-encadrants : Jean-Paul Comet et Adrien Richard
Contexte scientifique :
Objectif du stage :
Références
[1] G. Bernot, J-P. Comet, A. Richard, J. Guespin. Application of formal methods to biological regulatory networks: Extending Thomas' asynchronous logical approach with temporal logic, J. of Theoretical Biology (JTB), Vol.229, Issue 3, p.339-347, 2004.
[2] G. Bernot, F. Tahi. Behaviour preservation of a biological regulatory network when embedded into a larger network, Fundamenta informaticae, IOS Press, Amsterdam, 91(3-4):463--485, 2009.
[3] A. Naldi, E. Remy, D. Thiery, C. Chaouiya. A Reduction of Logical Regulatory Graphs Preserving Essential Dynamical Properties, CMSB 2009, p.266-280, 2009.
http://dx.doi.org/10.1007/978-3-642-03845-7_18
Equipe : BIOINFO
Contact : Gilles Bernot (gilles point bernot arobase unice point fr)
Co-encadrants : Jean-Paul Comet et Adrien Richard
Contexte scientifique :
L'étude des réseaux génétiques passe maintenant par
l'étude de leur dynamiques. Malheureusement, les
paramètres cinétiques ne sont pas souvent connus,
ce qui rend la simulation de ces systèmes
difficiles. Lorsqu'on se place dans le cadre de la
modélisation discrète de R. Thomas, l'ensemble des
paramètrages devient fini, et on peut envisager
l'énumération de tous les modèles [1].
Malheureusement, cette énumération est trop lourde.
Il devient alors nécessaire de s'intéresser à des
abstractions de sous-systèmes [2], dans le but de
limiter la combinatoire des comportements possibles
au niveau du réseau global. Dans ce cadre, nous
nous proposons d'étudier le pliage de graphe pour
faire de la réification dans le cadre de la
modélisation de R. Thomas.
Objectif du stage :
L'idée de départ consiste à «supprimer»
un nœud du graphe d'interactions lorsque ce n\oe ud
ne joue le rôle que d'un relai. On remplace alors
la flèche entrante régulant ce nœud par l'ensemble
des flèches partant du même régulateur vers chacune
des cibles du n\oe ud considéré, étiquetées par le
signe approprié. Ce processus peut être itéré le
long de chacun des chemins dits «fonctionnels».
La formalisation de ce processus sera faite avec
rigueur afin de pouvoir étudier les propriétés
dynamiques préservées. En particulier, on se
focalisera sur la conservation des états stables et
des attracteurs. Plus généralement, nous étudions
les relations entre la configuration d'attracteurs
du modèle d'origine et celle du modèle réduit,
ainsi que la question de l'atteignabilité des
attracteurs [3].
Références
[1] G. Bernot, J-P. Comet, A. Richard, J. Guespin. Application of formal methods to biological regulatory networks: Extending Thomas' asynchronous logical approach with temporal logic, J. of Theoretical Biology (JTB), Vol.229, Issue 3, p.339-347, 2004.
[2] G. Bernot, F. Tahi. Behaviour preservation of a biological regulatory network when embedded into a larger network, Fundamenta informaticae, IOS Press, Amsterdam, 91(3-4):463--485, 2009.
[3] A. Naldi, E. Remy, D. Thiery, C. Chaouiya. A Reduction of Logical Regulatory Graphs Preserving Essential Dynamical Properties, CMSB 2009, p.266-280, 2009.
http://dx.doi.org/10.1007/978-3-642-03845-7_18
L’aléatoire déterministe par des automates
cellulaires, liens avec les fonctions Booléennes
14/12/10 10:51 |
Stages 2010/11
| Permalien
Laboratoire : I3S, Sophia Antipolis
Equipe : MC3
Contact : Bruno Martin (bruno point martin arobase unice point fr)
Contexte
Compétences souhaitées
Références
[1] A.M. Apohan and C.K. Koc. Inversion of cellular automata iterations. In Computer and Digital Techniques,
volume 144, pages 279–284, 1997.
[2] A. Braeken, Y. Borissov, S. Nikova, and B. Preneel. Classification of boolean functions of 6 variables or less with
respect to cryptographic properties. Technical report, IACR248, 2008.
[3] P. Lacharme, B. Martin, and P. Sol´e. Pseudo-random sequences, boolean functions and cellular automata. In
Proceedings of Boolean Functions and Cryptographic Applications, 2008. A paraˆıtre.
[4] B. Martin. A Walsh exploration of elementary CA rules. Journal of Cellular Automata, 3(2) :145–156, 2008.
[5] W. Meier and O. Staffelbach. Analysis of pseudo random sequences generated by cellular automata. In EUROCRYPT
’91, Lecture Notes in Computer Science, pages 186–200. Springer Verlag, 1991.
[6] S.Wolfram. Cryptography with cellular automata. In CRYPTO 85, volume 218 of LNCS, pages 429–432. Springer
Verlag, 1985.
Equipe : MC3
Contact : Bruno Martin (bruno point martin arobase unice point fr)
Contexte
Les automates cellulaires (AC) constituent à la
fois un modèle de système dynamique discret et
un modèle de calcul. Un AC est composé d’un
ensemble infini de cellules identiques qui peuvent
prendre à un instant donné un état à valeurs
dans un ensemble fini. Le temps est également
discret et l’état d’une cellule au temps t est
fonction de l’état au temps t − 1 d’un nombre fini
de cellules, son «voisinage». À
chaque instant, la même règle est appliquée à
l’ensemble des cellules, produisant une nouvelle
«configuration» dépendant entièrement de la
configuration précédente. Nous considérons ici des
AC sur un anneau de N cellules dont les états sont
binaires et dont la règle est vue comme une
fonction Booléenne.
Wolfram [6] a proposé d’utiliser une règle d’AC
binaire (restreinte aux seules cellules voisines)
pour engendrer une suite pseudo-aléatoire qui
pourrait être utilisée comme la clé d’un chiffre de
Vernam.
Objectifs
L’étude de la génération des suites pseudo-aléatoires par des automates cellulaires ne s’est pas arrêtée. Plusieurs pistes sont actuellement à l’étude [3] :
– autoriser les cellules à exécuter des règles différentes (AC non uniformes) ;
– augmenter la taille du voisinage tout en conservant la même règle pour l’ensemble des cellules.
On se propose d'étudier la règle de l’AC comme une fonction Booléenne et d’utiliser la dynamique des AC pour étendre l’arité de la règle en une fonction Booléenne à N variables afin d’en extraire une suite pseudo-aléatoire. Pour cela, on cherche des fonctions Booléennes à plus de trois variables avec de bonnes propriétés de résilience et de non-linéarité. Une partie de l’étude a déjà été faite [2] et devra être étudiée.
Le but du stage est de comparer la qualité des suite pseudo-aléatoires engendrées par les deux approches citées en faisant le lien entre les propriétés des fonctions Booléennes et la dynamique d’un automate cellulaire du point de vue de la génération déterministe de suites pseudo-aléatoires.
Nous avons montré [4] qu’une seule règle pouvait
engendrer des suites pseudo-aléatoires
convenables. Cependant, ce générateur de suites
pseudo-aléatoires n’a pas résisté à diverses
attaques [1, 5].
Objectifs
L’étude de la génération des suites pseudo-aléatoires par des automates cellulaires ne s’est pas arrêtée. Plusieurs pistes sont actuellement à l’étude [3] :
– autoriser les cellules à exécuter des règles différentes (AC non uniformes) ;
– augmenter la taille du voisinage tout en conservant la même règle pour l’ensemble des cellules.
On se propose d'étudier la règle de l’AC comme une fonction Booléenne et d’utiliser la dynamique des AC pour étendre l’arité de la règle en une fonction Booléenne à N variables afin d’en extraire une suite pseudo-aléatoire. Pour cela, on cherche des fonctions Booléennes à plus de trois variables avec de bonnes propriétés de résilience et de non-linéarité. Une partie de l’étude a déjà été faite [2] et devra être étudiée.
Le but du stage est de comparer la qualité des suite pseudo-aléatoires engendrées par les deux approches citées en faisant le lien entre les propriétés des fonctions Booléennes et la dynamique d’un automate cellulaire du point de vue de la génération déterministe de suites pseudo-aléatoires.
Compétences souhaitées
Connaissances en informatique théorique
(complexité, cryptographie). Programmation en C ou
C++.
Références
[1] A.M. Apohan and C.K. Koc. Inversion of cellular automata iterations. In Computer and Digital Techniques,
volume 144, pages 279–284, 1997.
[2] A. Braeken, Y. Borissov, S. Nikova, and B. Preneel. Classification of boolean functions of 6 variables or less with
respect to cryptographic properties. Technical report, IACR248, 2008.
[3] P. Lacharme, B. Martin, and P. Sol´e. Pseudo-random sequences, boolean functions and cellular automata. In
Proceedings of Boolean Functions and Cryptographic Applications, 2008. A paraˆıtre.
[4] B. Martin. A Walsh exploration of elementary CA rules. Journal of Cellular Automata, 3(2) :145–156, 2008.
[5] W. Meier and O. Staffelbach. Analysis of pseudo random sequences generated by cellular automata. In EUROCRYPT
’91, Lecture Notes in Computer Science, pages 186–200. Springer Verlag, 1991.
[6] S.Wolfram. Cryptography with cellular automata. In CRYPTO 85, volume 218 of LNCS, pages 429–432. Springer
Verlag, 1985.
Stages sur la programmation par contraintes (PPC)
14/12/10 10:30 |
Stages 2010/11
| Permalien
Laboratoire : I3S, Sophia Antipolis
Equipe : CeP
Contact : Jean-Charles Régin (jean-charles point regin arobase unice point fr)
Les étudiants seront amenés à utiliser des solvers basés sur la PPC dejà existant
Equipe : CeP
Contact : Jean-Charles Régin (jean-charles point regin arobase unice point fr)
L'équipe CeP propose les stages suivants tous basés
sur la programmation par contraintes (PPC).
Remarque : il n'est pas nécessaire de connaitre la
programmation par contraintes. L'idée de base de la
PPC est de résoudre des problèmes complexes de
facon exacte en utilisant la résolution de
sous-problèmes (contraintes) faciles inclus dans le
problème général.
Les étudiants seront amenés à utiliser des solvers basés sur la PPC dejà existant
Sujets :
1) PPC et multithreading : il s'agit d'écrire le code permettant de lancer des solver en parallèle sur une machine multicoeurs.
2) Combinaisons de contraintes : il s'agit d'énumérer les solutions de 2 contraintes puis de les combiner sous la forme d'une seule contrainte plus générale et d'étudier les performances de la combinaison obtenue. L'étudiant devra coder.
3) Recherche de toutes les solutions dans un problème de PPC. Lors de l'énumération de toutes les solutions, l'utilisateur fait face à un grand nombre de symmétries. Il s'agit d'essayer de limiter l'explosition combinatoire (par exemple si 2 variables x et y peut prendre les memes valeurs alors on essaiera de ne produire que les solutions ou x <= y). L'étudiant pourra coder mais ce n'est pas obligatoire.
4) Application des heuristiques de l'algorithme de Belmann-Ford dans le cadre de la PPC. Il s'agit ici principalement de coder les heuristiques de Bellmann-Ford en PPC. L'étudiant devra être imaginatif pour résoudre certains problèmes
5) Affichage de données liées à la PPC et notamment au problème du bin-packing. L'étudiant devra définir une interface graphique claire et la programmer pour afficher des résolutions de problèmes dit de bin-packing.
1) PPC et multithreading : il s'agit d'écrire le code permettant de lancer des solver en parallèle sur une machine multicoeurs.
2) Combinaisons de contraintes : il s'agit d'énumérer les solutions de 2 contraintes puis de les combiner sous la forme d'une seule contrainte plus générale et d'étudier les performances de la combinaison obtenue. L'étudiant devra coder.
3) Recherche de toutes les solutions dans un problème de PPC. Lors de l'énumération de toutes les solutions, l'utilisateur fait face à un grand nombre de symmétries. Il s'agit d'essayer de limiter l'explosition combinatoire (par exemple si 2 variables x et y peut prendre les memes valeurs alors on essaiera de ne produire que les solutions ou x <= y). L'étudiant pourra coder mais ce n'est pas obligatoire.
4) Application des heuristiques de l'algorithme de Belmann-Ford dans le cadre de la PPC. Il s'agit ici principalement de coder les heuristiques de Bellmann-Ford en PPC. L'étudiant devra être imaginatif pour résoudre certains problèmes
5) Affichage de données liées à la PPC et notamment au problème du bin-packing. L'étudiant devra définir une interface graphique claire et la programmer pour afficher des résolutions de problèmes dit de bin-packing.
Recherche de bornes maximales pour la vérification de
programmes
14/12/10 10:14 |
Stages 2010/11
| Permalien
Laboratoire : I3S
Equipe : CeP
Contact : Michel Rueher (michel point rueher arobase unice point fr)
[1] The ASTRÉE Static Analyzer. http://www.astree.ens.fr/
[2] Vijay D'Silva, Daniel Kroening, and Georg Weissenbacher. A survey of automated techniques for formal software verifcation. IEEE Trans. on CAD of Integrated Circuits and Systems, 27(7):1165-1178, 2008.
[3] Malay K Ganai and Aarti Gupta. Accelerating high-level bounded model checking. In ICCAD, pages 794- 801. ACM, 2006.
[4] A Constraint-Programming Framework for Bounded Program Verification. Hélène Collavizza, Michel Rueher, and Pascal Van Hentenryck. Constraints Journal, Springer Verlag, vol. 15(2):238-264, 2010.
[5] Exploration of the capabilities of Constraint Programming Techniques for Software Verification . Hélène Collavizza and Michel Rueher.Proceedings of TACAS 06 (TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, LNCS: 3920/2006:182-196, 2006.
[6] CBMC : a Bounded Model Checker for ANSI-C and C++ programs. http://www.cprover.org/cbmc/
Equipe : CeP
Contact : Michel Rueher (michel point rueher arobase unice point fr)
La vérification automatique de programmes est
reconnue comme l’un des grands challenges de la
recherche en informatique. Deux techniques
complémentaires sont aujourd'hui utilisées:
l'interprétation abstraite et la vérification de
modèle bornée (Bounded Model Checking).
Les outils basés sur l'interprétation abstraite[1]
construisent une approximation des programmes et
permettent de garantir qu'un programme ne vas pas
provoquer des erreurs d'exécution suite à une
division par 0, au dépassement des bornes d'un
tableau, ou suite à un débordement sur les entiers.
Les techniques de Bounded Model Checking (BMC)
permettent de vérifier des propriétés plus
complexes mais la violation de ces propriétés n'est
détectée que pour des bornes fixées. Les techniques
de BMC ont été largement utilisées dans l'industrie
des semi-conducteurs pour trouver des erreurs dans
la conception de matériel et sont de plus en plus
utilisées pour les logiciels [2]. Le processus de
vérification (cf. [3]) consiste principalement à:
- Dérouler le programme k fois,
- Traduire le programme et la propriété en une
formule F telle que F est satisfiable si et
seulement si il existe un contre-exemple de
profondeur inférieure à k
- Utiliser un solveur pour vérifier la
satisfiabilité de F. L'utilisation des techniques
de programmation par contraintes dans cette
dernière étape permet de fournir un
contre-exemple lorsque la formule n'est pas
vérifiée [4,5].
Le problème qu'on propose de traiter ici concerne
la recherche des valeurs maximales des données
d'entrée pour qu'un programme soit correct, c'est à
dire pour qu'un outil d'interprétation abstraite
puisse garantir qu'il n'y a pas de débordement et
qu'un outil de BMC puisse vérifier certaines
propriétés. Dans le cadre de ce projet on abordera
ce problème avec les techniques de programmation
par contraintes et on se restreindra aux entiers.
[1] The ASTRÉE Static Analyzer. http://www.astree.ens.fr/
[2] Vijay D'Silva, Daniel Kroening, and Georg Weissenbacher. A survey of automated techniques for formal software verifcation. IEEE Trans. on CAD of Integrated Circuits and Systems, 27(7):1165-1178, 2008.
[3] Malay K Ganai and Aarti Gupta. Accelerating high-level bounded model checking. In ICCAD, pages 794- 801. ACM, 2006.
[4] A Constraint-Programming Framework for Bounded Program Verification. Hélène Collavizza, Michel Rueher, and Pascal Van Hentenryck. Constraints Journal, Springer Verlag, vol. 15(2):238-264, 2010.
[5] Exploration of the capabilities of Constraint Programming Techniques for Software Verification . Hélène Collavizza and Michel Rueher.Proceedings of TACAS 06 (TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, LNCS: 3920/2006:182-196, 2006.
[6] CBMC : a Bounded Model Checker for ANSI-C and C++ programs. http://www.cprover.org/cbmc/