[ADD] Tools from FMCAD25 #49

New Issue

mossbiscuits · 2025-10-10T17:20:21Z

mossbiscuits commented

2025-10-10 17:20:21 +00:00

At least these:

11:20
Mitja Kulczynski, Kevin Lotz and Dirk Nowotka
s2s: An Eager SMT Solver for Strings

ABSTRACT. String constraint solving describes the problem of determining the satisfiability of first-order formulas where variables range over strings. Automated procedures for solving these problems are known as string solvers. Most existing solvers adopt a lazy SMT approach, where a SAT solver handles the Boolean structure of the formula and alternates with a specialized string reasoning engine, following the CDCL(T) paradigm. An alternative strategy, called eager SMT solving, reduces the entire problem to Boolean satisfiability, allowing it to be handled directly by a SAT solver. While successful eager approaches have been proposed, current implementations either lack expressiveness or are not publicly available. Here, we present a new eager string solver based on existing techniques, capable of solving Boolean combinations of word equations, regular constraints, and linear arithmetic over string lengths. An evaluation on the SMT-LIB string benchmarks shows that our approach is competitive on a broad set of problems compared to state-of-the-art solvers, and even outperforms them in many cases. In particular, our solver demonstrates near best-in-class performance on the SMT-COMP pure string benchmarks.
11:40
Alexis Aurandt, Kristin Yvonne Rozier and Phillip H. Jones
R2U2 Playground: Visualization of a Real-time, Temporal Logic Runtime Monitor
PRESENTER: Alexis Aurandt

ABSTRACT. The Realizable, Responsive, Unobtrusive Unit (R2U2) is a real-time, temporal logic-based runtime monitoring engine that has been successfully deployed on-board a wide range of cyber-physical systems, from aircraft to spacecraft to robots, checking in real time whether these systems uphold specified system requirements. However, the efficacy of deploying runtime monitors is highly sensitive to their correct configuration. Moreover, there are many barriers to adopting runtime monitors, including a high learning curve and the challenge of eliciting formal specifications that accurately capture system requirements. Therefore, we present the R2U2 Playground, an interactive web-based playground that provides visualization of R2U2. The R2U2 Playground provides stepwise execution coupled with reactive timeline plotting and visualization of its internal abstract syntax tree architecture. To this extent, the R2U2 Playground provides insight into how R2U2 evaluates specifications, allowing for easier specification understanding and debugging.
12:00
Alexander Konrad and Christoph Scholl
FastPoly: An Efficient Polynomial Package for the Verification of Integer Arithmetic Circuits
PRESENTER: Alexander Konrad

ABSTRACT. In recent years, methods based on Symbolic Computer Algebra (SCA) have become increasingly successful in the field of formal verification of arithmetic circuits. While several different approaches have been proposed to tackle this challenging task, most of them are based on the same mathematical operations. They perform ideal membership tests that reduce specification polynomials by a series of polynomial divisions. For integer arithmetic, under certain conditions, the polynomial divisions boil down to substitutions of variables in integer polynomials. In this context, the overall performance of an SCA verification tool is closely related to the efficiency of the steps manipulating integer polynomials. In this paper we present our tool FastPoly, a package for representing integer polynomials that provides efficient operations including variable substitution with integrated normalization steps. We provide the sources of our tool, making it available for other research groups to support future progress in this field.
12:20
Oliver Markgraf, Anthony W. Lin, Matthew Hague, Philipp Rümmer, Zhilin Wu, Denghang Hu and Artur Jeż
OSTRICH: Solver for Complex String Constraints

ABSTRACT. We present OSTRICH2, the latest evolution of the SMT solver OSTRICH for string constraints. OSTRICH2 supports a wide range of complex functions on strings and provides completeness guarantees for a substantial fragment of string constraints, including the straight-line fragment and the chain-free fragment. OSTRICH2 provides full support for the SMT-LIB theory of Unicode strings, extending the standard with several unique features not found in other solvers: among others, parsing of ECMAScript regular expressions (including look‐around assertions and capture groups) and handling of user‐defined string transducers. We empirically demonstrate that OSTRICH2 is competitive to other string solvers on SMT-COMP benchmarks.

From https://easychair.org/smart-program/FMCAD2025/2025-10-10.html

