Formally verified suffix array construction

DOI10.1007/S10817-025-09735-8MaRDI QIDQ6912398zbMATH OpenFDO

Authors Louis Cheung, Alistair Moffat, Christine Rizkallah

Publication date 22 October 2025

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

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S10817-025-09735-8

zbMATH Keywords

data structuresformal verificationIsabelle/HOLSA-IS algorithmsuffix array

Mathematics Subject Classification ID

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

Cites work

• A fast string searching algorithm
• A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
• Algorithms on Strings
• An efficient, versatile approach to suffix sorting
• Bridging the Gap: Automatic Verified Abstraction of C
• Code generation via higher-order rewrite systems
• Concrete semantics. With Isabelle/HOL
• Edinburgh LCF. A mechanized logic of computation
• Efficient Verified Implementation of Introsort and Pdqsort
• Fast Pattern Matching in Strings
• Faster suffix sorting
• Grammar Compression by Induced Suffix Sorting
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 3551946 (Why is no real title available?)
• scientific article; zbMATH DE number 1952947 (Why is no real title available?)
• scientific article; zbMATH DE number 2038766 (Why is no real title available?)
• scientific article; zbMATH DE number 1786458 (Why is no real title available?)
• scientific article; zbMATH DE number 1420787 (Why is no real title available?)
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)
• Indexing compressed text
• Isabelle/HOL. A proof assistant for higher-order logic
• Optimal in-place suffix sorting
• Refinement through restraint: bringing down the cost of verification
• Refinement to imperative HOL
• Replacing suffix trees with enhanced suffix arrays
• Space efficient linear time construction of suffix arrays
• Suffix Arrays: A New Method for On-Line String Searches
• Two Efficient Algorithms for Linear Time Suffix Array Construction
• Verified Textbook Algorithms
• Verifying asymptotic time complexity of imperative programs in Isabelle

This page was built for publication: Formally verified suffix array construction

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