SMT-LIB Sequences and Regular Expressions

11 pages•Published: August 19, 2013

Nikolaj Bjorner, Vijay Ganesh, Raphaël Michel and Margus Veanes

Abstract

Strings are ubiquitous in software. Tools for specification,
verification and test-case generation of software rely in various degrees on
representing and reasoning about strings. Reasoning about strings is
particularly important in several security critical applications, such as
web sanitizers. Besides a basic representation of strings, applications
also use string recognizers and transducers.
This paper presents a proposal for an SMT-LIBization of strings and regular
expressions. It introduces a theory of sequences, generalizing strings,
and builds a theory of regular experssions on top of sequences.
The logic QF_BVRE is designed to capture a common substrate among
existing tools for string constraint solving.

Keyphrases: regular expressions, smt, smt lib, strings, theories

In: Pascal Fontaine and Amit Goel (editors). SMT 2012. 10th International Workshop on Satisfiability Modulo Theories, vol 20, pages 77-87.

Links:	https://easychair.org/publications/paper/1Cs
	https://doi.org/10.29007/w5m5

BibTeX entry

@inproceedings{SMT2012:SMT_LIB_Sequences_Regular,
  author    = {Nikolaj Bjorner and Vijay Ganesh and Raphaël Michel and Margus Veanes},
  title     = {SMT-LIB Sequences and Regular Expressions},
  booktitle = {SMT 2012. 10th International Workshop on Satisfiability Modulo Theories},
  editor    = {Pascal Fontaine and Amit Goel},
  series    = {EPiC Series in Computing},
  volume    = {20},
  publisher = {EasyChair},
  bibsource = {EasyChair, https://easychair.org},
  issn      = {2398-7340},
  url       = {/publications/paper/1Cs},
  doi       = {10.29007/w5m5},
  pages     = {77-87},
  year      = {2013}}

Download PDF Open PDF in browser