At least these: 11:20 Mitja Kulczynski, Kevin Lotz and Dirk Nowotka s2s: An Eager SMT Solver for Strings ABSTRACT. String constraint solving describes the problem of determining the satisfiability of first-order formulas where variables range over strings. Automated procedures for solving these problems are known as string solvers. Most existing solvers adopt a lazy SMT approach, where a SAT solver handles the Boolean structure of the formula and alternates with a specialized string reasoning engine, following the CDCL(T) paradigm. An alternative strategy, called eager SMT solving, reduces the entire problem to Boolean satisfiability, allowing it to be handled directly by a SAT solver. While successful eager approaches have been proposed, current implementations either lack expressiveness or are not publicly available. Here, we present a new eager string solver based on existing techniques, capable of solving Boolean combinations of word equations, regular constraints, and linear arithmetic over string lengths. An evaluation on the SMT-LIB string benchmarks shows that our approach is competitive on a broad set of problems compared to state-of-the-art solvers, and even outperforms them in many cases. In particular, our solver demonstrates near best-in-class performance on the SMT-COMP pure string benchmarks. 11:40 Alexis Aurandt, Kristin Yvonne Rozier and Phillip H. Jones R2U2 Playground: Visualization of a Real-time, Temporal Logic Runtime Monitor PRESENTER: Alexis Aurandt ABSTRACT. The Realizable, Responsive, Unobtrusive Unit (R2U2) is a real-time, temporal logic-based runtime monitoring engine that has been successfully deployed on-board a wide range of cyber-physical systems, from aircraft to spacecraft to robots, checking in real time whether these systems uphold specified system requirements. However, the efficacy of deploying runtime monitors is highly sensitive to their correct configuration. Moreover, there are many barriers to adopting runtime monitors, including a high learning curve and the challenge of eliciting formal specifications that accurately capture system requirements. Therefore, we present the R2U2 Playground, an interactive web-based playground that provides visualization of R2U2. The R2U2 Playground provides stepwise execution coupled with reactive timeline plotting and visualization of its internal abstract syntax tree architecture. To this extent, the R2U2 Playground provides insight into how R2U2 evaluates specifications, allowing for easier specification understanding and debugging. 12:00 Alexander Konrad and Christoph Scholl FastPoly: An Efficient Polynomial Package for the Verification of Integer Arithmetic Circuits PRESENTER: Alexander Konrad ABSTRACT. In recent years, methods based on Symbolic Computer Algebra (SCA) have become increasingly successful in the field of formal verification of arithmetic circuits. While several different approaches have been proposed to tackle this challenging task, most of them are based on the same mathematical operations. They perform ideal membership tests that reduce specification polynomials by a series of polynomial divisions. For integer arithmetic, under certain conditions, the polynomial divisions boil down to substitutions of variables in integer polynomials. In this context, the overall performance of an SCA verification tool is closely related to the efficiency of the steps manipulating integer polynomials. In this paper we present our tool FastPoly, a package for representing integer polynomials that provides efficient operations including variable substitution with integrated normalization steps. We provide the sources of our tool, making it available for other research groups to support future progress in this field. 12:20 Oliver Markgraf, Anthony W. Lin, Matthew Hague, Philipp Rümmer, Zhilin Wu, Denghang Hu and Artur Jeż OSTRICH: Solver for Complex String Constraints ABSTRACT. We present OSTRICH2, the latest evolution of the SMT solver OSTRICH for string constraints. OSTRICH2 supports a wide range of complex functions on strings and provides completeness guarantees for a substantial fragment of string constraints, including the straight-line fragment and the chain-free fragment. OSTRICH2 provides full support for the SMT-LIB theory of Unicode strings, extending the standard with several unique features not found in other solvers: among others, parsing of ECMAScript regular expressions (including look‐around assertions and capture groups) and handling of user‐defined string transducers. We empirically demonstrate that OSTRICH2 is competitive to other string solvers on SMT-COMP benchmarks. From https://easychair.org/smart-program/FMCAD2025/2025-10-10.html

mossbiscuits added the

enhancement

new tool

labels 2025-10-10 17:20:21 +00:00

mossbiscuits self-assigned this 2025-10-10 17:20:21 +00:00

Sign in to join this conversation.

1 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: fmtools/content#49