flat assembler
Message board for the users of flat assembler.

Index > Windows > [fasmg][Win64] Using Z3 Theorem Prover

Author
Thread Post new topic Reply to topic
bitRAKE



Joined: 21 Jul 2003
Posts: 3415
Location: vpcmipstrm
bitRAKE
Just some simple examples of using this tool from fasmg. The API is all pointers, so it's very easy to use from asm. There is a little bit of a learning curve to constructing model ASTs, but it's totally worth the effort to learn.

The intro tutorial online is quite a good overview of Z3:
https://rise4fun.com/z3/tutorial

Project is active on GitHub:
https://github.com/Z3Prover/z3
(Will need libz3.dll to run the examples. Since the DLL is dependent on UCRT, I've also used it for console output.)

It's really fun tool - will probably be posting more uses of it.

Software Modeling and Verification Lecture playlist (advanced course).
Prof. Joost-Pieter Katoen at RWTH Aachen University


Description: Uses the standard fasmg distro (even if it doesn't look like it, lol).
Download
Filename: fasmg_z3.zip
Filesize: 26.01 KB
Downloaded: 234 Time(s)


_________________
¯\(°_o)/¯ unlicense.org
Post 26 Jun 2021, 13:24
View user's profile Send private message Visit poster's website Reply with quote
Display posts from previous:
Post new topic Reply to topic

Jump to:  


< Last Thread | Next Thread >
Forum Rules:
You cannot post new topics in this forum
You cannot reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
You cannot attach files in this forum
You can download files in this forum


Copyright © 1999-2020, Tomasz Grysztar. Also on GitHub, YouTube, Twitter.

Website powered by rwasa.