SC-Square: When Satisfiability Checking and Symbolic Computation Join Forces

Erika Abraham; John Abbott; Bernd Becker; Anna M. Bigatti; Martin Brain; Alessandro Cimatti; James H. Davenport; Matthew England; Pascal Fontaine; Stephen Forrest; Vijay Ganesh; Alberto Griggio; Daniel Kroening; Werner M. Seiler

doi:10.29007/p319

SC-Square: When Satisfiability Checking and Symbolic Computation Join Forces

Erika Abraham, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Vijay Ganesh, Alberto Griggio, Daniel Kroening, Werner M. Seiler

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

Abstract

Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but with common interests, e.g., in the development, implementation and application of decision procedures for arithmetic theories. Despite their commonalities, the two communities are rather weakly connected. The aim of the SC-Square initiative is to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap from theory along the way to tools and (industrial) applications.

Original language	English
Title of host publication	ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements
Editors	Giles Reger, Dmitriy Traytel
Publisher	EasyChair
Pages	6-10
Number of pages	5
Volume	51
DOIs	https://doi.org/10.29007/p319
Publication status	Published - 8 Nov 2017
Event	Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements - Gothenburg, Sweden Duration: 6 Aug 2017 → 6 Aug 2017 Conference number: 1 http://www.cs.man.ac.uk/~regerg/arcade/

Workshop

Workshop	Automated Reasoning
Abbreviated title	ARCADE
Country/Territory	Sweden
City	Gothenburg
Period	6/08/17 → 6/08/17
Internet address	http://www.cs.man.ac.uk/~regerg/arcade/

Keywords

automated reasoning
computer algebra
satisfiability checking
symbolic computation

Access to Document

10.29007/p319

Cite this

Abraham, E., Abbott, J., Becker, B., Bigatti, A. M., Brain, M., Cimatti, A., Davenport, J. H., England, M., Fontaine, P., Forrest, S., Ganesh, V., Griggio, A., Kroening, D., & Seiler, W. M. (2017). SC-Square: When Satisfiability Checking and Symbolic Computation Join Forces. In G. Reger, & D. Traytel (Eds.), ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (Vol. 51, pp. 6-10). EasyChair. https://doi.org/10.29007/p319

SC-Square: When Satisfiability Checking and Symbolic Computation Join Forces. / Abraham, Erika; Abbott, John; Becker, Bernd et al.

ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements. ed. / Giles Reger; Dmitriy Traytel. Vol. 51 EasyChair, 2017. p. 6-10.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

Abraham, E, Abbott, J, Becker, B, Bigatti, AM, Brain, M, Cimatti, A, Davenport, JH, England, M, Fontaine, P, Forrest, S, Ganesh, V, Griggio, A, Kroening, D & Seiler, WM 2017, SC-Square: When Satisfiability Checking and Symbolic Computation Join Forces. in G Reger & D Traytel (eds), ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements. vol. 51, EasyChair, pp. 6-10, Automated Reasoning, Gothenburg, Sweden, 6/08/17. https://doi.org/10.29007/p319

@inproceedings{cf898d9731e149a0a2b0c6fafe85772a,

title = "SC-Square: When Satisfiability Checking and Symbolic Computation Join Forces",

abstract = "Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but with common interests, e.g., in the development, implementation and application of decision procedures for arithmetic theories. Despite their commonalities, the two communities are rather weakly connected. The aim of the SC-Square initiative is to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap from theory along the way to tools and (industrial) applications.",

keywords = "automated reasoning, computer algebra, satisfiability checking, symbolic computation",

author = "Erika Abraham and John Abbott and Bernd Becker and Bigatti, {Anna M.} and Martin Brain and Alessandro Cimatti and Davenport, {James H.} and Matthew England and Pascal Fontaine and Stephen Forrest and Vijay Ganesh and Alberto Griggio and Daniel Kroening and Seiler, {Werner M.}",

year = "2017",

month = nov,

day = "8",

doi = "10.29007/p319",

language = "English",

volume = "51",

pages = "6--10",

editor = "Giles Reger and Dmitriy Traytel",

booktitle = "ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements",

publisher = "EasyChair",

address = "United Kingdom",

note = "Automated Reasoning : Challenges, Applications, Directions, Exemplary Achievements, ARCADE ; Conference date: 06-08-2017 Through 06-08-2017",

url = "http://www.cs.man.ac.uk/~regerg/arcade/",

}

TY - GEN

T1 - SC-Square: When Satisfiability Checking and Symbolic Computation Join Forces

AU - Abraham, Erika

AU - Abbott, John

AU - Becker, Bernd

AU - Bigatti, Anna M.

AU - Brain, Martin

AU - Cimatti, Alessandro

AU - Davenport, James H.

AU - England, Matthew

AU - Fontaine, Pascal

AU - Forrest, Stephen

AU - Ganesh, Vijay

AU - Griggio, Alberto

AU - Kroening, Daniel

AU - Seiler, Werner M.

N1 - Conference code: 1

PY - 2017/11/8

Y1 - 2017/11/8

N2 - Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but with common interests, e.g., in the development, implementation and application of decision procedures for arithmetic theories. Despite their commonalities, the two communities are rather weakly connected. The aim of the SC-Square initiative is to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap from theory along the way to tools and (industrial) applications.

AB - Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but with common interests, e.g., in the development, implementation and application of decision procedures for arithmetic theories. Despite their commonalities, the two communities are rather weakly connected. The aim of the SC-Square initiative is to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap from theory along the way to tools and (industrial) applications.

KW - automated reasoning

KW - computer algebra

KW - satisfiability checking

KW - symbolic computation

UR - http://www.cs.man.ac.uk/~regerg/arcade/

U2 - 10.29007/p319

DO - 10.29007/p319

M3 - Conference proceeding

VL - 51

SP - 6

EP - 10

BT - ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements

A2 - Reger, Giles

A2 - Traytel, Dmitriy

PB - EasyChair

T2 - Automated Reasoning

Y2 - 6 August 2017 through 6 August 2017

ER -

SC-Square: When Satisfiability Checking and Symbolic Computation Join Forces

Abstract

Workshop

Keywords

Access to Document

Other files and links

Fingerprint

Cite this