Document Open Access Logo

Symbolic Automata Theory with Applications (Invited Talk)

Author Margus Veanes

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2017.7.pdf
  • Filesize: 237 kB
  • 3 pages

Document Identifiers

Subject Classification

Keywords
  • automaton
  • transducer
  • symbolic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Symbolic automata extend classic finite state automata by allowing
transitions to carry predicates over rich alphabet theories. The
key algorithmic difference to classic automata is the ability to
efficiently operate over very large or infinite alphabets. In this
talk we give an overview of what is currently known about symbolic
automata, what their main applications are, and what challenges
arise when reasoning about them. We also discuss some of the open
problems and research directions in symbolic automata theory.

Cite As Get BibTex

Margus Veanes. Symbolic Automata Theory with Applications (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 7:1-7:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CSL.2017.7

Author Details

Margus Veanes

References

  1. Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools (2nd Edition). Addison-Wesley, 2006. Google Scholar
  2. Rajeev Alur, Loris D'Antoni, and Mukund Raghothaman. Drex: A declarative language for efficiently evaluating regular string transformations. ACM SIGPLAN Notices - POPL'15, 50(1):125-137, 2015. Google Scholar
  3. Ahmed Bouajjani, Peter Habermehl, and Tomáš Vojnar. Abstract regular model checking. In CAV'04, pages 372-386. Springer, 2004. Google Scholar
  4. Mila Dalla Preda, Roberto Giacobazzi, Arun Lakhotia, and Isabella Mastroeni. Abstract symbolic automata: Mixed syntactic/semantic similarity analysis of executables. ACM SIGPLAN Notices - POPL'15, 50(1):329-341, 2015. Google Scholar
  5. Loris D'Antoni and Margus Veanes. Minimization of symbolic automata. ACM SIGPLAN Notices - POPL'14, 49(1):541-553, 2014. Google Scholar
  6. Loris D'antoni and Margus Veanes. Extended symbolic finite automata and transducers. Formal Methods System Design, 47(1):93-119, August 2015. Google Scholar
  7. Loris D'Antoni and Margus Veanes. Forward bisimulations for nondeterministic symbolic finite automata. In Axel Legay and Tiziana Margaria, editors, Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, TACAS 2017, volume 10205 of LNCS, pages 518-534. Springer, 2017. Google Scholar
  8. Loris D'Antoni and Margus Veanes. The power of symbolic automata and transducers. In Computer Aided Verification, 29th International Conference (CAV'17). Springer, 2017. Google Scholar
  9. Loris D'Antoni, Margus Veanes, Benjamin Livshits, and David Molnar. Fast: A transducer-based language for tree manipulation. ACM TOPLAS, 38(1):1-32, 2015. Google Scholar
  10. Pieter Hooimeijer, Benjamin Livshits, David Molnar, Prateek Saxena, and Margus Veanes. Fast and precise sanitizer analysis with BEK. In Proceedings of the 20th USENIX Conference on Security, SEC'11, 2011. Google Scholar
  11. Qinheping Hu and Loris D'Antoni. Automatic program inversion using symbolic transducers. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, pages 376-389, 2017. Google Scholar
  12. Amaldev Manuel and Ramaswamy Ramanujam. Automata over infinite alphabets. In Deepak D'Souza and Priti Shankar, editors, Modern Applications of Automata Theory, pages 529-554. World Scientific, 2012. Google Scholar
  13. Mehryar Mohri. Finite-state transducers in language and speech processing. Computational Linguistics, 23(2):269-311, 1997. Google Scholar
  14. Kristin Y. Rozier and Moshe Y. Vardi. A multi-encoding approach for LTL symbolic satisfiability checking. In FM'11, pages 417-431, 2011. Google Scholar
  15. Olli Saarikivi, Margus Veanes, Todd Mytkowicz, and Madan Musuvathi. Fusing effectful comprehensions. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, pages 17-32. ACM, 2017. Google Scholar
  16. Gertjan van Noord and Dale Gerdemann. Finite state transducers with predicates and identities. Grammars, 4(3):263-286, 2001. Google Scholar
  17. Margus Veanes, Peli de Halleux, and Nikolai Tillmann. Rex: Symbolic regular expression explorer. In ICST'10, pages 498-507. IEEE, 2010. Google Scholar
  18. Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, and Nikolaj Bjørner. Symbolic finite state transducers: Algorithms and applications. ACM SIGPLAN Notices - POPL'12, 47(1):137-150, 2012. Google Scholar
  19. Margus Veanes, Todd Mytkowicz, David Molnar, and Benjamin Livshits. Data-parallel string-manipulating programs. ACM SIGPLAN Notices - POPL'15, 50(1):139-152, 2015. Google Scholar
  20. Bruce W. Watson. Extended Finite State Models of Language, chapter Implementing and using finite automata toolkits, pages 19-36. Cambridge U. Press, 1999. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact