Path Feasibility Analysis for String-Manipulating Programs

DOI10.1007/978-3-642-00768-2_27zbMath1234.68070OpenAlexW2117402063MaRDI QIDQ3617764

Andrei Voronkov, Nikolaj Bjørner, Nikolai Tillmann

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) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Algorithms on strings (68W32)

Related Items (20)

An SMT solver for regular expressions and linear arithmetic over string length ⋮ Word equations in the context of string solving ⋮ Reasoning about vectors: satisfiability modulo a theory of sequences ⋮ Towards more efficient methods for solving regular-expression heavy string constraints ⋮ Word equations in synergy with regular constraints ⋮ A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings ⋮ Verified verifying: SMT-LIB for strings in Isabelle ⋮ Unnamed Item ⋮ Simple linear string constraints ⋮ On theorem prover-based testing ⋮ An efficient SMT solver for string constraints ⋮ Automata-based symbolic string analysis for vulnerability detection ⋮ Z3str2: an efficient solver for strings, regular expressions, and length constraints ⋮ Design and implementation of bounded-length sequence variables ⋮ A Slice-Based Decision Procedure for Type-Based Partial Orders ⋮ Relational String Verification Using Multi-track Automata ⋮ An Evaluation of Automata Algorithms for String Analysis ⋮ Dashed strings for string constraint solving ⋮ A decision procedure for string to code point conversion ⋮ Reasoning about vectors using an SMT theory of sequences

Uses Software

• CUTE
• DART
• Pex
• jCUTE
• STP

Cites Work

• Unnamed Item
• Definability in the Existential Theory of Concatenation and Undecidable Extensions of this Theory
• Symbolic execution and program testing
• Automatic Structures: Richness and Limitations
• What Else Is Decidable about Integer Arrays?
• Verification, Model Checking, and Abstract Interpretation

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