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

Added specification transformation #317

Closed leventeBajczi closed 2 weeks ago

leventeBajczi commented 3 weeks ago

This adds support for pre-transforming between various specifications.

sonarcloud[bot] commented 2 weeks ago

Quality Gate Failed Quality Gate failed

Failed conditions
53.7% Coverage on New Code (required ≥ 60%)

See analysis details on SonarCloud

github-actions[bot] commented 2 weeks ago

Benchexec test report for a selection of SV-Benchmarks (correct / incorrect / all):

Rundefinition BOUNDED CEGAR HORN
SV-COMP25_no-data-race :question: (0 / 0 / 31) HTML/CSV :exclamation: (5 / 1 / 10) HTML/CSV :question: (0 / 0 / 31) HTML/CSV
SV-COMP25_no-overflow :question: (0 / 0 / 4) HTML/CSV :question: (0 / 0 / 4) HTML/CSV :question: (0 / 0 / 4) HTML/CSV
SV-COMP25_termination :white_check_mark: (2 / 0 / 8) HTML/CSV :white_check_mark: (1 / 0 / 9) HTML/CSV :white_check_mark: (2 / 0 / 10) HTML/CSV
SV-COMP25_unreach-call :white_check_mark: (9 / 0 / 226) HTML/CSV :exclamation: (14 / 3 / 144) HTML/CSV :exclamation: (17 / 1 / 239) HTML/CSV
SV-COMP25_valid-memcleanup :question: (0 / 0 / 31) HTML/CSV :question: (0 / 0 / 34) HTML/CSV :question: (0 / 0 / 33) HTML/CSV
SV-COMP25_valid-memsafety :question: (0 / 0 / 172) HTML/CSV :white_check_mark: (16 / 0 / 109) HTML/CSV :question: (0 / 0 / 161) HTML/CSV