Timisoara - Union Square at sunrise

The First International Workshop on Satisfiability Checking and Symbolic Computation will be held on 24th September, 2016 in Timisoara, Romania. It is affiliated to the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2016.

Important dates

Submission deadlineJuly 15, 2016
NotificationAugust 11, 2016
Final versionAugust 31, 2016
Workshop dateSeptember 24, 2016

Call for papers

The call for papers is available here.

Scope

Symbolic Computation is concerned with the algorithmic determination of exact solutions to complex mathematical problems; more recent developments in the area of Satisfiability Checking are starting to tackle similar problems but with different algorithmic and technological solutions. The two communities share many central interests, but researchers from these two communities rarely interact. Also, the lack of common or compatible interfaces of tools is an obstacle to their fruitful combination. Bridges between the communities in the form of common platforms and road-maps are necessary to initiate an exchange, and to support and direct their interaction. The aim of this workshop, along the SC-square H2020 FETOPEN Coordination and Support Activity project, is to provide a time to discuss, share knowledge and experience across both communities.

The workshop is open for submission and participation to everyone interested in the topics, whether they are members or associates of the SC-square H2020 FETOPEN CSA project or not.

The topics of interest include but are not limited to:

Submission information

Submissions should be written in English, formatted according to the IEEE guidelines, and submitted via EasyChair. We invite two kinds of submissions, both having an upper page limit of 8 pages:

People from industries and businesses are warmly invited to submit papers to describe their problems, challenges, goals, and expectations for the SC-square community.

Proceedings

The authors of the papers presented at this workshop could opt in for CEUR proceedings. The proceedings of the workshop are available as Volume 1804 of CEUR.

Program

Keynote Speaker: Christopher W. Brown (United States Naval Academy, USA)

Friday, September 23

20:00 - Board Dinner
Hotel Perla 4 Restaurant: Protopop George Dragomir, nr. 9, 300233 Timişoara

Saturday, September 24

9:00 - 09:20 SYNASC opening
9:20 - 10:10
SC2 + SYNASC keynote

Chair:
J. H. Davenport
Christopher W. Brown (United States Naval Academy, USA)
Real polynomial constraints: satisfiability checking brings a new perspective to symbolic computing
 
10:10 - 10:30 Coffee break
 
10:30 - 12:00
DECISION PROCEDURES

Chair:
C. Brown
Matthew England and James H. Davenport (10:30-11:00)
Experience with Heuristics, Benchmarks & Standards for Cylindrical Algebraic Decomposition

John Abbott and Anna Maria Bigatti (11:00-11:30)
CoCoA and CoCoALib: Fast Prototyping and Flexible C++ Library for Computations in Commutative Algebra

Jan Horacek, Martin Kreuzer and Ange-Salome Messeng Ekossono (11:30-12:00)
Computing Boolean Border Bases
 
12:00 - 13:30 Lunch break
 
13:30 - 14:20 SYNASC program
 
14:20 - 14:40 Coffee break
 
14:40 - 16:10
APPLICATIONS

Chair:
M. England
Alessandro Cimatti, Ahmed Irfan, Alberto Griggio, Marco Roveri and Roberto Sebastiani (14:40-15:10)
A CEGAR-based approach for proving invariant properties of Transition Systems on Non-Linear Real Arithmetic

Curtis Bright, Vijay Ganesh, Albert Heinle, Ilias Kotsireas, Saeed Nejati and Krzysztof Czarnecki (15:10-15:40)
MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures

Felix Neubauer, Karsten Scheibler, Bernd Becker, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller and Detlef Fehrer (15:40-16:10)
Accurate Dead Code Detection in Embedded C Code by Arithmetic Constraint Solving
 
16:10 - 16:40 Coffee break
 
16:40 - 18:20
CHALLENGES AND POTENTIALS

Chair:
T. Sturm
Tom Bienmüller and Tino Teige (16:40-17:10)
Satisfaction Meets Practice and Confidence

James H. Davenport (17:10-17:40)
What does ``without loss of generality'' mean (and how do we detect it)

Martin Brain, Daniel Kroening and Ryan McCleeary (17:40-18:10)
Algebraic Techniques in Software Verification : Challenges and Opportunities
 
18:20 - 20:00 SYNASC Welcome reception

Sunday, September 25

Afternoon Board meeting and working sessions
 
18:00 - SYNASC Dinner

Co-chairs

Program Committee