Symbolic String Transformations with Regular Lookahead and Rollback

摘要: Implementing string transformation routines, such as encoders, decoders, and sanitizers, correctly efficiently is a difficult error prone task. Such routines are often used in security critical settings, process large amounts of data, must work correctly. We introduce new declarative language called Bex that builds on elements regular expressions, symbolic automata transducers, enables compilation scheme into C, C# or JavaScript avoids many the potential sources errors arise when implemented directly. The approach allows correctness analysis using theory not possible at level generated code. Moreover, case studies show code consistently outperforms hand-optimized