Path Feasibility Analysis for String-Manipulating Programs

DOI10.1007/978-3-642-00768-2_27MaRDI QIDQ3617764zbMATH OpenOpenAlexFDO

Authors Nikolaj Bjørner, Nikolai Tillmann, Andrei Voronkov

Publication date 31 March 2009

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-00768-2_27

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Algorithms on strings (68W32)

Recommendations

• A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type
• An efficient SMT solver for string constraints
• Z3str2: an efficient solver for strings, regular expressions, and length constraints
• Chain-free string constraints
• Constraint solving on bounded string variables

Cites work

• scientific article; zbMATH DE number 2090837 (Why is no real title available?)
• Automatic Structures: Richness and Limitations
• Definability in the Existential Theory of Concatenation and Undecidable Extensions of this Theory
• Symbolic execution and program testing
• Verification, Model Checking, and Abstract Interpretation
• What Else Is Decidable about Integer Arrays?

Cited in

(26)

• Reasoning about vectors using an SMT theory of sequences
• An SMT solver for regular expressions and linear arithmetic over string length
• An Evaluation of Automata Algorithms for String Analysis
• A decision procedure for regular membership and length constraints over unbounded strings
• Design and implementation of bounded-length sequence variables
• Quadratic word equations with length constraints, counter systems, and Presburger arithmetic with divisibility
• Reasoning about vectors: satisfiability modulo a theory of sequences
• Word equations in synergy with regular constraints
• Towards more efficient methods for solving regular-expression heavy string constraints
• Simple linear string constraints
• On theorem prover-based testing
• Word equations in the context of string solving
• Verified verifying: SMT-LIB for strings in Isabelle
• Certainty in formalising SMT-LIB for strings in Isabelle
• Relational string verification using multi-track automata
• Z3str2: an efficient solver for strings, regular expressions, and length constraints
• Automata-based symbolic string analysis for vulnerability detection
• Program specialization as a tool for solving word equations
• On the decidability and expressive power of several theories based on string constraints
• Even Faster Conflicts and Lazier Reductions for String Solvers
• A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type
• Dashed strings for string constraint solving
• On strings in software model checking
• An efficient SMT solver for string constraints
• A decision procedure for string to code point conversion
• A slice-based decision procedure for type-based partial orders

Describes a project that uses

Uses Software

• STP
• jCUTE
• Pex
• DART
• CUTE

This page was built for publication: Path Feasibility Analysis for String-Manipulating Programs

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