Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
收藏NIAID Data Ecosystem2026-03-11 收录
下载链接：
https://zenodo.org/record/1300852
下载链接
链接失效反馈官方服务：
资源简介：
The tarball contains Satisfiability Modulo Theories (SMT) and Verification Modulo Theories (VMT) benchmarks for the theories of Nonlinear Real Arithmetic (NRA) and NRA extended with Transcendental Functions (NTA). These benchmarks have been collected in the following works:
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani. "Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF". In proc. Tools and Algorithms for the Construction and Analysis of Systems, TACAS'17, 2017.
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani. "Satisfiability Modulo Transcendental Functions via Incremental Linearization". In proc. Int. Conference on Automated Deduction, CADE, 2017.
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani. "Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions". ACM Transactions on Computational Logics. 2018. To appear.
创建时间：
2020-01-24
