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 deadline | July 15, 2016 |
| Notification | August 11, 2016 |
| Final version | August 31, 2016 |
| Workshop date | September 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:
- Decision procedures and their embedding into SMT solvers and computer algebra systems
- Satisfiability Checking for Symbolic Computation
- Symbolic Computation for Satisfiability Checking
- Applications relying on both Symbolic Computation and Satisfiability Checking
- Combination of Symbolic Computation and Satisfiability Checking tools
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:
- Regular papers, describing research not published or submitted elsewhere. These papers will be thoroughly reviewed by the Program Committee, and included in the local proceedings distributed at the event. The authors can opt in for the selection process to appear as well in the IEEE post-proceedings of SYNASC.
- Extended abstracts, which are either position papers, description of research prospects, challenges, projects, ongoing works, or applications relevant to SC-square. They will be peer-reviewed and will be included in the local proceedings.
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
- Erika Ábrahám (RWTH Aachen University, Germany)
- Pascal Fontaine (Université de Lorraine, Inria, Loria, Nancy, France)
Program Committee
- John Abbott (Universität Kassel, Germany)
- Bernd Becker (Albert-Ludwigs-Universität, Freiburg, Germany)
- Anna M. Bigatti (Universita degli studi di Genova, Italy)
- Martin Brain (University of Oxford, U.K.)
- Bruno Buchberger (Johannes Kepler Universität, Linz, Austria)
- Changbo Chen (Chinese Academy of Sciences, China)
- James H. Davenport (University of Bath, U.K.)
- Matthew England (Coventry University, U.K.)
- Stephen Forrest (Maplesoft Europe Ltd)
- Vijay Ganesh (University of Waterloo, Canada)
- Alberto Griggio (Fondazione Bruno Kessler, Trento, Italy)
- Daniel Kroening (University of Oxford, U.K.)
- Werner Seiler (Universität Kassel, Germany)
- Thomas Sturm (CNRS, Nancy, France and MPI Informatik, Germany)
- Cesare Tinelli (The University of Iowa, USA)
- Ashish Tiwari (SRI, Menlo Park, CA, USA)