Incremental Linearization: A practical approach to Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions (Invited Paper)

被引：1

作者：

Cimatti, Alessandro ^{[1
]}

Griggio, Alberto ^{[1
]}

Irfan, Ahmed ^{[1
]}

Roveri, Marco ^{[1
]}

Sebastiani, Roberto ^{[2
]}

机构：

[1] Fdn Bruno Kessler FBK, Trento, Italy

[2] Univ Trento, Trento, Italy

来源：

2018 20TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC 2018) | 2019年

关键词：

Automated Reasoning; Linear and Nonlinear Arithmetic; SMT; Transcendental Functions;

D O I：

10.1109/SYNASC.2018.00016

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some theory or combination of theories. In this paper, we overview our recent approach called Incremental Linearization, which successfully tackles the problems of SMT over the theories of nonlinear arithmetic over the reals (NRA), nonlinear arithmetic over the integers (NIA) and their combination, and of NRA augmented with transcendental (exponential and trigonometric) functions (NTA). Moreover, we showcase some of the experimental results and outline interesting future directions.

引用

页码：19 / 26

页数：8

共 9 条

[1] Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
Cimatti, Alessandro
Griggio, Alberto
Irfan, Ahmed
Roveri, Marco
Sebastiani, Roberto
ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2018, 19 (03)
[2] Satisfiability Modulo Transcendental Functions via Incremental Linearization
Cimatti, Alessandro
Griggio, Alberto
Irfan, Ahmed
Roveri, Marco
Sebastiani, Roberto
AUTOMATED DEDUCTION - CADE 26, 2017, 10395 : 95 - 113
[3] Optimization Modulo Non-linear Arithmetic via Incremental Linearization
Bigarella, Filippo
Cimatti, Alessandro
Griggio, Alberto
Irfan, Ahmed
Jonas, Martin
Roveri, Marco
Sebastiani, Roberto
Trentin, Patrick
FRONTIERS OF COMBINING SYSTEMS (FROCOS 2021), 2021, 12941 : 213 - 231
[4] Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
Cimatti, Alessandro
Griggio, Alberto
Irfan, Ahmed
Roveri, Marco
Sebastiani, Roberto
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2018, 2018, 10929 : 383 - 398
[5] Practical Approach in Verification of Security Systems Using Satisfiability Modulo Theories
Zbrzezny, Agnieszka M.
Szymoniak, Sabina
Kurkowski, Miroslaw
LOGIC JOURNAL OF THE IGPL, 2022, 30 (02) : 289 - 300
[6] A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic
Kremer, Gereon
Corzilius, Florian
Abraham, Erika
COMPUTER ALGEBRA IN SCIENTIFIC COMPUTING, CASC 2016, 2016, 9890 : 315 - 335
[7] Coherent Combining with Active Phase Control: A Practical Tool for Adaptive and Nonlinear Optics (Invited paper)
Bourdon, P.
Le Gouet, J.
Goular, D.
Lombard, L.
Durecu, A.
2017 CONFERENCE ON LASERS AND ELECTRO-OPTICS PACIFIC RIM (CLEO-PR), 2017,
[8] Practical stability of nonlinear stochastic hybrid parabolic systems of Ito-type: Vector Lyapunov functions approach
Anabtawi, M. J.
NONLINEAR ANALYSIS-REAL WORLD APPLICATIONS, 2011, 12 (03) : 1386 - 1400
[9] Practical stability of nonlinear stochastic hybrid parabolic systems of Ito-type: Vector Lyapunov functions approach (vol 12, pg 1386, 2011)
不详
NONLINEAR ANALYSIS-REAL WORLD APPLICATIONS, 2023, 73

← 1 →