Concernant le premier paragraphe, je ne cherche pas à dire que les spécifications de CompCert sont fausses, seulement qu'on ne peut pas savoir si elles sont complètes et réalistes. Pour citer Xavier Leroy (source):
Csmith has many uses for CompCert, ranging from validating the formal C semantics to finding missing cases and "assertion failed" in the compiler.
Concernant le deuxième paragraphe:
Les "erreurs" citées par l'article "Randomized Stress-Testing of Link-Time Optimizers" de Vu Le, Chengnian Sun et Zhendong Su me semblent extrêmement suspectes, pour ne pas dire foireuses.
Je ne suis pas suffisamment expert pour juger de la validité des bugs ou non. En revanche, ils précisent bien que les auteurs de CompCert eux-mêmes ont reconnu la validité de ces bugs (qui ont j'imagine été corrigés depuis).
Csmith c'est ce que tu appelles "PLDI'11"; je ne suis pas convaincu par cette façon de nommer des articles qui tait l'important (le titre et les auteurs—et l'année) et montre la conférence, peu importante et source de vanité.
Juste pour donner mon point de vue: je considère au contraire que la conférence/journal (ainsi que l'année, incluse dans cette notation) est bien l'une, si ce n'est la plus importante, des informations à donner—à l'inverse de la liste des auteurs qui est bien elle l'information la moins importante. J'aurais du citer le titre en revanche.
[^] # Re: Nuance
Posté par Cioran_Naroic . En réponse au journal Xavier Leroy est le lauréat 2016 du Prix Milner.. Évalué à 1.
Concernant le premier paragraphe, je ne cherche pas à dire que les spécifications de CompCert sont fausses, seulement qu'on ne peut pas savoir si elles sont complètes et réalistes. Pour citer Xavier Leroy (source):
Concernant le deuxième paragraphe:
Je ne suis pas suffisamment expert pour juger de la validité des bugs ou non. En revanche, ils précisent bien que les auteurs de CompCert eux-mêmes ont reconnu la validité de ces bugs (qui ont j'imagine été corrigés depuis).
Juste pour donner mon point de vue: je considère au contraire que la conférence/journal (ainsi que l'année, incluse dans cette notation) est bien l'une, si ce n'est la plus importante, des informations à donner—à l'inverse de la liste des auteurs qui est bien elle l'information la moins importante. J'aurais du citer le titre en revanche.