k-legacy icon indicating copy to clipboard operation
k-legacy copied to clipboard

Published 20 hours ago • verified publisher icon kframework

Z3 solver

Open smaaliSahar opened this issue 8 years ago • 4 comments

Hello, I want to use Z3 solver of the K tool in order to verify my models. where may I find documentations or examples?? Thank you for replying.

smaaliSahar avatar Mar 21 '16 09:03 smaaliSahar

Hi, we usually recommend people who want to start using K to have a look at K tutorial http://www.kframework.org/index.php/K_Tutorial

laurayuwen avatar Mar 22 '16 03:03 laurayuwen

Hi, thank you for your answer. Actually, I know how to use K and I have defined my own language. Now, I want to use Z3 solver interface but I could not find documentation about it.

smaaliSahar avatar Mar 22 '16 10:03 smaaliSahar

Sorry, we haven't documented everything. You can find some examples, such as verifying some bst properties, in https://github.com/kframework/java-semantics, in src/verification

laurayuwen avatar Mar 23 '16 04:03 laurayuwen

Thank you for your help

smaaliSahar avatar Mar 23 '16 07:03 smaaliSahar