On strings in software model checking

DOI10.1007/978-3-030-34175-6_2MaRDI QIDQ6536304zbMATH OpenFDO

Authors Hossein Hojjat, Philipp Rümmer, Ali Shamakhi

Publication date 19 April 2024

Full work available at URL https://doi.org/10.1007/978-3-030-34175-6_2

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• String abstraction for model checking of C programs
• An efficient SMT solver for string constraints
• Path Feasibility Analysis for String-Manipulating Programs
• Model Checking for String Problems
• Automata-based model counting for string constraints

Cites work

• An automaton learning approach to solving safety games over infinite graphs
• Automata-based model counting for string constraints
• Dafny: an automatic program verifier for functional correctness
• Encodings of bounded synthesis
• From invariant checking to invariant inference using randomized search
• Handbook of model checking
• scientific article; zbMATH DE number 2090837 (Why is no real title available?)
• Interpolation and SAT-based model checking.
• Liveness of randomised parameterised systems under arbitrary schedulers
• SMT-based model checking for recursive programs
• Solving Horn clauses on inductive data types without induction
• Symbolic string transformations with regular lookahead and rollback

Cited in

(3)

• String abstraction for model checking of C programs
• Solving string constraints using SAT
• Certainty in formalising SMT-LIB for strings in Isabelle

This page was built for publication: On strings in software model checking

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