search

ftsrg / theta

Generic, modular and configurable formal verification framework supporting various formalisms and algorithms
http://theta.inf.mit.bme.hu/
Apache License 2.0
49 stars 43 forks source link

XSTS-cli: Allow the specification of the verification property in the XSTS file #301

Closed arminzavada closed 1 month ago

arminzavada commented 1 month ago

The current possible property configurations are the following:

Missing: The ability to specify the property as part of the XSTS file with a syntax similar to the supported property file.

Is this currently possible, and I just missed the feature?

Justification: The construction of the XSTS file is negligible compared to the actual verification task. Thus, it makes sense to construct a new XSTS file for each verification case, especially since a lot of model simplifications can be performed when knowing the property to be verified. I am taking this approach in Semantifyr, and I believe a similar approach is also used in Gamma. However, converting XSTS files to the supported format is cumbersome and should be simple to handle on the Theta side, by extending the XSTS grammar.

arminzavada commented 1 month ago

I have double checked, and realized, that this feature already exists currently.