Equational reasoning and combination methods: from programs to proofs
Identifieur interne : 002002 ( Hal/Corpus ); précédent : 002001; suivant : 002003Equational reasoning and combination methods: from programs to proofs
Auteurs : Christophe RingeissenSource :
Descripteurs français
- mix :
English descriptors
Abstract
In this document, we present decision procedures and solvers which are useful in verification. We consider first order logic with equality. This logic is undecidable in general, but the study of interesting fragments leads to automatic (push-button) tools. The notion of equality is particularly interesting for programming via oriented equalities (rule-based programming) or for deriving proofs thanks to the principle of replacement of equal by equal. In a modelisation using first order logic with equality, we easily have to deal with a problem involving different theories. For instance, these theories may be used to modelise the functions, the arithmetic operations and the memory of a program. Hence, we have to face a problem expressed in a combination of theories, which is interesting to solve in a modular way by using the decision procedures known for individual theories. This problem is the bulk of my research interests. The originality of my approach consists in developing combination methods which are useful in the domain of verification. All the given decision procedures are designed by using a rule-based formalism to ease their proofs.
Url:
Links to Exploration step
Hal:tel-00578600Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Equational reasoning and combination methods: from programs to proofs</title><title xml:lang="fr">Raisonnement équationnel et méthodes de combinaison: de la programmation à la preuve</title><author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name><affiliation><hal:affiliation type="researchteam" xml:id="struct-2366" status="OLD"><idno type="RNSR">200318302K</idno><orgName>Combination of approaches to the security of infinite states systems</orgName><orgName type="acronym">CASSIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/cassis</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation><relation active="#struct-866" type="direct"></relation><relation active="#struct-242365" type="indirect"></relation><relation active="#struct-300261" type="indirect"></relation><relation active="#struct-300360" type="indirect"></relation><relation name="UMR6174" active="#struct-441569" type="indirect"></relation><relation active="#struct-2496" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-866" type="direct"><org type="laboratory" xml:id="struct-866" status="VALID"><idno type="IdRef">152639071</idno><idno type="RNSR">200412232H</idno><orgName>Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies</orgName><orgName type="acronym">FEMTO-ST</orgName><desc><address><addrLine>32 avenue de l'Observatoire 25044 BESANCON CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.femto-st.fr</ref></desc><listRelation><relation active="#struct-242365" type="direct"></relation><relation active="#struct-300261" type="direct"></relation><relation active="#struct-300360" type="direct"></relation><relation name="UMR6174" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-242365" type="indirect"><org type="institution" xml:id="struct-242365" status="VALID"><idno type="IdRef">026403188</idno><idno type="ISNI">0000 0001 2188 3779 </idno><orgName>Université de Franche-Comté</orgName><orgName type="acronym">UFC</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.univ-fcomte.fr</ref></desc></org></tutelle><tutelle active="#struct-300261" type="indirect"><org type="institution" xml:id="struct-300261" status="VALID"><orgName>Université de Technologie de Belfort-Montbeliard</orgName><orgName type="acronym">UTBM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300360" type="indirect"><org type="institution" xml:id="struct-300360" status="VALID"><orgName>Ecole Nationale Supérieure de Mécanique et des Microtechniques</orgName><orgName type="acronym">ENSMM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR6174" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:tel-00578600</idno><idno type="halId">tel-00578600</idno><idno type="halUri">https://tel.archives-ouvertes.fr/tel-00578600</idno><idno type="url">https://tel.archives-ouvertes.fr/tel-00578600</idno><date when="2009-11-27">2009-11-27</date><idno type="wicri:Area/Hal/Corpus">002002</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Equational reasoning and combination methods: from programs to proofs</title><title xml:lang="fr">Raisonnement équationnel et méthodes de combinaison: de la programmation à la preuve</title><author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name><affiliation><hal:affiliation type="researchteam" xml:id="struct-2366" status="OLD"><idno type="RNSR">200318302K</idno><orgName>Combination of approaches to the security of infinite states systems</orgName><orgName type="acronym">CASSIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/cassis</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation><relation active="#struct-866" type="direct"></relation><relation active="#struct-242365" type="indirect"></relation><relation active="#struct-300261" type="indirect"></relation><relation active="#struct-300360" type="indirect"></relation><relation name="UMR6174" active="#struct-441569" type="indirect"></relation><relation active="#struct-2496" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-866" type="direct"><org type="laboratory" xml:id="struct-866" status="VALID"><idno type="IdRef">152639071</idno><idno type="RNSR">200412232H</idno><orgName>Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies</orgName><orgName type="acronym">FEMTO-ST</orgName><desc><address><addrLine>32 avenue de l'Observatoire 25044 BESANCON CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.femto-st.fr</ref></desc><listRelation><relation active="#struct-242365" type="direct"></relation><relation active="#struct-300261" type="direct"></relation><relation active="#struct-300360" type="direct"></relation><relation name="UMR6174" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-242365" type="indirect"><org type="institution" xml:id="struct-242365" status="VALID"><idno type="IdRef">026403188</idno><idno type="ISNI">0000 0001 2188 3779 </idno><orgName>Université de Franche-Comté</orgName><orgName type="acronym">UFC</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.univ-fcomte.fr</ref></desc></org></tutelle><tutelle active="#struct-300261" type="indirect"><org type="institution" xml:id="struct-300261" status="VALID"><orgName>Université de Technologie de Belfort-Montbeliard</orgName><orgName type="acronym">UTBM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300360" type="indirect"><org type="institution" xml:id="struct-300360" status="VALID"><orgName>Ecole Nationale Supérieure de Mécanique et des Microtechniques</orgName><orgName type="acronym">ENSMM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR6174" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation></affiliation></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>combination</term><term>decision procedure</term><term>equational reasoning</term><term>rewriting</term><term>unions of theories</term></keywords><keywords scheme="mix" xml:lang="fr"><term>combinaison</term><term>mélange de théories</term><term>procédure de décision</term><term>raisonnement équationnel</term><term>réécriture</term><term>unification</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">In this document, we present decision procedures and solvers which are useful in verification. We consider first order logic with equality. This logic is undecidable in general, but the study of interesting fragments leads to automatic (push-button) tools. The notion of equality is particularly interesting for programming via oriented equalities (rule-based programming) or for deriving proofs thanks to the principle of replacement of equal by equal. In a modelisation using first order logic with equality, we easily have to deal with a problem involving different theories. For instance, these theories may be used to modelise the functions, the arithmetic operations and the memory of a program. Hence, we have to face a problem expressed in a combination of theories, which is interesting to solve in a modular way by using the decision procedures known for individual theories. This problem is the bulk of my research interests. The originality of my approach consists in developing combination methods which are useful in the domain of verification. All the given decision procedures are designed by using a rule-based formalism to ease their proofs.</div></front></TEI><hal api="V3"><titleStmt><title xml:lang="en">Equational reasoning and combination methods: from programs to proofs</title><title xml:lang="fr">Raisonnement équationnel et méthodes de combinaison: de la programmation à la preuve</title><author role="aut"><persName><forename type="first">Christophe</forename><surname>Ringeissen</surname></persName><email></email><idno type="idhal">christophe-ringeissen</idno><idno type="halauthor">64659</idno><affiliation ref="#struct-2366"></affiliation></author><editor role="depositor"><persName><forename>Christophe</forename><surname>Ringeissen</surname></persName><email>Christophe.Ringeissen@loria.fr</email></editor></titleStmt><editionStmt><edition n="v1" type="current"><date type="whenSubmitted">2011-03-21 16:11:27</date><date type="whenModified">2016-05-19 01:12:05</date><date type="whenReleased">2011-03-21 16:47:21</date><date type="whenProduced">2009-11-27</date><date type="whenEndEmbargoed">2011-03-21</date><ref type="file" target="https://tel.archives-ouvertes.fr/tel-00578600/document"><date notBefore="2011-03-21"></date></ref><ref type="file" n="1" target="https://tel.archives-ouvertes.fr/tel-00578600/file/uhp-hdr-cr.pdf"><date notBefore="2011-03-21"></date></ref></edition><respStmt><resp>contributor</resp><name key="103757"><persName><forename>Christophe</forename><surname>Ringeissen</surname></persName><email>Christophe.Ringeissen@loria.fr</email></name></respStmt></editionStmt><publicationStmt><distributor>CCSD</distributor><idno type="halId">tel-00578600</idno><idno type="halUri">https://tel.archives-ouvertes.fr/tel-00578600</idno><idno type="halBibtex">ringeissen:tel-00578600</idno><idno type="halRefHtml">Génie logiciel [cs.SE]. Université Henri Poincaré - Nancy I, 2009</idno><idno type="halRef">Génie logiciel [cs.SE]. Université Henri Poincaré - Nancy I, 2009</idno></publicationStmt><seriesStmt><idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno><idno type="stamp" n="INRIA">INRIA - Institut National de Recherche en Informatique et en Automatique</idno><idno type="stamp" n="UNIV-FCOMTE">Université de Franche-Comté</idno><idno type="stamp" n="INPL">Institut National Polytechnique de Lorraine</idno><idno type="stamp" n="LORIA2">Publications du LORIA</idno><idno type="stamp" n="INRIA-NANCY-GRAND-EST">INRIA Nancy - Grand Est</idno><idno type="stamp" n="LORIA-FM" p="LORIA">Méthodes formelles</idno><idno type="stamp" n="LORIA">LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications</idno><idno type="stamp" n="INRIA2">INRIA 2</idno><idno type="stamp" n="INRIA-LORRAINE">INRIA Nancy - Grand Est</idno><idno type="stamp" n="LABO-LORIA-SET" p="LORIA">LABO-LORIA-SET</idno><idno type="stamp" n="UNIV-LORRAINE">Université de Lorraine</idno><idno type="stamp" n="UNIV-BM">Université de Technologie de Belfort-Montbeliard</idno><idno type="stamp" n="ENSMM">Ecole Nationale Supérieure de Mécanique et des Microtechniques</idno><idno type="stamp" n="FEMTO-ST" p="UNIV-FCOMTE">Franche-Comté Electronique, Mécanique, Thermique et Optique - Sciences et Technologies</idno><idno type="stamp" n="UNIV-BM-THESE">Université de Technologie de Belfort-Montbeliard</idno></seriesStmt><notesStmt></notesStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Equational reasoning and combination methods: from programs to proofs</title><title xml:lang="fr">Raisonnement équationnel et méthodes de combinaison: de la programmation à la preuve</title><author role="aut"><persName><forename type="first">Christophe</forename><surname>Ringeissen</surname></persName><idno type="idHal">christophe-ringeissen</idno><idno type="halAuthorId">64659</idno><affiliation ref="#struct-2366"></affiliation></author></analytic><monogr><imprint><date type="dateDefended">2009-11-27</date></imprint><authority type="institution">Université Henri Poincaré - Nancy I</authority><authority type="supervisor">Gilles Dowek</authority></monogr></biblStruct></sourceDesc><profileDesc><langUsage><language ident="fr">French</language></langUsage><textClass><keywords scheme="author"><term xml:lang="en">equational reasoning</term><term xml:lang="en">rewriting</term><term xml:lang="en">decision procedure</term><term xml:lang="en">combination</term><term xml:lang="en">unions of theories</term><term xml:lang="fr">raisonnement équationnel</term><term xml:lang="fr">réécriture</term><term xml:lang="fr">unification</term><term xml:lang="fr">procédure de décision</term><term xml:lang="fr">combinaison</term><term xml:lang="fr">mélange de théories</term></keywords><classCode scheme="halDomain" n="info.info-se">Computer Science [cs]/Software Engineering [cs.SE]</classCode><classCode scheme="halTypology" n="HDR">Accreditation to supervise research</classCode></textClass><abstract xml:lang="en">In this document, we present decision procedures and solvers which are useful in verification. We consider first order logic with equality. This logic is undecidable in general, but the study of interesting fragments leads to automatic (push-button) tools. The notion of equality is particularly interesting for programming via oriented equalities (rule-based programming) or for deriving proofs thanks to the principle of replacement of equal by equal. In a modelisation using first order logic with equality, we easily have to deal with a problem involving different theories. For instance, these theories may be used to modelise the functions, the arithmetic operations and the memory of a program. Hence, we have to face a problem expressed in a combination of theories, which is interesting to solve in a modular way by using the decision procedures known for individual theories. This problem is the bulk of my research interests. The originality of my approach consists in developing combination methods which are useful in the domain of verification. All the given decision procedures are designed by using a rule-based formalism to ease their proofs.</abstract><abstract xml:lang="fr">Les travaux décrits dans ce document ont pour objectif le développement de procédures de décision (et de résolution) pour la vérification. La logique considérée est la logique du premier ordre avec égalité. Cette logique est évidemment indécidable en général, mais l'étude de fragments intéressants pour la vérification peut conduire à des outils automatiques de type "presse-bouton". La notion d'égalité est particulièrement intéressante pour programmer, par orientation des égalités, c'est-à-dire par réécriture, ou pour prouver, grâce au principe de remplacement d'égal par égal. Dans une modélisation en logique du premier ordre avec égalité, on est très facilement amené à utiliser simultanément plusieurs théories différentes pour représenter par exemple les fonctions et la mémoire d'un programme ainsi que les opérations arithmétiques effectuées par le programme. On se retrouve ainsi naturellement face à un problème exprimé dans un mélange de théories, qu'il est souhaitable de résoudre de façon modulaire en réutilisant les procédures de décision connus pour les théories composant le mélange. Cette problématique est au coeur de mes travaux. L'originalité de mon approche consiste à développer des méthodes de combinaison pour les procédures de décision utilisées dans le domaine de la vérification. Toutes les procédures de décision obtenues ont été évidemment élaborées en suivant une démarche de conception sûre, qui s'appuie sur une description à base de systèmes d'inférence pour faciliter leurs preuves.</abstract></profileDesc></hal></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Hal/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002002 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Hal/Corpus/biblio.hfd -nk 002002 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Hal
|étape= Corpus
|type= RBID
|clé= Hal:tel-00578600
|texte= Equational reasoning and combination methods: from programs to proofs
}}
| This area was generated with Dilib version V0.6.33. |  |