flat assembler
Message board for the users of flat assembler.

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

Thread Post new topic Reply to topic

Joined: 21 Jul 2003
Posts: 3555
Location: vpcmipstrm
bitRAKE 26 Jun 2021, 13:24
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:

Project is active on GitHub:
(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).
Filename: fasmg_z3.zip
Filesize: 26.01 KB
Downloaded: 275 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-2023, Tomasz Grysztar. Also on GitHub, YouTube, Twitter.

Website powered by rwasa.