search

kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

Z3 solver #2157

Open smaaliSahar opened 8 years ago

smaaliSahar commented 8 years ago

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.

laurayuwen commented 8 years ago

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

smaaliSahar commented 8 years ago

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.

laurayuwen commented 8 years ago

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

smaaliSahar commented 8 years ago

Thank you for your help