Применение искинов - шоссе империализма (Стенгазета русификаторов ИТ)

Информация о пользователе

Привет, Гость! Войдите или зарегистрируйтесь.

2021, Xu, Automatic Generation and Validation of Instruction Encoders

Страница: 1

Сообщений 1 страница 7 из 7

1

  • Автор: Лис
  • Участник
  • Лис
  • Зарегистрирован: 2023-03-10
  • Приглашений: 0
  • Сообщений: 1011
  • Уважение: [+0/-0]
  • Позитив: [+0/-0]
  • Провел на форуме:
    5 дней 11 часов
  • Последний визит:
    Сегодня 10:00:32

2021-07, Xiangzhe Xu & Jinhua Wu & Yuting Wang &  Zhenguo Yin & Pengfei Li, Automatic Generation and Validation of Instruction Encoders and Decoders
    https://www.researchgate.net/publicatio … coders.pdf

«We observe that consistent encoder-decoder pairs can be automatically derived from bijections inherently embedded in instruction formats.»

«we develop a framework for writing specifications that capture these bijections, for automatically generating encoders and decoders from these specifications, and for formally validating the consistency and soundness of the generated encoders and decoders by synthesizing proofs in Coq and discharging verification conditions using SMT solvers. We apply this framework to a subset of X86-32 instructions to illustrate its effectiveness in these regards. We also demonstrate that the generated encoders and decoders have reasonable performance.»

Отредактировано Лис (2024-08-25 20:52:30)

0

2

  • Автор: Лис
  • Участник
  • Лис
  • Зарегистрирован: 2023-03-10
  • Приглашений: 0
  • Сообщений: 1011
  • Уважение: [+0/-0]
  • Позитив: [+0/-0]
  • Провел на форуме:
    5 дней 11 часов
  • Последний визит:
    Сегодня 10:00:32

«The whole framework took six person months to develop.»

«In the future, we would like to apply this framework to a major part of X86-32 and X86-64 instructions and also to other ISAs, thereby to demonstrate the versatility and scalability of our framework.»

Отредактировано Лис (2024-08-25 19:42:21)

0

3

  • Автор: Лис
  • Участник
  • Лис
  • Зарегистрирован: 2023-03-10
  • Приглашений: 0
  • Сообщений: 1011
  • Уважение: [+0/-0]
  • Позитив: [+0/-0]
  • Провел на форуме:
    5 дней 11 часов
  • Последний визит:
    Сегодня 10:00:32

Xiangzhe Xu
Purdue University
https://scholar.google.com/citations?hl … by=pubdate

Смотрим, продолжил ли он исследования в обещаемом направлении, или оставил последователям, или этим занимался на самом деле кто-то другой из их команды.

2023, Wu J & Wang Y & Sun M & Xu X & Y Song, Towards a Framework for Developing Verified Assemblers for the ELF Format
Asian Symposium on Programming Languages and Systems, 205-224

2020, Wang Y & Xu X & Wilke P & Shao Z, CompCertELF: verified separate compilation of C programs into ELF object files
Proceedings of the ACM on Programming Languages 4 (OOPSLA), 1-28

Университет Пердью — общественный исследовательский университет в США, расположенный в городе Уэст-Лафейетт, штат Индиана, главный из шести кампусов Системы университетов Пёрдью. Университет неизменно входит в списки самых престижных высших учебных заведений.

Можно ли предположить, что эти исследования финансируются из оплаты обучения студентами (их родителями), обучающимися там?
Учитывая, что он общественный, мы бы тоже так могли?
Как при этом он может быть "исследовательским"? Т.е. он зарабатывает исследованиями на заказ?

«This work was supported by the National Natural Science Foundation of China (NSFC) under Grant No. 62002217.»

Отредактировано Лис (2024-08-25 20:04:18)

0

4

  • Автор: Лис
  • Участник
  • Лис
  • Зарегистрирован: 2023-03-10
  • Приглашений: 0
  • Сообщений: 1011
  • Уважение: [+0/-0]
  • Позитив: [+0/-0]
  • Провел на форуме:
    5 дней 11 часов
  • Последний визит:
    Сегодня 10:00:32

Jinhua Wu
https://scholar.google.com/citations?hl … by=pubdate
https://orcid.org/0000-0001-5812-053X
Shanghai Jiao Tong University, Shanghai, China

0

5

  • Автор: Лис
  • Участник
  • Лис
  • Зарегистрирован: 2023-03-10
  • Приглашений: 0
  • Сообщений: 1011
  • Уважение: [+0/-0]
  • Позитив: [+0/-0]
  • Провел на форуме:
    5 дней 11 часов
  • Последний визит:
    Сегодня 10:00:32

Yuting Wang
https://jhc.sjtu.edu.cn/~yutingwang/
https://scholar.google.com/citations?hl … by=pubdate
https://orcid.org/0000-0003-3990-2418
Shanghai Jiao Tong University, 200240, Shanghai, China
John Hopcroft Center for Computer Science (https://jhc.sjtu.edu.cn/ , Tenure-Track Associate Professor)

2023, Wu J & Wang Y & Sun  M & Xu X & Song Y, Towards a Framework for Developing Verified Assemblers for the ELF Format
Asian Symposium on Programming Languages and Systems, 205-224

2022, Wang Y & Zhang L & Shao Z & Koenig J, Verified compilation of C programs with a nominal memory model
Proceedings of the ACM on Programming Languages 6 (POPL), 1-31

Research Interests

I am broadly interested in the following research areas:

    Formal Verification
    Programming Languages
    Proof Theory and Type Theory
    Logical Framework

My current research focuses on techniques and frameworks for verifying system software (including compilers and operating systems). I am also involved in developing theories and frameworks for programming, specifying and verifying rule-based relational specifications.
This line of research centers on the development of the Abella theorem prover.

Отредактировано Лис (2024-08-25 20:41:12)

0

6

  • Автор: Лис
  • Участник
  • Лис
  • Зарегистрирован: 2023-03-10
  • Приглашений: 0
  • Сообщений: 1011
  • Уважение: [+0/-0]
  • Позитив: [+0/-0]
  • Провел на форуме:
    5 дней 11 часов
  • Последний визит:
    Сегодня 10:00:32

Pengfei Li
Shanghai Jiao Tong University
Department of Nuclear Science and Engineering
Assistant Professor
https://me.sjtu.edu.cn/en/FullTimeTeach … ngfei.html

по фотке его не найти, потому что все азиаты на одно лицо (для images.google.com).
https://me.sjtu.edu.cn/upload/image/201 … 164830.jpg

Скрытный человек, у которого нет работ на Research Gate
«This page lists works of an author who doesn't have a ResearchGate profile or hasn't added the works to their profile yet.»

0

7

  • Автор: Лис
  • Участник
  • Лис
  • Зарегистрирован: 2023-03-10
  • Приглашений: 0
  • Сообщений: 1011
  • Уважение: [+0/-0]
  • Позитив: [+0/-0]
  • Провел на форуме:
    5 дней 11 часов
  • Последний визит:
    Сегодня 10:00:32

Zhenguo Yin
Shanghai Jiao Tong University, Shanghai, 200240, China

0

Страница: 1