@inproceedings{RISC6348,
author = {Antonio Jiménez-Pastor and Philipp Nuspl and Veronika Pillwein},
title = {{On C2-Finite Sequences}},
booktitle = {{Proceedings of the 2021 on International Symposium on Symbolic and Algebraic Computation}},
language = {english},
abstract = {Holonomic sequences are widely studied as many objects interesting to mathematiciansand computer scientists are in this class. In the univariate case, these are the sequencessatisfying linear recurrences with polynomial coefficients and also referred to asD-finite sequences. A subclass are C-finite sequences satisfying a linear recurrencewith constant coefficients.We investigate the set of sequences which satisfy linearrecurrence equations with coefficients that are C-finite sequences. These sequencesare a natural generalization of holonomic sequences. In this paper, we show that C2-finitesequences form a difference ring and provide methods to compute in this ring.},
series = {ISSAC '21},
pages = {217--224},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
isbn_issn = {ISBN 9781450383820},
year = {2021},
editor = {Frédéric Chyzak and George Labahn},
refereed = {yes},
keywords = {holonomic sequences, algorithms, closure properties, difference equations},
length = {8},
url = {https://doi.org/10.1145/3452143.3465529}
}

@inproceedings{RISC6361,
author = {Wolfgang Schreiner and Franz-Xaver Reichl},
title = {{First-Order Logic in Finite Domains: Where Semantic Evaluation Competes with SMT Solving}},
booktitle = {{Proceedings of the 9th International Symposium on Symbolic Computation in Software Science (SCSS 2021), Hagenberg, Austria, September 8-10, 2021}},
language = {english},
abstract = {In this paper, we compare two alternative mechanisms for deciding the validity of first-order formulas over finite domains supported by the mathematical model checker RISCAL: first, the original approach of semantic evaluation (based on an implementation of the denotational semantics of the RISCAL language) and, second, the later approach of SMT solving (based on satisfiability preserving translations of RISCAL formulas to SMT-LIB formulas as inputs for SMT solvers). After a short presentation of the two approaches and a discussion of their fundamental pros and cons, we quantitatively evaluate them, both by a set of artificial benchmarks and by a set of benchmarks taken from real-life applications of RISCAL; for this, we apply the state-of-the-art SMT solvers Boolector, CVC4, Yices, and Z3. Our benchmarks demonstrate that (while SMT solving generally vastly outperforms semantic evaluation), the various SMT solvers exhibit great performance differences. More important, we identify classes of formulas where semantic evaluation is able to compete with (or even outperform) satisfiability solving, outlining some room for improvements in the translation of RISCAL formulas to SMT-LIB formulas as well as in the current SMT technology.},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {342},
pages = {99--113},
isbn_issn = {ISSN 2075-2180},
year = {2021},
month = {September},
editor = {Temur Kutsia},
refereed = {yes},
keywords = {model checking, SMT solving, first-order logic, automated reasoning, formal methods},
sponsor = {e JKU Linz LIT Project LOGTECHEDU, Aktion Österreich-Slowakei Project 2019-10-15-003, Austrian Science Fund (FWF) grant W1255},
length = {15},
url = {https://doi.org/10.4204/EPTCS.342.9}
}