Satisfiability Checking and Symbolic Computation

被引：2

作者：

Abraham, E. ^{[1
]}

Abbott, J. ^{[11
]}

Becker, B. ^{[2
]}

Bigatti, A. M. ^{[3
]}

Brain, M. ^{[10
]}

Buchberger, B. ^{[4
]}

Cimatti, A. ^{[5
]}

Davenport, J. H. ^{[6
]}

England, M. ^{[7
]}

Fontaine, P. ^{[8
]}

Forrest, S. ^{[9
]}

Griggio, A. ^{[5
]}

Kroening, D. ^{[10
]}

Seiler, W. M. ^{[11
]}

Sturm, T. ^{[12
,13
]}

机构：

[1] Rhein Westfal TH Aachen, Aachen, Germany

[2] Albert Ludwigs Univ, Freiburg, Germany

[3] Univ Genoa, Genoa, Italy

[4] Johannes Kepler Univ Linz, Linz, Austria

[5] Fdn Bruno Kessler, Trento, Italy

[6] Univ Bath, Bath, Avon, England

[7] Coventry Univ, Coventry, W Midlands, England

[8] Univ Lorraine, Inria, LORIA, Nancy, France

[9] Maplesoft Europe Ltd, Cambridge, England

[10] Univ Oxford, Oxford, England

[11] Univ Kassel, Kassel, Germany

[12] LORIA, CNRS, Nancy, France

[13] Max Planck Inst Informat, Saarbrucken, Germany

来源：

ACM COMMUNICATIONS IN COMPUTER ALGEBRA | 2016年 / 50卷 / 04期

基金：

欧盟地平线“2020”;

关键词：

D O I：

10.1145/3055282.3055285

中图分类号：

O29 [应用数学];

学科分类号：

070104 ;

摘要：

Symbolic Computation and Satisfiability Checking are viewed as individual research areas, but they share common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite these commonalities, the two communities are currently only weakly connected. We introduce a new project SC2 to build a joint community in this area, supported by a newly accepted EU (H2020-FETOPEN-CSA) project of the same name. We aim to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap. This abstract and accompanying poster describes the motivation and aims for the project, and reports on the first activities.

引用

页码：145 / 147

页数：3

共 50 条

[1] Symbolic computation and satisfiability checking
Davenport, James H.
England, Matthew
Griggio, Alberto
Sturm, Thomas
Tinelli, Cesare
JOURNAL OF SYMBOLIC COMPUTATION, 2020, 100 : 1 - 10
[2] Symbolic Computation Techniques in Satisfiability Checking
Abraham, Erika
PROCEEDINGS OF 2016 18TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC), 2016, : 3 - 10
[3] Building Bridges between Symbolic Computation and Satisfiability Checking
Abraham, Erika
PROCEEDINGS OF THE 2015 ACM ON INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION (ISSAC'15), 2015, : 1 - 6
[4] SC2: Satisfiability Checking Meets Symbolic Computation (Project Paper)
Abraham, Erika
Abbott, John
Becker, Bernd
Bigatti, Anna M.
Brain, Martin
Buchberger, Bruno
Cimatti, Alessandro
Davenport, James H.
England, Matthew
Fontaine, Pascal
Forrest, Stephen
Griggio, Alberto
Kroening, Daniel
Seiler, Werner M.
Sturm, Thomas
INTELLIGENT COMPUTER MATHEMATICS, 2016, 9791 : 28 - 43
[5] Graded-CTL: Satisfiability and Symbolic Model Checking
Ferrante, Alessandro
Napoli, Margherita
Parente, Mimmo
FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2009, 5885 : 306 - +
[6] When Satisfiability Solving Meets Symbolic Computation
Bright, Curtis
Kotsireas, Ilias
Ganesh, Vijay
COMMUNICATIONS OF THE ACM, 2022, 65 (07) : 64 - 72
[7] Proceedings of SC-Square 2021: The 6th International Workshop on Satisfiability Checking and Symbolic Computation
Bright, Curtis
Davenport, James
CEUR Workshop Proceedings, 2022, 3273
[8] Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure
Li B.
Wang C.
Somenzi F.
International Journal on Software Tools for Technology Transfer, 2005, 7 (2) : 143 - 155
[9] LTL satisfiability checking
Rozier, Kristin Y.
Vardi, Moshe Y.
MODEL CHECKING SOFTWARE, PROCEEDINGS, 2007, 4595 : 149 - +
[10] LTL satisfiability checking
Rozier K.Y.
Vardi M.Y.
International Journal on Software Tools for Technology Transfer, 2010, 12 (02) : 123 - 137

← 1 2 3 4 5 →