theta
theta copied to clipboard
ftsrg
Generic, modular and configurable formal verification framework supporting various formalisms and algorithms
This is the result of my BSc degree project: a CHC frontend implemented in Theta. It can be enabled with the `--chc` flag, and different transformation methods can be chosen...
Adding a workflow which generate release automaticly. The .jar files are generated by the gradle build and the version number is equals with the build.gradle.kts all-project version number
The expression simplification of `FpDivExpr`s sometimes yield bad results: https://github.com/ftsrg/theta/blob/b379e4ea0a77db26c040ad7798936fd1caeee7d3/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java#L1967-L1984 The underlying problem seems to be not with Theta, but with the BigFloat library. To see the wrong results: ```...
This PR adds the following flags to XstsCli: * `--smt-home`: folder where smt solvers are located * `--refinement-solver`: solver to use during refinement * `--abstraction-solver`: solver to use during abstraction....
This pull request contains an abstraction-aware partial order reduction for the XCFA project. More details about the algorithm can be found in my Scientific Students' Association Report.
A beta version of Ubuntu 22.04 environment is available. Are there any objections on building there as well?
Two variables with the same name (but different values) can be put in the explicit state. This may result in a false unsafe verdict (with an incorrect counterexample). A function...
As discussed at TACAS, it would be great if Theta could support CHC front-end. The language is a simple extension of SMT-LIB, format described [here](https://chc-comp.github.io/format.html). At least transition systems (1...
