Thanks a lot, Quynh, my pleasure will do.
Appreciated!
Sincerely,
Amer
On Fri, Nov 8, 2019 at 3:12 AM Nguyen Anh Quynh <aquynh@xxxxxxxxx> wrote:
Congrats on a nice work!
Feel free to put your paper up in the collection at
https://github.com/unicorn-engine/unicorn/issues/1104
Cheers,
Q
http://www.keystone-engine.org
http://www.capstone-engine.org
http://www.unicorn-engine.org
On Tue, Nov 5, 2019 at 3:54 AM Amer Tahat <antahat@xxxxxx> wrote:
emulator based on a unicorn (AARCH 64) and ASL (ARM specification
Hi All,
We want to share our paper from FMCAD19 with unicorn users,
http://theory.stanford.edu/~barrett/fmcad/papers/FMCAD2019_paper_77.pdf
Among many things, the paper describes a test generator and a formal
language). We lift the formal semantics of the instructions to a theorem
prover PVS7 based on ASL. Then we generated tens of thousands of test cases
using unicorn for the instructions that we formalized. There was an
exciting match between the results obtained from the unicorn emulator and
their formal counterparts of ASL-based PVS7 models. The findings increase
the trust in the unicorn models as well as PVS7's.
details are involved in the article.
The paper has formalized a subset of the instructions of AARCH64; more
Enjoy!
--
Dr. Amer Tahat, Ph.D. CS&E
Systems Software Research Group,
454 Durham, Department of Electrical and Computer Engineering,
Virginia Tech University, Blacksburg, VA, 24061, U.S.A
