Chain-free string constraints

DOI10.1007/978-3-030-31784-3_16MaRDI QIDQ3297597zbMATH OpenOpenAlexFDO

Authors Mohamed Faouzi Atig, Bui Phi Diep, Lukáš Holik, Petr Janků, Parosh A. Abdulla

Publication date 20 July 2020

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-030-31784-3_16

zbMATH Keywords

program verificationsatisfiability modulo theoriesstring constraints

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Computational aspects of satisfiability (68R07)

Recommendations

• An efficient SMT solver for string constraints
• A decision procedure for regular membership and length constraints over unbounded strings
• A decision procedure for string logic with quadratic equations, regular expressions and length constraints
• Constraint solving on bounded string variables
• String solving with word equations and transducers: towards a logic for analysing mutation XSS

Cites work

• An efficient algorithm for solving word equations
• Automata, Languages and Programming
• Computation paradigms in light of Hilbert's tenth problem
• Concatenation as a basis for arithmetic
• Definability in the Existential Theory of Concatenation and Undecidable Extensions of this Theory
• Graph logics with rational relations
• scientific article; zbMATH DE number 1304322 (Why is no real title available?)
• scientific article; zbMATH DE number 1512622 (Why is no real title available?)
• Makanin's algorithm for word equations-two improvements and a generalization
• Progressive reasoning over recursively-defined strings
• Satisfiability of word equations with constants is in PSPACE
• Scaling up DPLL(T) string solvers using context-dependent simplification
• String Analysis via Automata Manipulation with Logic Circuit Representation
• String solving with word equations and transducers: towards a logic for analysing mutation XSS
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP

Cited in

(21)

• Propagating \textsc{lex}, \textsc{find} and \textsc{replace} with dashed strings
• A decision procedure for string to code point conversion
• Relational string abstract domains
• Twinning automata and regular expressions for string static analysis
• String solving with word equations and transducers: towards a logic for analysing mutation XSS
• A decision procedure for regular membership and length constraints over unbounded strings
• Path Feasibility Analysis for String-Manipulating Programs
• Simple linear string constraints
• scientific article; zbMATH DE number 7559472 (Why is no real title available?)
• A solver for arrays with concatenation
• A decision procedure for string logic with quadratic equations, regular expressions and length constraints
• Word equations in synergy with regular constraints
• A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type
• Solving Not-Substring Constraint withFlat Abstraction
• Reasoning About Regular Properties: A Comparative Study
• Decision procedures for sequence theories
• On the satisfiability of context-free string constraints with subword-ordering
• Cooking string-integer conversions with noodles
• Satisfiability of context-free string constraints with subword-ordering and transducers
• Word equations in synergy with regular constraints (extended version)
• Negated string containment is decidable

Describes a project that uses

Uses Software

• CVC4
• Stranger
• Norn
• Z3str3
• S3
• z3
• HAMPI
• GitHub

This page was built for publication: Chain-free string constraints

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3297597)