Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks

Autor: Liu, Jiaxiang, Xing, Yunhan, Shi, Xiaomu, Song, Fu, Xu, Zhiwu, Ming, Zhong

As a new programming paradigm, deep neural networks (DNNs) have been increasingly deployed in practice, but the lack of robustness hinders their applications in safety-critical domains. While there are techniques for verifying DNNs with formal guaran

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

Certification of an Instruction Set Simulator

Autor: Shi, Xiaomu

Cette thèse expose nos travaux de certification d'une partie d'un programme C/C++ nommé SimSoC (Simulation of System on Chip), qui simule le comportement d'architectures basées sur des processeurs tels que ARM, PowerPC, MIPS ou SH4. Un simulateur

Externí odkaz: http://www.theses.fr/2013GRENM075/document

Designing a CPU model: from a pseudo-formal document to fast code

Autor: Blanqui, Frédéric, Helmstetter, Claude, Joloboff, Vania, Monin, Jean-François, Shi, Xiaomu

For validating low level embedded software, engineers use simulators that take the real binary as input. Like the real hardware, these full-system simulators are organized as a set of components. The main component is the CPU simulator (ISS), because

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

Certification d'un simulateur de jeu d'instructions

Autor: Shi, Xiaomu

Publikováno v: Embedded Systems. Université de Grenoble, 2013. English. ⟨NNT : 2013GRENM075⟩

Approaches based on axiomatic semantics (typically, Hoare logic) are the mostpopular for proving the correctness of imperative programs. However, we prefered totry a less usual but more direct approach, based on operational semantics : this wasmade p

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::44514fa78fe77002104ff7ce4c08405f
https://theses.hal.science/tel-00937524v2

Designing a CPU model: from a pseudo-formal document to fast code

Autor: Blanqui, Fr��d��ric, Helmstetter, Claude, Joloboff, Vania, Monin, Jean-Fran��ois, Shi, Xiaomu

Publikováno v: 3rd Workshop on: Rapid Simulation and Performance Evaluation: Methods and Tools
3rd Workshop on: Rapid Simulation and Performance Evaluation: Methods and Tools, Jan 2011, Heraklion, Greece

For validating low level embedded software, engineers use simulators that take the real binary as input. Like the real hardware, these full-system simulators are organized as a set of components. The main component is the CPU simulator (ISS), because

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9c89d10efb449d3f103862ab8e7c9e1c
https://hal.inria.fr/inria-00546228