A solver for arrays with concatenation

DOI10.1007/s10817-022-09654-yOpenAlexW4313680408MaRDI QIDQ6156632

Andrew W. Appel, Qinshi Wang

Publication date: 14 June 2023

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-022-09654-y

zbMATH Keywords

program verificationdecision procedureproof automationcorrectness proofarray theory

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Unnamed Item
• Unnamed Item
• Z3str2: an efficient solver for strings, regular expressions, and length constraints
• VST-Floyd: a separation logic tool to verify correctness of C programs
• String solving with word equations and transducers: towards a logic for analysing mutation XSS
• An efficient algorithm for solving word equations
• Verified Software Toolchain
• Dafny: An Automatic Program Verifier for Functional Correctness
• Modular SMT Proofs for Fast Reflexive Checking Inside Coq
• Satisfiability Modulo Theories
• Chain-Free String Constraints
• Satisfiability of word equations with constants is in PSPACE
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Array Folds Logic
• What Else Is Decidable about Integer Arrays?
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: A solver for arrays with concatenation