Easing Maintenance of Academic Static Analyzers

Autor: Monat, Raphaël, Ouadjaout, Abdelraouf, Miné, Antoine

Academic research in static analysis produces software implementations. These implementations are time-consuming to develop and some need to be maintained in order to enable building further research upon the implementation. While necessary, these pr

Externí odkaz: http://arxiv.org/abs/2407.12499

Abstract interpretation of Michelson smart-contracts

Autor: Bau, Guillaume, Miné, Antoine, Botbol, Vincent, Bouaziz, Mehdi

Publikováno v: SOAP '22: 11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, Jun 2022, San Diego, CA, United States. pp.36-43

Static analysis of smart-contracts is becoming more widespread on blockchain platforms. Analyzers rely on techniques like symbolic execution or model checking, but few of them can provide strong soundness properties and guarantee the analysis termina

Externí odkaz: http://arxiv.org/abs/2210.05217

Input Validation for Neural Networks via Runtime Local Robustness Verification

Autor: Liu, Jiangchao, Chen, Liqian, Mine, Antoine, Wang, Ji

Local robustness verification can verify that a neural network is robust wrt. any perturbation to a specific input within a certain distance. We call this distance Robustness Radius. We observe that the robustness radii of correctly classified inputs

Externí odkaz: http://arxiv.org/abs/2002.03339

Analyse statique par interprétation abstraite de programmes concurrents

Autor: Miné, Antoine

Ce mémoire d'habilitation résume la majeure partie de mes recherches, depuis la fin de mon doctorat, fin 2004, jusqu'à aujourd'hui. Le but essentiel de mes recherches est le développement de méthodes fondées sur des bases mathématiques et perf

Externí odkaz: http://tel.archives-ouvertes.fr/tel-00903447
http://tel.archives-ouvertes.fr/docs/00/90/34/47/PDF/hdr-compact-col.pdf
http://tel.archives-ouvertes.fr/docs/00/90/34/47/ANNEX/expose_ok.pdf

Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs

Autor: Miné, Antoine

Publikováno v: Logical Methods in Computer Science, Volume 8, Issue 1 (March 26, 2012) lmcs:799

We present a static analysis by Abstract Interpretation to check for run-time errors in parallel and multi-threaded C programs. Following our work on Astr\'ee, we focus on embedded critical programs without recursion nor dynamic memory allocation, bu

Externí odkaz: http://arxiv.org/abs/1203.3724