Program specialization as a tool for solving word equations

DOI10.4204/EPTCS.341.4MaRDI QIDQ6646292zbMATH OpenFDO

Authors Antonina N. Nepeivoda

Publication date 29 November 2024

Full work available at URL https://doi.org/10.4204/EPTCS.341.4

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Combinatorics on words (68R15) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Recommendations

• Solving word equations
• On PSPACE generation of a solution set of a word equation and its applications
• On solving word equations using SAT
• Solving equations on words with morphisms and antimorphisms
• Makanin's algorithm for word equations-two improvements and a generalization

Cites work

• scientific article; zbMATH DE number 1630107 (Why is no real title available?)
• scientific article; zbMATH DE number 1344899 (Why is no real title available?)
• scientific article; zbMATH DE number 236855 (Why is no real title available?)
• scientific article; zbMATH DE number 3336814 (Why is no real title available?)
• scientific article; zbMATH DE number 3355024 (Why is no real title available?)
• A Transformation System for Developing Recursive Programs
• A decision procedure for string logic with quadratic equations, regular expressions and length constraints
• An efficient SMT solver for string constraints
• An efficient algorithm for solving word equations
• Annotation of logic programs for independent AND-parallelism by partial evaluation
• Computational complexity via programming languages: Constant factors do matter
• Control-flow refinement by partial evaluation, and its application to termination and cost analysis
• Efficient and flexible access control via Jones-optimal logic program specialisation
• On solving word equations using SAT
• Partial evaluation of computation process -- an approach to a compiler-compiler
• Path Feasibility Analysis for String-Manipulating Programs
• Ping-pong protocols as prefix grammars: modelling and verification via program transformation
• Progressive reasoning over recursively-defined strings
• Quadratic word equations with length constraints, counter systems, and Presburger arithmetic with divisibility
• REACHABILITY ANALYSIS IN VERIFICATION VIA SUPERCOMPILATION
• Recompression: a simple and powerful technique for word equations
• Relational string verification using multi-track automata
• Solving Horn clauses on inductive data types without induction
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• The concept of a supercompiler
• The hardness of solving simple word equations

This page was built for publication: Program specialization as a tool for solving word equations

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