Bienvenue sur mon site Web personnel. Je suis Professeur au département
d'informatique et de génie logiciel depuis janvier 2003. Le principal
objectif de ma recherche est l'élaboration de méthodes et d'outils pratiques,
fondés sur des aspects formels et théoriques, pour l'analyse et la
certification de systèmes informatiques (programmes, traces réseaux, etc.),
relativement à des propriétés données.
Cours
- IFT-3000: Langages de
programmation.
- GLO-7003:
Certification de logiciels (cours gradué).
Publications
|
[1]
|
Waly, H. et B. Ktari, A complete framework for kernel trace analysis,
Proceedings of the 24th Canadian Conference on Electrical and Computer
Engineering, CCECE 2011, Niagara Falls, Ontario, 1426-1430, 16 pages. IEEE,
2011.
|
|
[2]
|
Bolduc, C.et B. Ktari. Verification of Common Interprocedural Compiler Optimizations Using Visibly
Pushdown Kleene Algebra. Relation and Kleene Algebra in Computer Science,
Proceedings of the 13th International Conference, AMAST'2010, Québec, Qc,
Canada, June 23-25, LNCS, 16 pages, Springer, juin
2010.
|
|
[3]
|
Bolduc,
C. et B. Ktari. Verification of Common Interprocedural Compiler Optimizations Using Visibly
Pushdown Kleene Algebra (Extended Version). Rapport de recherche DIUL-RR-1001, Département
d’informatique et de génie logiciel, Université Laval, 101 pages,
avril 2010.
|
|
[4]
|
Bolduc,
C. et B. Ktari. Visibly pushdown
Kleene algebra. Rapport de recherche
DIUL-RR-0901, Département d’informatique et de génie logiciel, Université
Laval, 101 pages, novembre 2009.
|
|
[5]
|
Bolduc, C.et B. Ktari. Visibly pushdown Kleene
algebra and its use in interprocedural analysis
of (mutually) recursive programs. Relation and Kleene Algebra in Computer
Science, Proceedings of the 11th International Conference on Relational
Methods in Computer Science and 6th International Conference on
Applications of Kleene Algebra (RelMiCS/AKA),
Doha, Qatar, LNCS, vol. 5827, 15 pages, Springer, novembre
2009.
|
|
[6]
|
Ktari, B.,
F. Lajeunesse-Robert et C. Bolduc, «Solving linear equations in
*-continuous action lattices », Rudolf Berghammer,
Bernhard Möller, et Georg Struth,
editeurs, Relation and Kleene Algebra in
Computer Science, 10th Internation Conference on
Relational Methods in Computer Science and 5th International Conference on
Applications of Kleene Algebra (RelMiCS/AKA), Frauenwörth, Germany, Proceedings, no 4988 dans Lecture Notes in Compter
Science (LNCS), pages 289–303. Springer, avril 2008.
|
|
[7]
|
Ktari, B., F. Lajeunesse-Robert, et C. Bolduc, Solving linear equations in *-continuous
action lattices (Extended Version). rapport
technique, DIUL-RR-0801, université Laval, juin 2008.
|
|
[8]
|
Ktari, B., H. Fujita et M. Mejri et D. Godbout, «Toward a new software
development environment », Knowledge-Based Systems, 20(7),
683–693, octobre 2007.
|
|
[9]
|
Lajeunesse-Robert, F. et B. Ktari, «Toward
Solving Equations in Kleene Algebras », H. Fujita et D.M. Pisanelli, éditeurs, New
Trends in Software Methodologies, Tools and Techniques, Proceedings of the
6th SoMeT International Conference, Roma, Italy,
volume 161, pages 285–304. IOS Press, 2007.
|
|
[10]
|
Godbout, D., B. Ktari et M. Mejri, «A Formal Translation From an Imperative
Language With Array to a Declarative Language », H. Fujita et M. Mejri, éditeurs, New
Trends in Software Methodologies, Tools and Techniques, Proceedings of the
5th SoMeT International Conference, Quebec,
Canada, volume 147, pages 319–339. IOS Press, 2006.
|
|
[11]
|
Fujita, H., B. Ktari et M. Mejri, «Implementing Lyee-calculus
in Java », Knowledge-Based Systems, 19(2), 116–129, juin 2006.
|
|
[12]
|
Mbarki, M., M. Mejri et B. Ktari,
«Converting an imperative program to a declarative one », Knowledge-Based
Systems, 19(2), 130–140, juin 2006.
|
|
[13]
|
Ktari,
B., D. Godbout, M. Mejri, et H. Fujita.
«LyeeBuilder »,
H. Fujita et M. Mejri, éditeurs, New Trends in Software Methodologies,
Tools and Techniques, Proceedings of the 4th SoMeT
International Conference, Tokyo, Japan, volume 129, pages 83–99. IOS Press,
2005.
|
|
[14]
|
Fujita, H., M. Mejri
et B. Ktari, «A process algebra to formalize the Lyee
methodology », Knowledge-Based Systems, 17(7-8), 263–281, décembre 2004.
|
|
[15]
|
Couture, M., B. Ktari, F. Massicotte et
M. Mejri, «A declarative approach to stateful intrusion detection and network monitoring », Proceedings
of the 2nd Annual Conference on Privacy, Security and Trust (PST’04),
p. 175–179, New Brunswick, Canada, octobre
2004.
|
|
[16]
|
Lacasse, A., M. Mejri et B. Ktari,
«Formal implementation of network security policies », Proceedings of
the 2nd Annual Conference on Privacy, Security and Trust (PST’04),
p. 161–166, New Brunswick, Canada, octobre
2004.
|
|
[17]
|
Ktari,
B., M. Mejri et H. Fujita, «From Lyee-calculus to Java
code », H. Fujita et V. Gruhn, éditeurs, New Trends in Software Methodologies, Tools and Techniques, Proceedings of the 3rd SoMeT
International Conference, Tokyo, Japan, volume 111, pages 283–300. IOS Press, 2004.
|
|
[18]
|
Mbarki, M., M. Mejri et B. Ktari,
«From imperative to declarative languages : A formal translation »,
H. Fujita et V. Gruhn, éditeurs, New Trends in Software Methodologies,
Tools and Techniques, Proceedings of the 3rd SoMeT
International Conference, Tokyo, Japan, volume 111, pages 153–177. IOS Press,
2004.
|
|
[19]
|
Couture,
M., B. Ktari, F. Massicotte et M. Mejri, «Détection
d’intrusion et acquisition passive d’information », A. Bouabdallah et A. Serhrouchni,
éditeurs, Proceedings of the 3rd Conference on Security and Network Architectures
(SAR’04), Lalonde, France, pages 309–318, juin 2004.
|
|
[20]
|
Mejri, M., B. Ktari, H. Fujita et M. Erhioui,
«Static analysis on Lyee requirements », Knowledge-Based
Systems, 16(7-8), 361–382, novembre 2003.
|
|
[21]
|
Mejri, M., B. Ktari et H. Fujita, «Lyee
methodology : A formalization using process algebra », H. Fujita et
P. Johannesson, éditeurs,
New Trends in Software Methodologies, Tools and Techniques, Proceedings
of the 2nd SoMeT International Conference, Tokyo,
Japan, volume 98, pages 235–261. IOS Press, 2003.
|
|
[22]
|
Béchir
Ktari, Specification of safety and security policies - litterature review, rapport technique, livrables pour le
Centre de Recherche pour la Défense à Valcartier
(CRDV), Canada, 87 pages, août 2003.
|
|
[23]
|
Béchir
Ktari, Specification of safety and security policies - theoritical study, rapport technique, livrables pour le Centre
de Recherche pour la Défense à Valcartier (CRDV),
Canada, 48 pages, août 2003.
|
|
[24]
|
Debbabi, M., J. Desharnais, B. Ktari, F. Michaud et
N. Tawbi, «A framework for the certification of COTS », I. Chrisment et R. Dssouli,
éditeurs, Proceedings of the 2nd Conference
on Security and Network Architectures (SAR’03), Nancy, France, pages
275–284, juin 2003.
|
|
[25]
|
Ktari, B., «A 3-valued logic for the specification
and the verification of security properties », I. Cervesato,
éditeur, Proceedings of the LICS’03 workshop
on Foundations of Computer Security (FCS), Ottawa, Canada, pages
15–25, juin 2003.
|
|
[26]
|
Béchir
Ktari. Certification de composants logiciels. Thèse de doctorat, Université
Laval, Québec, Canada, avril 2003.
|
|
[27]
|
Mejri,
M., B. Ktari et H. Fujita, Algorithms for static
analysis on Lyee methodology, rapport technique livré à
l’Université Iwate, Japon, 45 pages, janvier 2003.
|
|
[28]
|
Mejri, M., B. Ktari et M. Erhioui,
«Static analysis on Lyee-oriented software »,
P. Johannesson et H. Fujita, éditeurs, New Trends in Software Methodologies,
Tools and Techniques, Proceedings of the Lyee
International Workshop, Paris, France, volume 84, pages 375–394. IOS Press,
2002.
|
|
[29]
|
Bergeron,
J., R. Charpentier, M. Debbabi,
J. Desharnais, E. Giasson, B. Ktari, F. Michaud,
M. Salois et N. Tawbi, «Secure Integration of Critical Software via Certifying compilers », 13th
Congrès Canadien annuel de la sécurité des technologies de l’information,
Symposium CSE, Ottawa, Canada, juin 2001.
|
|
[30]
|
Debbabi, M., B. Ktari, et F. Painchaud.
Emerging Technologies for the Certification of
Critical Software. Tutoriel
présenté au Canadian Security Establishment (CSE) Security Symposium, Ottawa,
juin 2001.
|
|
[31]
|
Debbabi, M., E. Giasson, B. Ktari, F. Michaud, et
N. Tawbi. Secure Self-Certified Code. Proceedings of the
IEEE 5th International Workshop on Enterprise Security (WETICE’00),
National Institute of Standards and Technology (NIST), Maryland, USA,
14–16 juin 2000. IEEE Press.
|
|
[32]
|
Giasson,
E., B. Ktari, et F. Michaud, Compilateur certificateur produisant un code
sûr et sécurisé. Rapport technique, livrables pour le Centre de Recherche
pour la Défense à Valcartier (CRDV), février 2000.
|
|
[33]
|
Bergeron,
J., M. Debbabi, M. Erhioui,
et B. Ktari. Static Analysis of Binary Code to Isolate
Malicious Behaviors. Proceedings of IEEE 4th International Workshop on
Enterprise Security (WETICE’99), Stanford University, California, USA,
16–18 juin 1999. IEEE Press.
|
|
[34]
|
Bergeron,
J., M. Debbabi, J. Desharnais, B.
Ktari, M. Salois, et N. Tawbi. Detection of Malicious Code in COTS Software: A Short Survey. 1st International
Software Assurance Certification Conference
(ISACC’99),
Washington D.C, USA, mars 1999.
|
|
[35]
|
Debbabi, M., A. Benzakour, et B.
Ktari. A Synergy Between Model-Checking and Type
Inference for the Verification of Value-Passing Higher-Order Processes. 7th
International Conference on Algebraic Methodology And Software Technology, AMAST’98,
Lecture Notes in Computer Science, LNCS, Springer Verlag,
vol. 1548. Pages
214–230, Amazonia, Manaus, Brésil,
4–8 janvier 1999.
|
|
[36]
|
Bergeron,
J., M. Debbabi, J. Desharnais, B.
Ktari, M. Salois, et N. Tawbi, Malicious Code Detection.
Rapport technique, livrables pour le Centre de Recherche pour la Défense à Valcartier (CRDV), Canada, novembre 1998.
|
|
[37]
|
Bergeron,
J., M. Debbabi, J. Desharnais, B.
Ktari, M. Salois, et N. Tawbi, Skeleton of a Taxonomy for Malicious Code. Rapport technique, livrables pour le
Centre de Recherche pour la Défense à Valcartier
(CRDV), Canada, novembre 1998.
|
|