Benchmark results for JavaSMT code-generator and parser-interpreter for SMT-LIB2
收藏资源简介:
The new integration of a code-generator and parser-interpreter for SMT-LIB2 into JavaSMT [1] was benchmark tested with CPAchecker [2], the Benchexec framework [3] using the included run definition 'princess_run.xml' and SV-Benchmarks [4]. The results are available in 'results.2023-11-28_17-09-38.table.csv' and 'results.2023-11-28_17-09-38.table.csv'. The log files for each individual task can be found in results.zip. [1] github.com/sosy-lab/java-smt/pull/343 [2] svn.sosy-lab.org/software/cpachecker/branches/javasmt-smtlib2-generator-parser/ [3] github.com/sosy-lab/benchexec/releases/tag/3.20 [4] gitlab.com/sosy-lab/benchmarking/sv-benchmarks, commit 509aa682
将面向SMT-LIB2的代码生成器与解析解释器集成至JavaSMT[1]的新增方案,已借助CPAchecker[2]、Benchexec基准测试框架[3](采用内置运行定义文件'princess_run.xml')与SV-Benchmarks[4]完成基准测试。测试结果可从'results.2023-11-28_17-09-38.table.csv'与'results.2023-11-28_17-09-38.table.csv'中获取。各单任务的日志文件可于results.zip中获取。 [1] github.com/sosy-lab/java-smt/pull/343 [2] svn.sosy-lab.org/software/cpachecker/branches/javasmt-smtlib2-generator-parser/ [3] github.com/sosy-lab/benchexec/releases/tag/3.20 [4] gitlab.com/sosy-lab/benchmarking/sv-benchmarks, commit 509aa682



