Specification inference capabilities of Verifast

[Sophie Lathouwers]

Hi Verifast team!

I came across several papers about specification inference/generation with Verifast and wanted to try this for myself with some examples. I tried to find the specification inference option in Verifast but have not been able to find it. I found the shape analysis option but this only seems available for C programs (I have a Java example).
I used the latest nightly build. However, there are several other repositories such as https://github.com/Mahmohsen/AutoVeriFast and https://github.com/Mahmohsen/verifast/tree/Automated-Verifast. I am unsure what would be the correct repository to use.

In short, does Verifast currently support specification inference for Java programs? If so, where can I find this?


Kind regards,
Sophie Lathouwers

[Bart Jacobs]

Hi Sophie,

Unfortunately, it does not. My former PhD student Mahmoud Mohsen has worked on this, but he left before he could finish it and integrate it into the mainline.

Best,

Bart

Op 15 mrt. 2023 om 11:21 heeft Sophie Lathouwers <sophie.l...@gmail.com> het volgende geschreven:

Hi Verifast team!

--
You received this message because you are subscribed to the Google Groups "VeriFast" group.
To unsubscribe from this group and stop receiving emails from it, send an email to verifast+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/verifast/eb1e765c-8b55-4485-830f-0232ce4ac7fbn%40googlegroups.com.