Norn: an SMT solver for string constraints. We present version 1.0 of the Norn SMT solver for string constraints. Norn is a solver for an expressive constraint language, including word equations, length constraints, and regular membership queries. As a feature distinguishing Norn from other SMT solvers, Norn is a decision procedure under the assumption of a set of acyclicity conditions on word equations, without any restrictions on the use of regular membership.
Keywords for this software
References in zbMATH (referenced in 10 articles )
Showing results 1 to 10 of 10.
- Arceri, Vincenzo; Olliaro, Martina; Cortesi, Agostino; Mastroeni, Isabella: Completeness of string analysis for dynamic languages (2021)
- Garreta, Albert; Gray, Robert D.: On equations and first-order theory of one-relator monoids (2021)
- Amadini, Roberto; Gange, Graeme; Stuckey, Peter J.: Dashed strings for string constraint solving (2020)
- Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Diep, Bui Phi; Holík, Lukáš; Janků, Petr: Chain-free string constraints (2019)
- Day, Joel D.; Ganesh, Vijay; He, Paul; Manea, Florin; Nowotka, Dirk: The satisfiability of word equations: decidable and undecidable theories (2018)
- Amadini, Roberto; Flener, Pierre; Pearson, Justin; Scott, Joseph D.; Stuckey, Peter J.; Tack, Guido: Minizinc with strings (2017)
- Berzish, M., Ganesh, V., Zheng, Y.: Z3str3: A String Solver with Theory-aware Branching (2017) arXiv
- Scott, Joseph D.; Flener, Pierre; Pearson, Justin; Schulte, Christian: Design and implementation of bounded-length sequence variables (2017)