How do I represent the control and loop structures using Z3

Reply

KimYLee Posted: 09-09-2009 5:22 AM

rated by 0 users

Hello,

How do I represent some control and loop structures such as:
if...else;
for();
while();

by using Z3 ???

 Thanks

Lee, Kim

Reply

Nikolaj Bjorner replied on 09-09-2009 11:29 AM

rated by 0 users

Dear Lee, Kim.

There was just a similar sounding post. I include the reply:

It sounds like you want to perform program verification. There are several existing tools that build on top of Z3 to perform program verification. In particular, try out Spec#: http://research.microsoft.com/en-us/projects/specsharp/.

You will also find quite extensive documentation on how formulas (verification conditions) are extacted from imperative/object-oriented programs. When done for realistic settings, this is a considerable task.

Regards,

Nikolaj