Margus Veanes

Principal Researcher

Publications

View by:

- Regex Decision Procedures in Extended RE#
  
  Ian Erik Varatalu, Margus Veanes, Ekaterina Zhuchko, Juhan Ernits
  
  CAV 2025 | July 2025
  
  Editor(s): R. Piskac and Z. Rakamaric
  
  Published in LNCS vol. 15933
  
  DOI Project
- RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement, and Restricted Lookarounds
  
  Ian Erik Varatalu, Margus Veanes, Juhan Ernits
  
  POPL | January 2025
  
  DOI Author's Version Project
- Symbolic Automata: Omega-Regularity Modulo Theories
  
  Margus Veanes, Thomas Ball, Gabriel Ebner, Ekaterina Zhuchko
  
  POPL | January 2025
  
  Author's Version DOI Project
- Lean Formalization of Extended Regular Expression Matching with Lookarounds
  
  Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner
  
  CPP | January 2024
  
  Author's Version DOI Project
- Derivative Based Nonbacktracking Real-World Regex Matching with Backtracking Semantics
  
  Dan Moseley, Mario Nishio, Jose Perez Rodriguez, Olli Saarikivi, Stephen Toub, Margus Veanes, Tiki Wan, Eric Xu
  
  MSR-TR-2023-15 | April 2023
  
  Published by Microsoft
  
  Extended version of paper that appears in PLDI 2023.
  
  Publication Author's Version Project
- Incremental Dead State Detection in Logarithmic Time
  
  Caleb Stanford , Margus Veanes
  
  January 2023
  
  Preliminary and extended version of paper that appears in CAV 2023
  
  DOI
- Lost in Translation: from Linear Temporal Logic to Büchi Automata
  
  Margus Veanes, Olli Saarikivi, Thomas Ball
  
  MSR-TR-2022-26 | October 2022
  
  Published by Microsoft
  
  Publication Project
- Counting in Regexes Considered Harmful: Exposing ReDoS Vulnerability of Nonbacktracking Matchers
  
  Lenka Turoňová, Lukáš Holík, Ivan Homoliak, Ondřej Lengál, Margus Veanes, Tomáš Vojnar
  
  31st USENIX Security Symposium | August 2022
  
  Publication
- Regex Matching with Counting-Set Automata
  
  Margus Veanes (margus), Lukas Holik, Ondrej Lengal, Olli Saarikivi (olsaarik), Lenka Turonova, Tomas Vojnar
  
  MSR-TR-2020-31 | September 2020
  
  Published by Microsoft
  
  The technical report includes detailed proofs of most of the theorems stated in the conference OOPSLA'2020 paper.
  
  DOI Project
- Symbolic Boolean Derivatives for Efficiently Solving Extended Regular Expression Constraints
  
  Caleb Stanford, Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2020-25 | August 2020
  
  Published by Microsoft
  
  Updated November 2020. Extended version of paper in PLDI'2021.
  
  Publication Author's Version Project
- Niijima: sound and automated computation consolidation for efficient multilingual data-parallel pipelines
  
  Guoqing Harry Xu, Margus Veanes (margus), Michael Barnett, Madan Musuvathi (madanm), Todd Mytkowicz (toddm), Ben Zorn (zorn), Huan He, Haibo Lin
  
  Proceedings of the 27th ACM Symposium on Operating Systems Principles | October 2019
  
  Publication DOI
- Symbolic Regex Matcher
  
  Margus Veanes (margus), Olli Saarikivi (olsaarik), Tiki Wan, Eric Xu
  
  TACAS | April 2019
  
  Author's Version Project
- Simulation Algorithms for Symbolic Automata
  
  Lukáš Holík, Ondřej Lengál, Juraj Síč, Margus Veanes, Tomáš Vojnar
  
  International Symposium on Automated Technology for Verification and Analysis (ATVA) | September 2018
  
  Editor(s): Lahiri, S. and Wang, C.
  
  DOI
- Theoretical Aspects of Symbolic Automata
  
  Hellis Tamm, Margus Veanes
  
  44th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'18) | January 2018
  
  Publication Project
- Minimization of Symbolic Transducers
  
  Olli Saarikivi, Margus Veanes
  
  Computer Aided Verification, 29th International Conference (CAV 2017) | July 2017
  
  Publication Project
- The power of symbolic automata and transducers
  
  Loris D'Antoni, Margus Veanes
  
  Computer Aided Verification, 29th International Conference (CAV'17) | July 2017
  
  Publication Project
- Fusing Effectful Comprehensions
  
  Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi
  
  ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017) | June 2017
  
  Publication Project
- Monadic Decomposition
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  Journal of the ACM | May 2017, Vol 64
  
  Publication Publication Publication Project
- Forward Bisimulations for Nondeterministic Symbolic Finite Automata
  
  Loris D'Antoni, Margus Veanes
  
  TACAS | April 2017
  
  Publication Project
- Prepose: Privacy, Security, and Reliability for Gesture-Based Programming
  
  Lucas Silva Figueiredo , David Molnar, Margus Veanes, Benjamin Livshits
  
  IEEE Security & Privacy | April 2017, Vol 15: pp. 14-23
  
  Publication Publication
- Translating C# to Branching Symbolic Transducers
  
  Olli Saarikivi, Margus Veanes
  
  LPAR-21: 21ST INTERNATIONAL CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING (Selected Workshop and Short Presentations) | March 2017
  
  Publication Project
- Monadic Second-Order Logic on Finite Sequences
  
  Loris D'Antoni, Margus Veanes
  
  POPL'2017 | January 2017
  
  Publication Publication Project
- Prepose: Privacy, Security, and Reliability for Gesture-Based Programming
  
  Lucas Silva Figueiredo, David Molnar, Margus Veanes, Ben Livshits
  
  IEEE Journal of Security and Privacy | December 2016
  
  Publication
- Fusing Effectful Comprehensions
  
  Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi
  
  MSR-TR-2016-55 | October 2016
  
  Publication
- Minimization of Symbolic Tree Automata
  
  Margus Veanes
  
  LICS | July 2016
  
  LICS
  
  Publication
- Fast: A Transducer-Based Language for Tree Manipulation
  
  Loris D’antoni, Margus Veanes, Ben Livshits, David Molnar
  
  ACM Transactions on Programming Languages and Systems (TOPLAS), 2015 | October 2015
  
  Publication Publication
- FAST: A Transducer-Based Language for Tree Manipulation
  
  Lori D'Antoni, Margus Veanes, Ben Livshits, David Molnar
  
  ACM Transactions on Programming Languages and Systems (TOPLAS) | October 2015, Vol 38
  
  Publication Publication
- Extended symbolic finite automata and transducers
  
  Loris D’Antoni, Margus Veanes
  
  Formal Methods in System Design | July 2015
  
  Publication
- Symbolic Tree Automata
  
  Margus Veanes, Nikolaj Bjørner
  
  Information Processing Letters | March 2015, Vol 115(3): pp. 418-424
  
  Publication Publication
- Symbolic String Transformations with Regular Lookahead and Rollback
  
  Margus Veanes
  
  PSI 2014 | February 2015
  
  Publication Publication
- Program Boosting: Program Synthesis via Crowd-Sourcing
  
  Robert A Cochran, Loris D’Antoni, Ben Livshits, David Molnar, Margus Veanes
  
  Symposium on the Principles of Programming Languages (POPL) | January 2015
  
  Publication Publication
- Data-Parallel String-Manipulating Programs
  
  Margus Veanes, Todd Mytkowicz, David Molnar, Ben Livshits
  
  Symposium on the Principles of Programming Languages (POPL), Mumbai, India | January 2015
  
  Publication Publication
- Data-Parallel String-Manipulating Programs
  
  Margus Veanes, Todd Mytkowicz, David Molnar, Ben Livshits
  
  POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2015
  
  POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
  
  Publication Publication Project Project
- Program Boosting: Program Synthesis via Crowd-Sourcing
  
  Robert A Cochran, , Benjamin Livshits, David Molnar, Margus Veanes, Ben Livshits
  
  POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2015
  
  Publication Publication
- PrePose: Security and Privacy for Gesture-Based Programming
  
  Lucas Silva Figueiredo, Ben Livshits, David Molnar, Margus Veanes
  
  MSR-TR-2014-146 | November 2014
  
  Publication
- Skolemization Modulo Theories
  
  Konstantin Korovin, Margus Veanes
  
  ICMS'14 | August 2014
  
  Publication Publication
- Monadic Decomposition
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  CAV'14 | July 2014
  
  Publication
- FAST: A Transducer-Based Language for Tree Manipulation
  
  Margus Veanes, Benjamin Livshits, David Molnar, Ben Livshits
  
  PLDI 2014: Programming Language Design and Implementation | June 2014
  
  Publication
- Minimization of Symbolic Automata
  
  Loris D'Antoni, Margus Veanes
  
  POPL'14 | January 2014
  
  POPL'14
  
  Publication Project
- Effectively Monadic Predicates
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  LPAR-19 | December 2013
  
  Publication
- FAST: A Transducer-Based Language for Tree Manipulation
  
  Loris D'Antoni, Margus Veanes, Ben Livshits, David Molnar,
  
  MSR-TR-2013-121 | November 2013
  
  Publication
- Applications of Symbolic Finite Automata
  
  Margus Veanes
  
  CIAA'13 | July 2013
  
  Publication Project
- Equivalence of Extended Symbolic Finite Transducers
  
  Loris D'Antoni, Margus Veanes,
  
  25th International Conference on Computer Aided Verification (CAV'13) | July 2013
  
  The associated TR is an extended version of the conference paper.
  
  Publication
- Minimization of Symbolic Automata
  
  Margus Veanes
  
  MSR-TR-2013-48 | April 2013
  
  Publication
- Equivalence of Extended Symbolic Finite Transducers
  
  Loris D'Antoni, Margus Veanes,
  
  MSR-TR-2013-4 | January 2013
  
  Publication
- Static Analysis of String Encoders and Decoders
  
  Margus Veanes, Loris D'Antoni
  
  VMCAI 2013 | January 2013
  
  Publication
- Data-Parallel String-Manipulating Programs
  
  Margus Veanes, David Molnar, Todd Mytkowicz, Ben Livshits
  
  MSR-TR-2012-72 | July 2012
  
  Publication Project Project
- Symbolic Automata: The Toolkit
  
  Margus Veanes, Nikolaj Bjørner
  
  TACAS'12 | March 2012
  
  Publication
- Symbolic Finite State Transducers: Algorithms and Applications
  
  Margus Veanes, Pieter Hooimeijer, David Molnar, Nikolaj Bjorner, Ben Livshits
  
  POPL'12 | January 2012
  
  Publication
- Generating Fast String Manipulating Code Through Transducer Exploration and SIMD Integration
  
  Margus Veanes, David Molnar, Ben Livshits, Lubomir Litchev
  
  MSR-TR-2011-124 | November 2011
  
  Publication
- Alternating simulation and IOCO
  
  Margus Veanes, Nikolaj Bjørner
  
  International Journal on Software Tools for Technology Transfer (STTT) | September 2011
  
  Publication Publication
- Fast and Precise Sanitizer Analysis with BEK
  
  Pieter Hooimeijer, Ben Livshits, David Molnar, Prateek Saxena, Margus Veanes,
  
  USENIX Security'11 | August 2011
  
  USENIX Security'11
  
  Publication
- Symbolic Finite State Transducers: Algorithms and Applications
  
  Nikolaj Bjørner, Ben Livshits, David Molnar, Margus Veanes
  
  MSR-TR-2011-85 | July 2011
  
  Publication
- Decision Procedures for Composition and Equivalence of Symbolic Finite State Transducers
  
  Margus Veanes, David Molnar, Ben Livshits
  
  MSR-TR-2011-32 | March 2011
  
  Publication
- Symbolic Transducers
  
  Nikolaj Bjørner, Margus Veanes
  
  MSR-TR-2011-3 | January 2011
  
  Publication
- Symbolic Tree Transducers
  
  Margus Veanes, Nikolaj Bjørner
  
  Ershov Informatics Conference (PSI'11) | January 2011
  
  Publication
- BEK: Modeling Imperative String Operations with Symbolic Transducers
  
  , Ben Livshits, David Molnar, Prateek Saxena, Margus Veanes
  
  MSR-TR-2010-154 | November 2010
  
  Publication
- Composing Model Programs for Analysis
  
  Margus Veanes, Jonathan Jacky
  
  The Journal of Logic and Algebraic Programming | October 2010, Vol 79: pp. 467-482
  
  Publication Publication
- An Evaluation of Automata Algorithms for String Analysis
  
  , Margus Veanes
  
  MSR-TR-2010-90 | July 2010
  
  Updated August, 2010
  
  Publication Project
- Modeling Imperative String Operations with Transducers
  
  Pieter Hooimeijer, David Molnar, Prateek Saxena, Margus Veanes
  
  MSR-TR-2010-96 | July 2010
  
  Publication
- Alternating Simulation and IOCO
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2010-38 | April 2010
  
  Extended version of paper with the same title in ICTSS 2010, LNCS vol 6435
  
  Publication
- Qex: Symbolic SQL Query Explorer
  
  Margus Veanes, Nikolai Tillmann, Jonathan "Peli" de Halleux
  
  LPAR-16 | April 2010
  
  Publication Publication Project
- Rex: Symbolic Regular Expression Explorer
  
  Margus Veanes, Jonathan "Peli" de Halleux, Nikolai Tillmann
  
  Third International Conference on Software Testing, Verification and Validation (ICST) | April 2010
  
  Publication Publication Project Project Project
- Solving Extended Regular Constraints Symbolically
  
  Margus Veanes, Nikolaj Bjørner, Leonardo de Moura
  
  MSR-TR-2009-177 | December 2009
  
  Publication Project
- Symbolic Query Exploration
  
  Margus Veanes, Pavel Grigorenko, Jonathan "Peli" de Halleux, Nikolai Tillmann
  
  ICFEM'09 | December 2009
  
  Publication Project
- Model-Based Testing of Web Applications using NModel
  
  Juhan Ernits, Rivo Roo, Jonathan Jacky, Margus Veanes
  
  LNCS, TESTCOM/FATES 2009 | November 2009
  
  Publication Publication
- Qex: Symbolic SQL Query Explorer
  
  Margus Veanes, Jonathan de Halleux, Nikolai Tillmann, Jonathan "Peli" de Halleux
  
  MSR-TR-2009-2015 | October 2009
  
  Updated January 2010
  
  Publication Project
- Rex: Symbolic Regular Expression Explorer
  
  Margus Veanes, Jonathan "Peli" de Halleux, Nikolai Tillmann
  
  MSR-TR-2009-137 | October 2009
  
  ICST'10
  
  Publication Publication Project
- Symbolic Bounded Model Checking of Abstract State Machines
  
  Margus Veanes, Nikolaj Bjørner, Yuri Gurevich, Wolfram Schulte
  
  Int J Software Informatics | June 2009, pp. 149-170
  
  Publication Project
- Input-Output Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-56 | May 2009
  
  Preliminary version of paper to appear in ICTAC'09, LNCS.
  
  Publication
- Symbolic Query Exploration
  
  Margus Veanes, Pavel Grigorenko, Jonathan "Peli" de Halleux, Nikolai Tillmann
  
  MSR-TR-2009-65 | May 2009
  
  Publication Project Project
- Symbolic Bounded Conformance Checking of Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-28 | March 2009
  
  This is an extended version of a paper to appear in PSI'09, LNCS.
  
  Publication Project
- Arranging Partitures for Models and Theorems
  
  Johannes Helander, Margus Veanes
  
  MSR-TR-2009-24 | March 2009
  
  Publication
- On Bounded Reachability of Programs with Set Comprehensions
  
  Margus Veanes, Ando Saabas
  
  LPAR'08 | November 2008
  
  LPAR'08
  
  Publication Project
- Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract)
  
  Margus Veanes, Ando Saabas
  
  ABZ'08 | September 2008
  
  This is an extended abstract.
  
  Publication Publication Project
- An SMT Approach to Bounded Reachability Analysis of Model Programs
  
  Margus Veanes, Nikolaj Bjørner, Alexander Raschke
  
  FORTE'08 | June 2008
  
  FORTE'08
  
  Publication Project Project
- Model-Based Testing of Robots with NModel
  
  Juhan Ernits, Margus Veanes, Johannes Helander
  
  TestCom/FATES 2008 Short Papers | June 2008
  
  TestCom/FATES 2008 Short Papers
  
  Publication
- Protocol Modeling with Model Program Composition
  
  Margus Veanes, Wolfram Schulte
  
  FORTE'08 | June 2008
  
  ISBN: 978-3-540-68854-9
  
  Publication
- Bounded reachability of model programs
  
  Margus Veanes, Ando Saabas, Nikolaj Bjørner
  
  MSR-TR-2008-81 | May 2008
  
  Parts of this report are presented at FORTE'08 and LPAR'08.
  
  Publication Project
- Enabling the Future Auto with Model-Driven Services
  
  Johannes Helander, Margus Veanes
  
  National Workshop on High-Confidence Automotive Cyber-Physical Systems. | April 2008
  
  Publication
- Model-Based Software Testing and Analysis with C#
  
  Jonathan Jacky, Margus Veanes, Colin Campbell, Wolfram Schulte
  
  Published by Cambridge University Press | January 2008
  
  ISBN: 9.78052E+12
  
  Publication
- Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer
  
  Margus Veanes, Colin Campbell, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, Lev Nachmanson
  
  Formal Methods and Testing | Published by Springer Verlag | 2008, Vol 4949
  
  ISBN: 978-3-540-78916-1
  
  The attached file is a preliminary version.
  
  Publication Project Project Project
- Adapting Futures: Scalability for Real-World Computing
  
  Johannes Helander, Risto Serg, Margus Veanes, Pritam Roy
  
  RTSS'07 | December 2007
  
  Publication Publication
- Embedded Systems Research at DemoFest’07
  
  Oscar Almeida, Alessandro Forin, Philip Garcia, Johannes Helander, Nishith Khantal, Hong Lu, Karl Meier, Sibin Mohan, Henrik Frystyk Nielsen, Neil Pittman, Risto Serg, Bharat Sukhwani, Margus Veanes, Ben Zorn, Sarah Berry, Chris Boyce, David Chaszar, Brandon Culrich, Mikhail Kisin, Gabe Knezek, Warren Linam-Church, Steve Liu, Michael Stewart, Doug Toney
  
  MSR-TR-2007-94 | July 2007
  
  Publication Publication
- Composition of Model Programs
  
  Margus Veanes, Colin Campbell, Wolfram Schulte
  
  FORTE | June 2007
  
  ISBN: 978-3-540-73195-5
  
  Publication Project
- State Isomorphism in Model Programs with Abstract Data Structures
  
  Margus Veanes, Juhan Ernits, Colin Campbell
  
  FORTE'07 | June 2007
  
  Publication Project
- Can Abstract State Machines Be Useful in Language Theory?
  
  Yuri Gurevich, Margus Veanes, Charles Wallace
  
  Theoretical Computer Science | January 2007, Vol 376: pp. 17-29
  
  Publication Project
- Online Testing with Reinforcement Learning
  
  Margus Veanes, Pritam Roy, Colin Campbell
  
  Formal Approaches to Software Testing and Runtime Verification, FATES/RV 2006 | January 2006
  
  Publication
- Action Machines – Towards a Framework for Model Composition, Exploration and Conformance Testing Based on Symbolic Computation
  
  Nikolai Tillmann, Wolfram Schulte, Margus Veanes
  
  Quality Software, 2005. (QSIC 2005). Fifth International Conference on | September 2005
  
  Quality Software, 2005. (QSIC 2005). Fifth International Conference on
  
  ISBN: 0-7695-2399-4
  
  Publication Project
- Play to Test
  
  Andreas Blass, Yuri Gurevich, Lev Nachmanson, Margus Veanes
  
  FATES 2005 | July 2005
  
  Publication Project Project
- Multiplexing of Partially Ordered Events
  
  Colin Campbell, Margus Veanes, Jiale Huo, Alexandre Petrenko
  
  TestCom 2005 | June 2005
  
  Received Best paper award.
  
  Publication Project
- Exploration with Multiple State Groupings
  
  Colin Campbell, Margus Veanes
  
  Abstract State Machines 2005 | January 2005
  
  Publication Project Project
- On-The-Fly Testing of Reactive Systems
  
  Margus Veanes, Colin Campbell, Wolfram Schulte, Pushmeet Kohli
  
  MSR-TR-2005-05 | January 2005
  
  Publication Project
- Online testing with model programs
  
  Margus Veanes, Colin Campbell, Wolfram Schulte, Nikolai Tillmann
  
  ESEC/SIGSOFT FSE | January 2005
  
  ESEC/SIGSOFT FSE
  
  ISBN: 1-59593-014-0
  
  Publication Project Project
- Play to Test
  
  Andreas Blass, Yuri Gurevich, Lev Nachmanson, Margus Veanes
  
  MSR-TR-2005-04 | January 2005
  
  A short version appears in: FATES 2005, LNCS vol. 3997, pp. 32-46
  
  Publication Project
- Testing Concurrent Object-Oriented Systems with Spec Explorer
  
  Colin Campbell, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  January 2005
  
  ISBN: 3-540-27882-6
  
  Publication Project Project Project
- Abstract Communication Model for Distributed Systems
  
  Uwe Glässer, Yuri Gurevich, Margus Veanes
  
  IEEE Transactions on Software Engineering | July 2004, Vol 30(7): pp. 458-472
  
  Publication Project Project
- Instrumenting Scenarios in a Model-Driven Development Environment
  
  Wolfgang Grieskamp, Nikolai Tillmann, Margus Veanes
  
  Journal of Information and Software Technology | January 2004, Vol 46: pp. 1027-1036
  
  Publication Project Project Project
- Optimal Strategies for Testing Nondeterministic Systems
  
  Lev Nachmanson, Margus Veanes, Wolfram Schulte, Nikolai Tillmann, Wolfgang Grieskamp
  
  ISSTA 2004 | January 2004
  
  ISBN: 1-58113-820-2
  
  Publication Project Project
- Towards a Tool Environment for Model-Based Testing with AsmL
  
  Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  FATES 2003 | January 2004
  
  Publication Project Project Project
- Combined Algorithm for Approximating a Finite State Abstraction of a Large System
  
  Rostislav Yavorsky, Margus Veanes
  
  ICSE 2003/Scenarios Workshop | January 2003
  
  ICSE 2003/Scenarios Workshop
  
  Publication Project Project
- Model-Based Testing with AsmL .NET
  
  Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  1st European Conference on Model-Driven Software Engineering | January 2003
  
  Publication Project Project Project
- Scenario-oriented Modeling in AsmL and its Instrumentation for Testing
  
  Mike Barnett, Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  Proc. of 2nd International Workshop on Scenarios and State Machines: Models, Algorithms, and Tools held at ICSE 2003, International Conference on Software Engineering 2003 | January 2003
  
  Publication
- Validating Use-Cases with the AsmL Test Tool
  
  Wolfram Schulte, Nikolai Tillmann, Margus Veanes, Mike Barnett
  
  QSIC | January 2003
  
  QSIC
  
  ISBN: 0-7695-2015-4
  
  Publication Project Project
- Generating finite state machines from abstract state machines
  
  Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
  
  ISSTA 2002 | July 2002
  
  Publication Project Project
- An Abstract Communication Model
  
  Uwe Glässer, Yuri Gurevich, Margus Veanes
  
  MSR-TR-2002-55 | May 2002
  
  Publication Publication Project
- High-level Executable Specification of the Universal Plug and Play Architecture
  
  Uwe Glässer, Yuri Gurevich, Margus Veanes
  
  HICSS 2002 | January 2002
  
  Publication Project
- Universal Plug and Play Machine Models: Modeling with Distributed Abstract State Machines
  
  Uwe Glässer, Margus Veanes
  
  Design and Analysis of Distributed Embedded Systems, IFIP 17th World Computer Congress (DIPES 2002) | January 2002
  
  Publication Project
- Universal Plug and Play Machine Models
  
  U. Glässer, Y. Gurevich, M. Veanes, Yuri Gurevich, Margus Veanes
  
  MSR-TR-2001-59 | June 2001
  
  Publication Project
- Conformance Testing with Abstract State Machines
  
  Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
  
  EUROCAST 2001 | February 2001
  
  Publication Project
- Toward Industrial Strength Abstract State Machines
  
  Yuri Gurevich, Wolfram Schulte, Margus Veanes
  
  MSR-TR-2001-98 | October 2001
  
  Publication Project
- Decidability and Complexity of Simultaneous Rigid E-Unification with One Variable and Related Results
  
  Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, Andrei Voronkov
  
  Theoretical Computer Science | August 2000, Vol 243(1-2): pp. 167-184
  
  Publication
- Farmer’s Theorem revisited
  
  Margus Veanes
  
  Information Processing Letters | April 2000, Vol 74: pp. 47-53
  
  Publication
- On the Undecidability of Second-Order Unification
  
  Jordi Levy, Margus Veanes
  
  Information and Computation | January 2000, Vol 159: pp. 125-150
  
  Publication Publication
- Rigid Reachability, The Non-Symmetric Form of Rigid E-Unification
  
  Harald Ganzinger, Florent Jacquemard, Margus Veanes
  
  International Journal of Foundations of Computer Science | January 2000, pp. 3-27
  
  Publication
- Using Abstract State Machines at Microsoft: A Case Study
  
  Yuri Gurevich, Wolfram Schulte, Margus Veanes, Mike Barnett
  
  Abstract State Machines | January 2000
  
  Abstract State Machines
  
  ISBN: 3-540-67959-6
  
  Publication Project
- Logic with Equality: Partisan Corroboration and Shifted Pairing
  
  Yuri Gurevich, Margus Veanes
  
  August 1999
  
  Publication Publication
- Decidable Fragments of Simultaneous Rigid Reachability
  
  Véronique Cortier, Harald Ganzinger, Florent Jacquemard, Margus Veanes
  
  ICALP 1999 | January 1999
  
  Publication
- The Two-Variable Guarded Fragment with Transitive Relations
  
  Harald Ganzinger, Christoph Meyer, Margus Veanes
  
  LICS 1999 | January 1999
  
  Publication
- The relation between second-order unification and simultaneous rigid E-unification
  
  Margus Veanes
  
  Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS'98) | June 1998
  
  Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS'98)
  
  Publication
- The Relation Between Second-Order Unification and Simultaneous Rigid E-Unification
  
  Margus Veanes
  
  MPI-I-98-2-005 | February 1998
  
  Publication
- On Unification Problems in Restricted Second-Order Languages
  
  Jordi Jevy, Margus Veanes
  
  Annual Conference of the European Association for Computer Science Logic, CSL'98 | January 1998
  
  Annual Conference of the European Association for Computer Science Logic, CSL'98
  
  Appears in preliminary proceedings of CSL'98
  
  Publication
- Rigid Reachability
  
  Harald Ganzinger, Florent Jacquemard, Margus Veanes
  
  Proceedings of the 4th Asian Computing Science Conference on Advances in Computing Science (ASIAN 98) | January 1998
  
  Publication
- The Decidability of Simultaneous Rigid E-Unification with One Variable
  
  Paliath Narendran, Margus Veanes, Andrei Voronkov, Anatoli Degtyarev, Yuri Gurevich
  
  RTA'98 | January 1998
  
  Publication
- On Simultaneous Rigid E-Unification
  
  Margus Veanes
  
  June 1997, pp. 120
  
  June 1997
  
  Publication Publication
- The decidability of simultaneous rigid E-unification with one variable
  
  Paliath Narendran, Margus Veanes, Andrei Voronkov, Anatoli Degtyarev, Yuri Gurevich
  
  139 | April 1997
  
  Publication
- Some undecidable problems related to the Herbrand theorem
  
  Yuri Gurevich, Margus Veanes
  
  UPMAIL-TR-138 | March 1997
  
  Publication
- On Computational Complexity of Basic Decision Problems of Finite Tree Automata
  
  Margus Veanes
  
  133 | January 1997
  
  Publication
- The undecidability of simultaneous rigid E-unification with two variables
  
  Margus Veanes
  
  5th Kurt GÃ¶del Colloquium (KGC'97) | January 1997
  
  Publication
- Uniform representation of recursively enumerable sets with simultaneous rigid E-unification
  
  Margus Veanes
  
  126 | June 1996
  
  Publication
- Construction of natural cycletrees
  
  Margus Veanes, Jonas Barklund
  
  Information Processing Letters | January 1996, Vol 60: pp. 313-318
  
  Publication
- Natural cycletrees: Flexible interconnection graphs
  
  Margus Veanes, Jonas Barklund
  
  Journal of Parallel and Distributed Computing | January 1996, Vol 33: pp. 44-54
  
  Publication Publication
- On the number of edges in cycletrees
  
  Margus Veanes, Jonas Barklund
  
  Information Processing Letters | January 1996, Vol 57: pp. 225-229
  
  Publication Publication
- Meta-programming with Theory Systems
  
  Jonas Barklund, Katrin Boberg, Pierangelo Dell'Acqua, Margus Veanes
  
  106 | May 1995
  
  This paper appears as a chapter in Metalogics and Logic Programming, edited by K. Apt and F. Turini, and published by MIT Press in 1995.
  
  Publication
- Cycletrees: Flexible Interconnection Graphs for Parallel Computing
  
  Margus Veanes, Jonas Barklund
  
  97 | February 1995
  
  Publication
- Cycletrees: a Novel Class of Interconnection Graphs
  
  Margus Veanes
  
  January 1993
  
  January 1993
  
  Publication

- Universal Plug and Play Machine Models
  
  U. Glässer, Y. Gurevich, M. Veanes, Yuri Gurevich, Margus Veanes
  
  MSR-TR-2001-59 | June 2001
  
  Publication Project
- Conformance Testing with Abstract State Machines
  
  Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
  
  EUROCAST 2001 | February 2001
  
  Publication Project
- Decidability and Complexity of Simultaneous Rigid E-Unification with One Variable and Related Results
  
  Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, Andrei Voronkov
  
  Theoretical Computer Science | August 2000, Vol 243(1-2): pp. 167-184
  
  Publication
- Farmer’s Theorem revisited
  
  Margus Veanes
  
  Information Processing Letters | April 2000, Vol 74: pp. 47-53
  
  Publication
- Using Abstract State Machines at Microsoft: A Case Study
  
  Yuri Gurevich, Wolfram Schulte, Margus Veanes, Mike Barnett
  
  Abstract State Machines | January 2000
  
  Abstract State Machines
  
  ISBN: 3-540-67959-6
  
  Publication Project
- Rigid Reachability, The Non-Symmetric Form of Rigid E-Unification
  
  Harald Ganzinger, Florent Jacquemard, Margus Veanes
  
  International Journal of Foundations of Computer Science | January 2000, pp. 3-27
  
  Publication
- Decidable Fragments of Simultaneous Rigid Reachability
  
  Véronique Cortier, Harald Ganzinger, Florent Jacquemard, Margus Veanes
  
  ICALP 1999 | January 1999
  
  Publication
- On Simultaneous Rigid E-Unification
  
  Margus Veanes
  
  June 1997, pp. 120
  
  June 1997
  
  Publication Publication
- On Computational Complexity of Basic Decision Problems of Finite Tree Automata
  
  Margus Veanes
  
  133 | January 1997
  
  Publication
- Construction of natural cycletrees
  
  Margus Veanes, Jonas Barklund
  
  Information Processing Letters | January 1996, Vol 60: pp. 313-318
  
  Publication
- Meta-programming with Theory Systems
  
  Jonas Barklund, Katrin Boberg, Pierangelo Dell'Acqua, Margus Veanes
  
  106 | May 1995
  
  This paper appears as a chapter in Metalogics and Logic Programming, edited by K. Apt and F. Turini, and published by MIT Press in 1995.
  
  Publication
- Cycletrees: Flexible Interconnection Graphs for Parallel Computing
  
  Margus Veanes, Jonas Barklund
  
  97 | February 1995
  
  Publication
- Cycletrees: a Novel Class of Interconnection Graphs
  
  Margus Veanes
  
  January 1993
  
  January 1993
  
  Publication
- Regex Decision Procedures in Extended RE#
  
  Ian Erik Varatalu, Margus Veanes, Ekaterina Zhuchko, Juhan Ernits
  
  CAV 2025 | July 2025
  
  Editor(s): R. Piskac and Z. Rakamaric
  
  Published in LNCS vol. 15933
  
  DOI Project
- Symbolic Automata: Omega-Regularity Modulo Theories
  
  Margus Veanes, Thomas Ball, Gabriel Ebner, Ekaterina Zhuchko
  
  POPL | January 2025
  
  Author's Version DOI Project
- RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement, and Restricted Lookarounds
  
  Ian Erik Varatalu, Margus Veanes, Juhan Ernits
  
  POPL | January 2025
  
  DOI Author's Version Project
- Lean Formalization of Extended Regular Expression Matching with Lookarounds
  
  Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner
  
  CPP | January 2024
  
  Author's Version DOI Project
- Derivative Based Nonbacktracking Real-World Regex Matching with Backtracking Semantics
  
  Dan Moseley, Mario Nishio, Jose Perez Rodriguez, Olli Saarikivi, Stephen Toub, Margus Veanes, Tiki Wan, Eric Xu
  
  MSR-TR-2023-15 | April 2023
  
  Published by Microsoft
  
  Extended version of paper that appears in PLDI 2023.
  
  Publication Author's Version Project
- Incremental Dead State Detection in Logarithmic Time
  
  Caleb Stanford , Margus Veanes
  
  January 2023
  
  Preliminary and extended version of paper that appears in CAV 2023
  
  DOI
- Lost in Translation: from Linear Temporal Logic to Büchi Automata
  
  Margus Veanes, Olli Saarikivi, Thomas Ball
  
  MSR-TR-2022-26 | October 2022
  
  Published by Microsoft
  
  Publication Project
- Regex Matching with Counting-Set Automata
  
  Margus Veanes (margus), Lukas Holik, Ondrej Lengal, Olli Saarikivi (olsaarik), Lenka Turonova, Tomas Vojnar
  
  MSR-TR-2020-31 | September 2020
  
  Published by Microsoft
  
  The technical report includes detailed proofs of most of the theorems stated in the conference OOPSLA'2020 paper.
  
  DOI Project
- Symbolic Boolean Derivatives for Efficiently Solving Extended Regular Expression Constraints
  
  Caleb Stanford, Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2020-25 | August 2020
  
  Published by Microsoft
  
  Updated November 2020. Extended version of paper in PLDI'2021.
  
  Publication Author's Version Project
- Niijima: sound and automated computation consolidation for efficient multilingual data-parallel pipelines
  
  Guoqing Harry Xu, Margus Veanes (margus), Michael Barnett, Madan Musuvathi (madanm), Todd Mytkowicz (toddm), Ben Zorn (zorn), Huan He, Haibo Lin
  
  Proceedings of the 27th ACM Symposium on Operating Systems Principles | October 2019
  
  Publication DOI
- Symbolic Regex Matcher
  
  Margus Veanes (margus), Olli Saarikivi (olsaarik), Tiki Wan, Eric Xu
  
  TACAS | April 2019
  
  Author's Version Project
- Simulation Algorithms for Symbolic Automata
  
  Lukáš Holík, Ondřej Lengál, Juraj Síč, Margus Veanes, Tomáš Vojnar
  
  International Symposium on Automated Technology for Verification and Analysis (ATVA) | September 2018
  
  Editor(s): Lahiri, S. and Wang, C.
  
  DOI
- Theoretical Aspects of Symbolic Automata
  
  Hellis Tamm, Margus Veanes
  
  44th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'18) | January 2018
  
  Publication Project
- The power of symbolic automata and transducers
  
  Loris D'Antoni, Margus Veanes
  
  Computer Aided Verification, 29th International Conference (CAV'17) | July 2017
  
  Publication Project
- Minimization of Symbolic Transducers
  
  Olli Saarikivi, Margus Veanes
  
  Computer Aided Verification, 29th International Conference (CAV 2017) | July 2017
  
  Publication Project
- Fusing Effectful Comprehensions
  
  Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi
  
  ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017) | June 2017
  
  Publication Project
- Monadic Decomposition
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  Journal of the ACM | May 2017, Vol 64
  
  Publication Publication Publication Project
- Forward Bisimulations for Nondeterministic Symbolic Finite Automata
  
  Loris D'Antoni, Margus Veanes
  
  TACAS | April 2017
  
  Publication Project
- Translating C# to Branching Symbolic Transducers
  
  Olli Saarikivi, Margus Veanes
  
  LPAR-21: 21ST INTERNATIONAL CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING (Selected Workshop and Short Presentations) | March 2017
  
  Publication Project
- Monadic Second-Order Logic on Finite Sequences
  
  Loris D'Antoni, Margus Veanes
  
  POPL'2017 | January 2017
  
  Publication Publication Project
- Prepose: Privacy, Security, and Reliability for Gesture-Based Programming
  
  Lucas Silva Figueiredo, David Molnar, Margus Veanes, Ben Livshits
  
  IEEE Journal of Security and Privacy | December 2016
  
  Publication
- Fusing Effectful Comprehensions
  
  Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi
  
  MSR-TR-2016-55 | October 2016
  
  Publication
- Minimization of Symbolic Tree Automata
  
  Margus Veanes
  
  LICS | July 2016
  
  LICS
  
  Publication
- Fast: A Transducer-Based Language for Tree Manipulation
  
  Loris D’antoni, Margus Veanes, Ben Livshits, David Molnar
  
  ACM Transactions on Programming Languages and Systems (TOPLAS), 2015 | October 2015
  
  Publication Publication
- FAST: A Transducer-Based Language for Tree Manipulation
  
  Lori D'Antoni, Margus Veanes, Ben Livshits, David Molnar
  
  ACM Transactions on Programming Languages and Systems (TOPLAS) | October 2015, Vol 38
  
  Publication Publication
- Symbolic String Transformations with Regular Lookahead and Rollback
  
  Margus Veanes
  
  PSI 2014 | February 2015
  
  Publication Publication
- Program Boosting: Program Synthesis via Crowd-Sourcing
  
  Robert A Cochran, Loris D’Antoni, Ben Livshits, David Molnar, Margus Veanes
  
  Symposium on the Principles of Programming Languages (POPL) | January 2015
  
  Publication Publication
- Data-Parallel String-Manipulating Programs
  
  Margus Veanes, Todd Mytkowicz, David Molnar, Ben Livshits
  
  Symposium on the Principles of Programming Languages (POPL), Mumbai, India | January 2015
  
  Publication Publication
- Program Boosting: Program Synthesis via Crowd-Sourcing
  
  Robert A Cochran, , Benjamin Livshits, David Molnar, Margus Veanes, Ben Livshits
  
  POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2015
  
  Publication Publication
- Skolemization Modulo Theories
  
  Konstantin Korovin, Margus Veanes
  
  ICMS'14 | August 2014
  
  Publication Publication
- Monadic Decomposition
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  CAV'14 | July 2014
  
  Publication
- FAST: A Transducer-Based Language for Tree Manipulation
  
  Margus Veanes, Benjamin Livshits, David Molnar, Ben Livshits
  
  PLDI 2014: Programming Language Design and Implementation | June 2014
  
  Publication
- Minimization of Symbolic Automata
  
  Loris D'Antoni, Margus Veanes
  
  POPL'14 | January 2014
  
  POPL'14
  
  Publication Project
- FAST: A Transducer-Based Language for Tree Manipulation
  
  Loris D'Antoni, Margus Veanes, Ben Livshits, David Molnar,
  
  MSR-TR-2013-121 | November 2013
  
  Publication
- Equivalence of Extended Symbolic Finite Transducers
  
  Loris D'Antoni, Margus Veanes,
  
  25th International Conference on Computer Aided Verification (CAV'13) | July 2013
  
  The associated TR is an extended version of the conference paper.
  
  Publication
- Applications of Symbolic Finite Automata
  
  Margus Veanes
  
  CIAA'13 | July 2013
  
  Publication Project
- Minimization of Symbolic Automata
  
  Margus Veanes
  
  MSR-TR-2013-48 | April 2013
  
  Publication
- Static Analysis of String Encoders and Decoders
  
  Margus Veanes, Loris D'Antoni
  
  VMCAI 2013 | January 2013
  
  Publication
- Equivalence of Extended Symbolic Finite Transducers
  
  Loris D'Antoni, Margus Veanes,
  
  MSR-TR-2013-4 | January 2013
  
  Publication
- Symbolic Automata: The Toolkit
  
  Margus Veanes, Nikolaj Bjørner
  
  TACAS'12 | March 2012
  
  Publication
- Symbolic Finite State Transducers: Algorithms and Applications
  
  Margus Veanes, Pieter Hooimeijer, David Molnar, Nikolaj Bjorner, Ben Livshits
  
  POPL'12 | January 2012
  
  Publication
- Generating Fast String Manipulating Code Through Transducer Exploration and SIMD Integration
  
  Margus Veanes, David Molnar, Ben Livshits, Lubomir Litchev
  
  MSR-TR-2011-124 | November 2011
  
  Publication
- Alternating simulation and IOCO
  
  Margus Veanes, Nikolaj Bjørner
  
  International Journal on Software Tools for Technology Transfer (STTT) | September 2011
  
  Publication Publication
- Fast and Precise Sanitizer Analysis with BEK
  
  Pieter Hooimeijer, Ben Livshits, David Molnar, Prateek Saxena, Margus Veanes,
  
  USENIX Security'11 | August 2011
  
  USENIX Security'11
  
  Publication
- Decision Procedures for Composition and Equivalence of Symbolic Finite State Transducers
  
  Margus Veanes, David Molnar, Ben Livshits
  
  MSR-TR-2011-32 | March 2011
  
  Publication
- Symbolic Transducers
  
  Nikolaj Bjørner, Margus Veanes
  
  MSR-TR-2011-3 | January 2011
  
  Publication
- Symbolic Tree Transducers
  
  Margus Veanes, Nikolaj Bjørner
  
  Ershov Informatics Conference (PSI'11) | January 2011
  
  Publication
- BEK: Modeling Imperative String Operations with Symbolic Transducers
  
  , Ben Livshits, David Molnar, Prateek Saxena, Margus Veanes
  
  MSR-TR-2010-154 | November 2010
  
  Publication
- Composing Model Programs for Analysis
  
  Margus Veanes, Jonathan Jacky
  
  The Journal of Logic and Algebraic Programming | October 2010, Vol 79: pp. 467-482
  
  Publication Publication
- An Evaluation of Automata Algorithms for String Analysis
  
  , Margus Veanes
  
  MSR-TR-2010-90 | July 2010
  
  Updated August, 2010
  
  Publication Project
- Modeling Imperative String Operations with Transducers
  
  Pieter Hooimeijer, David Molnar, Prateek Saxena, Margus Veanes
  
  MSR-TR-2010-96 | July 2010
  
  Publication
- Rex: Symbolic Regular Expression Explorer
  
  Margus Veanes, Jonathan "Peli" de Halleux, Nikolai Tillmann
  
  Third International Conference on Software Testing, Verification and Validation (ICST) | April 2010
  
  Publication Publication Project Project Project
- Alternating Simulation and IOCO
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2010-38 | April 2010
  
  Extended version of paper with the same title in ICTSS 2010, LNCS vol 6435
  
  Publication
- Qex: Symbolic SQL Query Explorer
  
  Margus Veanes, Nikolai Tillmann, Jonathan "Peli" de Halleux
  
  LPAR-16 | April 2010
  
  Publication Publication Project
- Symbolic Query Exploration
  
  Margus Veanes, Pavel Grigorenko, Jonathan "Peli" de Halleux, Nikolai Tillmann
  
  ICFEM'09 | December 2009
  
  Publication Project
- Solving Extended Regular Constraints Symbolically
  
  Margus Veanes, Nikolaj Bjørner, Leonardo de Moura
  
  MSR-TR-2009-177 | December 2009
  
  Publication Project
- Model-Based Testing of Web Applications using NModel
  
  Juhan Ernits, Rivo Roo, Jonathan Jacky, Margus Veanes
  
  LNCS, TESTCOM/FATES 2009 | November 2009
  
  Publication Publication
- Rex: Symbolic Regular Expression Explorer
  
  Margus Veanes, Jonathan "Peli" de Halleux, Nikolai Tillmann
  
  MSR-TR-2009-137 | October 2009
  
  ICST'10
  
  Publication Publication Project
- Qex: Symbolic SQL Query Explorer
  
  Margus Veanes, Jonathan de Halleux, Nikolai Tillmann, Jonathan "Peli" de Halleux
  
  MSR-TR-2009-2015 | October 2009
  
  Updated January 2010
  
  Publication Project
- Symbolic Bounded Model Checking of Abstract State Machines
  
  Margus Veanes, Nikolaj Bjørner, Yuri Gurevich, Wolfram Schulte
  
  Int J Software Informatics | June 2009, pp. 149-170
  
  Publication Project
- Input-Output Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-56 | May 2009
  
  Preliminary version of paper to appear in ICTAC'09, LNCS.
  
  Publication
- Symbolic Query Exploration
  
  Margus Veanes, Pavel Grigorenko, Jonathan "Peli" de Halleux, Nikolai Tillmann
  
  MSR-TR-2009-65 | May 2009
  
  Publication Project Project
- Symbolic Bounded Conformance Checking of Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-28 | March 2009
  
  This is an extended version of a paper to appear in PSI'09, LNCS.
  
  Publication Project
- Arranging Partitures for Models and Theorems
  
  Johannes Helander, Margus Veanes
  
  MSR-TR-2009-24 | March 2009
  
  Publication
- On Bounded Reachability of Programs with Set Comprehensions
  
  Margus Veanes, Ando Saabas
  
  LPAR'08 | November 2008
  
  LPAR'08
  
  Publication Project
- Protocol Modeling with Model Program Composition
  
  Margus Veanes, Wolfram Schulte
  
  FORTE'08 | June 2008
  
  ISBN: 978-3-540-68854-9
  
  Publication
- An SMT Approach to Bounded Reachability Analysis of Model Programs
  
  Margus Veanes, Nikolaj Bjørner, Alexander Raschke
  
  FORTE'08 | June 2008
  
  FORTE'08
  
  Publication Project Project
- Model-Based Testing of Robots with NModel
  
  Juhan Ernits, Margus Veanes, Johannes Helander
  
  TestCom/FATES 2008 Short Papers | June 2008
  
  TestCom/FATES 2008 Short Papers
  
  Publication
- Bounded reachability of model programs
  
  Margus Veanes, Ando Saabas, Nikolaj Bjørner
  
  MSR-TR-2008-81 | May 2008
  
  Parts of this report are presented at FORTE'08 and LPAR'08.
  
  Publication Project
- Enabling the Future Auto with Model-Driven Services
  
  Johannes Helander, Margus Veanes
  
  National Workshop on High-Confidence Automotive Cyber-Physical Systems. | April 2008
  
  Publication
- Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer
  
  Margus Veanes, Colin Campbell, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, Lev Nachmanson
  
  Formal Methods and Testing | Published by Springer Verlag | 2008, Vol 4949
  
  ISBN: 978-3-540-78916-1
  
  The attached file is a preliminary version.
  
  Publication Project Project Project
- Model-Based Software Testing and Analysis with C#
  
  Jonathan Jacky, Margus Veanes, Colin Campbell, Wolfram Schulte
  
  Published by Cambridge University Press | January 2008
  
  ISBN: 9.78052E+12
  
  Publication
- Adapting Futures: Scalability for Real-World Computing
  
  Johannes Helander, Risto Serg, Margus Veanes, Pritam Roy
  
  RTSS'07 | December 2007
  
  Publication Publication
- Composition of Model Programs
  
  Margus Veanes, Colin Campbell, Wolfram Schulte
  
  FORTE | June 2007
  
  ISBN: 978-3-540-73195-5
  
  Publication Project
- State Isomorphism in Model Programs with Abstract Data Structures
  
  Margus Veanes, Juhan Ernits, Colin Campbell
  
  FORTE'07 | June 2007
  
  Publication Project
- Can Abstract State Machines Be Useful in Language Theory?
  
  Yuri Gurevich, Margus Veanes, Charles Wallace
  
  Theoretical Computer Science | January 2007, Vol 376: pp. 17-29
  
  Publication Project
- Online Testing with Reinforcement Learning
  
  Margus Veanes, Pritam Roy, Colin Campbell
  
  Formal Approaches to Software Testing and Runtime Verification, FATES/RV 2006 | January 2006
  
  Publication
- Action Machines – Towards a Framework for Model Composition, Exploration and Conformance Testing Based on Symbolic Computation
  
  Nikolai Tillmann, Wolfram Schulte, Margus Veanes
  
  Quality Software, 2005. (QSIC 2005). Fifth International Conference on | September 2005
  
  Quality Software, 2005. (QSIC 2005). Fifth International Conference on
  
  ISBN: 0-7695-2399-4
  
  Publication Project
- Play to Test
  
  Andreas Blass, Yuri Gurevich, Lev Nachmanson, Margus Veanes
  
  FATES 2005 | July 2005
  
  Publication Project Project
- Multiplexing of Partially Ordered Events
  
  Colin Campbell, Margus Veanes, Jiale Huo, Alexandre Petrenko
  
  TestCom 2005 | June 2005
  
  Received Best paper award.
  
  Publication Project
- Play to Test
  
  Andreas Blass, Yuri Gurevich, Lev Nachmanson, Margus Veanes
  
  MSR-TR-2005-04 | January 2005
  
  A short version appears in: FATES 2005, LNCS vol. 3997, pp. 32-46
  
  Publication Project
- Online testing with model programs
  
  Margus Veanes, Colin Campbell, Wolfram Schulte, Nikolai Tillmann
  
  ESEC/SIGSOFT FSE | January 2005
  
  ESEC/SIGSOFT FSE
  
  ISBN: 1-59593-014-0
  
  Publication Project Project
- Testing Concurrent Object-Oriented Systems with Spec Explorer
  
  Colin Campbell, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  January 2005
  
  ISBN: 3-540-27882-6
  
  Publication Project Project Project
- Exploration with Multiple State Groupings
  
  Colin Campbell, Margus Veanes
  
  Abstract State Machines 2005 | January 2005
  
  Publication Project Project
- On-The-Fly Testing of Reactive Systems
  
  Margus Veanes, Colin Campbell, Wolfram Schulte, Pushmeet Kohli
  
  MSR-TR-2005-05 | January 2005
  
  Publication Project
- Optimal Strategies for Testing Nondeterministic Systems
  
  Lev Nachmanson, Margus Veanes, Wolfram Schulte, Nikolai Tillmann, Wolfgang Grieskamp
  
  ISSTA 2004 | January 2004
  
  ISBN: 1-58113-820-2
  
  Publication Project Project
- Instrumenting Scenarios in a Model-Driven Development Environment
  
  Wolfgang Grieskamp, Nikolai Tillmann, Margus Veanes
  
  Journal of Information and Software Technology | January 2004, Vol 46: pp. 1027-1036
  
  Publication Project Project Project
- Towards a Tool Environment for Model-Based Testing with AsmL
  
  Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  FATES 2003 | January 2004
  
  Publication Project Project Project
- Scenario-oriented Modeling in AsmL and its Instrumentation for Testing
  
  Mike Barnett, Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  Proc. of 2nd International Workshop on Scenarios and State Machines: Models, Algorithms, and Tools held at ICSE 2003, International Conference on Software Engineering 2003 | January 2003
  
  Publication
- Validating Use-Cases with the AsmL Test Tool
  
  Wolfram Schulte, Nikolai Tillmann, Margus Veanes, Mike Barnett
  
  QSIC | January 2003
  
  QSIC
  
  ISBN: 0-7695-2015-4
  
  Publication Project Project
- Model-Based Testing with AsmL .NET
  
  Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  1st European Conference on Model-Driven Software Engineering | January 2003
  
  Publication Project Project Project
- Combined Algorithm for Approximating a Finite State Abstraction of a Large System
  
  Rostislav Yavorsky, Margus Veanes
  
  ICSE 2003/Scenarios Workshop | January 2003
  
  ICSE 2003/Scenarios Workshop
  
  Publication Project Project
- Generating finite state machines from abstract state machines
  
  Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
  
  ISSTA 2002 | July 2002
  
  Publication Project Project
- An Abstract Communication Model
  
  Uwe Glässer, Yuri Gurevich, Margus Veanes
  
  MSR-TR-2002-55 | May 2002
  
  Publication Publication Project
- Universal Plug and Play Machine Models: Modeling with Distributed Abstract State Machines
  
  Uwe Glässer, Margus Veanes
  
  Design and Analysis of Distributed Embedded Systems, IFIP 17th World Computer Congress (DIPES 2002) | January 2002
  
  Publication Project
- High-level Executable Specification of the Universal Plug and Play Architecture
  
  Uwe Glässer, Yuri Gurevich, Margus Veanes
  
  HICSS 2002 | January 2002
  
  Publication Project
- On the Undecidability of Second-Order Unification
  
  Jordi Levy, Margus Veanes
  
  Information and Computation | January 2000, Vol 159: pp. 125-150
  
  Publication Publication
- Logic with Equality: Partisan Corroboration and Shifted Pairing
  
  Yuri Gurevich, Margus Veanes
  
  August 1999
  
  Publication Publication
- The relation between second-order unification and simultaneous rigid E-unification
  
  Margus Veanes
  
  Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS'98) | June 1998
  
  Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS'98)
  
  Publication
- The Relation Between Second-Order Unification and Simultaneous Rigid E-Unification
  
  Margus Veanes
  
  MPI-I-98-2-005 | February 1998
  
  Publication
- Rigid Reachability
  
  Harald Ganzinger, Florent Jacquemard, Margus Veanes
  
  Proceedings of the 4th Asian Computing Science Conference on Advances in Computing Science (ASIAN 98) | January 1998
  
  Publication
- On Unification Problems in Restricted Second-Order Languages
  
  Jordi Jevy, Margus Veanes
  
  Annual Conference of the European Association for Computer Science Logic, CSL'98 | January 1998
  
  Annual Conference of the European Association for Computer Science Logic, CSL'98
  
  Appears in preliminary proceedings of CSL'98
  
  Publication
- The Decidability of Simultaneous Rigid E-Unification with One Variable
  
  Paliath Narendran, Margus Veanes, Andrei Voronkov, Anatoli Degtyarev, Yuri Gurevich
  
  RTA'98 | January 1998
  
  Publication
- Some undecidable problems related to the Herbrand theorem
  
  Yuri Gurevich, Margus Veanes
  
  UPMAIL-TR-138 | March 1997
  
  Publication
- The undecidability of simultaneous rigid E-unification with two variables
  
  Margus Veanes
  
  5th Kurt GÃ¶del Colloquium (KGC'97) | January 1997
  
  Publication
- Natural cycletrees: Flexible interconnection graphs
  
  Margus Veanes, Jonas Barklund
  
  Journal of Parallel and Distributed Computing | January 1996, Vol 33: pp. 44-54
  
  Publication Publication
- Cycletrees: a Novel Class of Interconnection Graphs
  
  Margus Veanes
  
  January 1993
  
  January 1993
  
  Publication
- Symbolic Automata: Omega-Regularity Modulo Theories
  
  Margus Veanes, Thomas Ball, Gabriel Ebner, Ekaterina Zhuchko
  
  POPL | January 2025
  
  Author's Version DOI Project
- RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement, and Restricted Lookarounds
  
  Ian Erik Varatalu, Margus Veanes, Juhan Ernits
  
  POPL | January 2025
  
  DOI Author's Version Project
- Incremental Dead State Detection in Logarithmic Time
  
  Caleb Stanford , Margus Veanes
  
  January 2023
  
  Preliminary and extended version of paper that appears in CAV 2023
  
  DOI
- Simulation Algorithms for Symbolic Automata
  
  Lukáš Holík, Ondřej Lengál, Juraj Síč, Margus Veanes, Tomáš Vojnar
  
  International Symposium on Automated Technology for Verification and Analysis (ATVA) | September 2018
  
  Editor(s): Lahiri, S. and Wang, C.
  
  DOI
- Monadic Second-Order Logic on Finite Sequences
  
  Loris D'Antoni, Margus Veanes
  
  POPL'2017 | January 2017
  
  Publication Publication Project
- Minimization of Symbolic Tree Automata
  
  Margus Veanes
  
  LICS | July 2016
  
  LICS
  
  Publication
- Extended symbolic finite automata and transducers
  
  Loris D’Antoni, Margus Veanes
  
  Formal Methods in System Design | July 2015
  
  Publication
- Symbolic Tree Automata
  
  Margus Veanes, Nikolaj Bjørner
  
  Information Processing Letters | March 2015, Vol 115(3): pp. 418-424
  
  Publication Publication
- Symbolic String Transformations with Regular Lookahead and Rollback
  
  Margus Veanes
  
  PSI 2014 | February 2015
  
  Publication Publication
- Data-Parallel String-Manipulating Programs
  
  Margus Veanes, Todd Mytkowicz, David Molnar, Ben Livshits
  
  POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2015
  
  POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
  
  Publication Publication Project Project
- Program Boosting: Program Synthesis via Crowd-Sourcing
  
  Robert A Cochran, , Benjamin Livshits, David Molnar, Margus Veanes, Ben Livshits
  
  POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2015
  
  Publication Publication
- Skolemization Modulo Theories
  
  Konstantin Korovin, Margus Veanes
  
  ICMS'14 | August 2014
  
  Publication Publication
- Monadic Decomposition
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  CAV'14 | July 2014
  
  Publication
- FAST: A Transducer-Based Language for Tree Manipulation
  
  Margus Veanes, Benjamin Livshits, David Molnar, Ben Livshits
  
  PLDI 2014: Programming Language Design and Implementation | June 2014
  
  Publication
- Minimization of Symbolic Automata
  
  Loris D'Antoni, Margus Veanes
  
  POPL'14 | January 2014
  
  POPL'14
  
  Publication Project
- Effectively Monadic Predicates
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  LPAR-19 | December 2013
  
  Publication
- Equivalence of Extended Symbolic Finite Transducers
  
  Loris D'Antoni, Margus Veanes,
  
  25th International Conference on Computer Aided Verification (CAV'13) | July 2013
  
  The associated TR is an extended version of the conference paper.
  
  Publication
- Applications of Symbolic Finite Automata
  
  Margus Veanes
  
  CIAA'13 | July 2013
  
  Publication Project
- Minimization of Symbolic Automata
  
  Margus Veanes
  
  MSR-TR-2013-48 | April 2013
  
  Publication
- Static Analysis of String Encoders and Decoders
  
  Margus Veanes, Loris D'Antoni
  
  VMCAI 2013 | January 2013
  
  Publication
- Equivalence of Extended Symbolic Finite Transducers
  
  Loris D'Antoni, Margus Veanes,
  
  MSR-TR-2013-4 | January 2013
  
  Publication
- Symbolic Finite State Transducers: Algorithms and Applications
  
  Margus Veanes, Pieter Hooimeijer, David Molnar, Nikolaj Bjorner, Ben Livshits
  
  POPL'12 | January 2012
  
  Publication
- Alternating simulation and IOCO
  
  Margus Veanes, Nikolaj Bjørner
  
  International Journal on Software Tools for Technology Transfer (STTT) | September 2011
  
  Publication Publication
- Symbolic Finite State Transducers: Algorithms and Applications
  
  Nikolaj Bjørner, Ben Livshits, David Molnar, Margus Veanes
  
  MSR-TR-2011-85 | July 2011
  
  Publication
- Decision Procedures for Composition and Equivalence of Symbolic Finite State Transducers
  
  Margus Veanes, David Molnar, Ben Livshits
  
  MSR-TR-2011-32 | March 2011
  
  Publication
- Symbolic Tree Transducers
  
  Margus Veanes, Nikolaj Bjørner
  
  Ershov Informatics Conference (PSI'11) | January 2011
  
  Publication
- Symbolic Bounded Model Checking of Abstract State Machines
  
  Margus Veanes, Nikolaj Bjørner, Yuri Gurevich, Wolfram Schulte
  
  Int J Software Informatics | June 2009, pp. 149-170
  
  Publication Project
- Input-Output Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-56 | May 2009
  
  Preliminary version of paper to appear in ICTAC'09, LNCS.
  
  Publication
- Symbolic Bounded Conformance Checking of Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-28 | March 2009
  
  This is an extended version of a paper to appear in PSI'09, LNCS.
  
  Publication Project
- Counting in Regexes Considered Harmful: Exposing ReDoS Vulnerability of Nonbacktracking Matchers
  
  Lenka Turoňová, Lukáš Holík, Ivan Homoliak, Ondřej Lengál, Margus Veanes, Tomáš Vojnar
  
  31st USENIX Security Symposium | August 2022
  
  Publication
- Prepose: Privacy, Security, and Reliability for Gesture-Based Programming
  
  Lucas Silva Figueiredo , David Molnar, Margus Veanes, Benjamin Livshits
  
  IEEE Security & Privacy | April 2017, Vol 15: pp. 14-23
  
  Publication Publication
- Prepose: Privacy, Security, and Reliability for Gesture-Based Programming
  
  Lucas Silva Figueiredo, David Molnar, Margus Veanes, Ben Livshits
  
  IEEE Journal of Security and Privacy | December 2016
  
  Publication
- PrePose: Security and Privacy for Gesture-Based Programming
  
  Lucas Silva Figueiredo, Ben Livshits, David Molnar, Margus Veanes
  
  MSR-TR-2014-146 | November 2014
  
  Publication
- Symbolic Finite State Transducers: Algorithms and Applications
  
  Margus Veanes, Pieter Hooimeijer, David Molnar, Nikolaj Bjorner, Ben Livshits
  
  POPL'12 | January 2012
  
  Publication
- Generating Fast String Manipulating Code Through Transducer Exploration and SIMD Integration
  
  Margus Veanes, David Molnar, Ben Livshits, Lubomir Litchev
  
  MSR-TR-2011-124 | November 2011
  
  Publication
- Fast and Precise Sanitizer Analysis with BEK
  
  Pieter Hooimeijer, Ben Livshits, David Molnar, Prateek Saxena, Margus Veanes,
  
  USENIX Security'11 | August 2011
  
  USENIX Security'11
  
  Publication
- Decision Procedures for Composition and Equivalence of Symbolic Finite State Transducers
  
  Margus Veanes, David Molnar, Ben Livshits
  
  MSR-TR-2011-32 | March 2011
  
  Publication
- Symbolic Transducers
  
  Nikolaj Bjørner, Margus Veanes
  
  MSR-TR-2011-3 | January 2011
  
  Publication
- BEK: Modeling Imperative String Operations with Symbolic Transducers
  
  , Ben Livshits, David Molnar, Prateek Saxena, Margus Veanes
  
  MSR-TR-2010-154 | November 2010
  
  Publication
- The decidability of simultaneous rigid E-unification with one variable
  
  Paliath Narendran, Margus Veanes, Andrei Voronkov, Anatoli Degtyarev, Yuri Gurevich
  
  139 | April 1997
  
  Publication
- Theoretical Aspects of Symbolic Automata
  
  Hellis Tamm, Margus Veanes
  
  44th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'18) | January 2018
  
  Publication Project
- Program Boosting: Program Synthesis via Crowd-Sourcing
  
  Robert A Cochran, , Benjamin Livshits, David Molnar, Margus Veanes, Ben Livshits
  
  POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2015
  
  Publication Publication
- PrePose: Security and Privacy for Gesture-Based Programming
  
  Lucas Silva Figueiredo, Ben Livshits, David Molnar, Margus Veanes
  
  MSR-TR-2014-146 | November 2014
  
  Publication
- Data-Parallel String-Manipulating Programs
  
  Margus Veanes, David Molnar, Todd Mytkowicz, Ben Livshits
  
  MSR-TR-2012-72 | July 2012
  
  Publication Project Project
- The Two-Variable Guarded Fragment with Transitive Relations
  
  Harald Ganzinger, Christoph Meyer, Margus Veanes
  
  LICS 1999 | January 1999
  
  Publication
- Uniform representation of recursively enumerable sets with simultaneous rigid E-unification
  
  Margus Veanes
  
  126 | June 1996
  
  Publication
- Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract)
  
  Margus Veanes, Ando Saabas
  
  ABZ'08 | September 2008
  
  This is an extended abstract.
  
  Publication Publication Project
- Toward Industrial Strength Abstract State Machines
  
  Yuri Gurevich, Wolfram Schulte, Margus Veanes
  
  MSR-TR-2001-98 | October 2001
  
  Publication Project
- On the number of edges in cycletrees
  
  Margus Veanes, Jonas Barklund
  
  Information Processing Letters | January 1996, Vol 57: pp. 225-229
  
  Publication Publication
- Enabling the Future Auto with Model-Driven Services
  
  Johannes Helander, Margus Veanes
  
  National Workshop on High-Confidence Automotive Cyber-Physical Systems. | April 2008
  
  Publication
- Embedded Systems Research at DemoFest’07
  
  Oscar Almeida, Alessandro Forin, Philip Garcia, Johannes Helander, Nishith Khantal, Hong Lu, Karl Meier, Sibin Mohan, Henrik Frystyk Nielsen, Neil Pittman, Risto Serg, Bharat Sukhwani, Margus Veanes, Ben Zorn, Sarah Berry, Chris Boyce, David Chaszar, Brandon Culrich, Mikhail Kisin, Gabe Knezek, Warren Linam-Church, Steve Liu, Michael Stewart, Doug Toney
  
  MSR-TR-2007-94 | July 2007
  
  Publication Publication
- Abstract Communication Model for Distributed Systems
  
  Uwe Glässer, Yuri Gurevich, Margus Veanes
  
  IEEE Transactions on Software Engineering | July 2004, Vol 30(7): pp. 458-472
  
  Publication Project Project
- On-The-Fly Testing of Reactive Systems
  
  Margus Veanes, Colin Campbell, Wolfram Schulte, Pushmeet Kohli
  
  MSR-TR-2005-05 | January 2005
  
  Publication Project

- Conformance Testing with Abstract State Machines
  
  Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
  
  EUROCAST 2001 | February 2001
  
  Publication Project
- Using Abstract State Machines at Microsoft: A Case Study
  
  Yuri Gurevich, Wolfram Schulte, Margus Veanes, Mike Barnett
  
  Abstract State Machines | January 2000
  
  Abstract State Machines
  
  ISBN: 3-540-67959-6
  
  Publication Project
- Logic with Equality: Partisan Corroboration and Shifted Pairing
  
  Yuri Gurevich, Margus Veanes
  
  August 1999
  
  Publication Publication
- Decidable Fragments of Simultaneous Rigid Reachability
  
  Véronique Cortier, Harald Ganzinger, Florent Jacquemard, Margus Veanes
  
  ICALP 1999 | January 1999
  
  Publication
- The Two-Variable Guarded Fragment with Transitive Relations
  
  Harald Ganzinger, Christoph Meyer, Margus Veanes
  
  LICS 1999 | January 1999
  
  Publication
- The relation between second-order unification and simultaneous rigid E-unification
  
  Margus Veanes
  
  Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS'98) | June 1998
  
  Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS'98)
  
  Publication
- Rigid Reachability
  
  Harald Ganzinger, Florent Jacquemard, Margus Veanes
  
  Proceedings of the 4th Asian Computing Science Conference on Advances in Computing Science (ASIAN 98) | January 1998
  
  Publication
- On Unification Problems in Restricted Second-Order Languages
  
  Jordi Jevy, Margus Veanes
  
  Annual Conference of the European Association for Computer Science Logic, CSL'98 | January 1998
  
  Annual Conference of the European Association for Computer Science Logic, CSL'98
  
  Appears in preliminary proceedings of CSL'98
  
  Publication
- The Decidability of Simultaneous Rigid E-Unification with One Variable
  
  Paliath Narendran, Margus Veanes, Andrei Voronkov, Anatoli Degtyarev, Yuri Gurevich
  
  RTA'98 | January 1998
  
  Publication
- The undecidability of simultaneous rigid E-unification with two variables
  
  Margus Veanes
  
  5th Kurt GÃ¶del Colloquium (KGC'97) | January 1997
  
  Publication
- Regex Decision Procedures in Extended RE#
  
  Ian Erik Varatalu, Margus Veanes, Ekaterina Zhuchko, Juhan Ernits
  
  CAV 2025 | July 2025
  
  Editor(s): R. Piskac and Z. Rakamaric
  
  Published in LNCS vol. 15933
  
  DOI Project
- Symbolic Automata: Omega-Regularity Modulo Theories
  
  Margus Veanes, Thomas Ball, Gabriel Ebner, Ekaterina Zhuchko
  
  POPL | January 2025
  
  Author's Version DOI Project
- RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement, and Restricted Lookarounds
  
  Ian Erik Varatalu, Margus Veanes, Juhan Ernits
  
  POPL | January 2025
  
  DOI Author's Version Project
- Lean Formalization of Extended Regular Expression Matching with Lookarounds
  
  Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner
  
  CPP | January 2024
  
  Author's Version DOI Project
- Counting in Regexes Considered Harmful: Exposing ReDoS Vulnerability of Nonbacktracking Matchers
  
  Lenka Turoňová, Lukáš Holík, Ivan Homoliak, Ondřej Lengál, Margus Veanes, Tomáš Vojnar
  
  31st USENIX Security Symposium | August 2022
  
  Publication
- Niijima: sound and automated computation consolidation for efficient multilingual data-parallel pipelines
  
  Guoqing Harry Xu, Margus Veanes (margus), Michael Barnett, Madan Musuvathi (madanm), Todd Mytkowicz (toddm), Ben Zorn (zorn), Huan He, Haibo Lin
  
  Proceedings of the 27th ACM Symposium on Operating Systems Principles | October 2019
  
  Publication DOI
- Symbolic Regex Matcher
  
  Margus Veanes (margus), Olli Saarikivi (olsaarik), Tiki Wan, Eric Xu
  
  TACAS | April 2019
  
  Author's Version Project
- Simulation Algorithms for Symbolic Automata
  
  Lukáš Holík, Ondřej Lengál, Juraj Síč, Margus Veanes, Tomáš Vojnar
  
  International Symposium on Automated Technology for Verification and Analysis (ATVA) | September 2018
  
  Editor(s): Lahiri, S. and Wang, C.
  
  DOI
- Theoretical Aspects of Symbolic Automata
  
  Hellis Tamm, Margus Veanes
  
  44th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'18) | January 2018
  
  Publication Project
- The power of symbolic automata and transducers
  
  Loris D'Antoni, Margus Veanes
  
  Computer Aided Verification, 29th International Conference (CAV'17) | July 2017
  
  Publication Project
- Minimization of Symbolic Transducers
  
  Olli Saarikivi, Margus Veanes
  
  Computer Aided Verification, 29th International Conference (CAV 2017) | July 2017
  
  Publication Project
- Fusing Effectful Comprehensions
  
  Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi
  
  ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017) | June 2017
  
  Publication Project
- Forward Bisimulations for Nondeterministic Symbolic Finite Automata
  
  Loris D'Antoni, Margus Veanes
  
  TACAS | April 2017
  
  Publication Project
- Translating C# to Branching Symbolic Transducers
  
  Olli Saarikivi, Margus Veanes
  
  LPAR-21: 21ST INTERNATIONAL CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING (Selected Workshop and Short Presentations) | March 2017
  
  Publication Project
- Monadic Second-Order Logic on Finite Sequences
  
  Loris D'Antoni, Margus Veanes
  
  POPL'2017 | January 2017
  
  Publication Publication Project
- Minimization of Symbolic Tree Automata
  
  Margus Veanes
  
  LICS | July 2016
  
  LICS
  
  Publication
- Fast: A Transducer-Based Language for Tree Manipulation
  
  Loris D’antoni, Margus Veanes, Ben Livshits, David Molnar
  
  ACM Transactions on Programming Languages and Systems (TOPLAS), 2015 | October 2015
  
  Publication Publication
- Symbolic String Transformations with Regular Lookahead and Rollback
  
  Margus Veanes
  
  PSI 2014 | February 2015
  
  Publication Publication
- Program Boosting: Program Synthesis via Crowd-Sourcing
  
  Robert A Cochran, Loris D’Antoni, Ben Livshits, David Molnar, Margus Veanes
  
  Symposium on the Principles of Programming Languages (POPL) | January 2015
  
  Publication Publication
- Data-Parallel String-Manipulating Programs
  
  Margus Veanes, Todd Mytkowicz, David Molnar, Ben Livshits
  
  Symposium on the Principles of Programming Languages (POPL), Mumbai, India | January 2015
  
  Publication Publication
- Data-Parallel String-Manipulating Programs
  
  Margus Veanes, Todd Mytkowicz, David Molnar, Ben Livshits
  
  POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2015
  
  POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
  
  Publication Publication Project Project
- Program Boosting: Program Synthesis via Crowd-Sourcing
  
  Robert A Cochran, , Benjamin Livshits, David Molnar, Margus Veanes, Ben Livshits
  
  POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2015
  
  Publication Publication
- Skolemization Modulo Theories
  
  Konstantin Korovin, Margus Veanes
  
  ICMS'14 | August 2014
  
  Publication Publication
- Monadic Decomposition
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  CAV'14 | July 2014
  
  Publication
- FAST: A Transducer-Based Language for Tree Manipulation
  
  Margus Veanes, Benjamin Livshits, David Molnar, Ben Livshits
  
  PLDI 2014: Programming Language Design and Implementation | June 2014
  
  Publication
- Minimization of Symbolic Automata
  
  Loris D'Antoni, Margus Veanes
  
  POPL'14 | January 2014
  
  POPL'14
  
  Publication Project
- Effectively Monadic Predicates
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  LPAR-19 | December 2013
  
  Publication
- Equivalence of Extended Symbolic Finite Transducers
  
  Loris D'Antoni, Margus Veanes,
  
  25th International Conference on Computer Aided Verification (CAV'13) | July 2013
  
  The associated TR is an extended version of the conference paper.
  
  Publication
- Applications of Symbolic Finite Automata
  
  Margus Veanes
  
  CIAA'13 | July 2013
  
  Publication Project
- Static Analysis of String Encoders and Decoders
  
  Margus Veanes, Loris D'Antoni
  
  VMCAI 2013 | January 2013
  
  Publication
- Symbolic Automata: The Toolkit
  
  Margus Veanes, Nikolaj Bjørner
  
  TACAS'12 | March 2012
  
  Publication
- Symbolic Finite State Transducers: Algorithms and Applications
  
  Margus Veanes, Pieter Hooimeijer, David Molnar, Nikolaj Bjorner, Ben Livshits
  
  POPL'12 | January 2012
  
  Publication
- Fast and Precise Sanitizer Analysis with BEK
  
  Pieter Hooimeijer, Ben Livshits, David Molnar, Prateek Saxena, Margus Veanes,
  
  USENIX Security'11 | August 2011
  
  USENIX Security'11
  
  Publication
- Symbolic Tree Transducers
  
  Margus Veanes, Nikolaj Bjørner
  
  Ershov Informatics Conference (PSI'11) | January 2011
  
  Publication
- Rex: Symbolic Regular Expression Explorer
  
  Margus Veanes, Jonathan "Peli" de Halleux, Nikolai Tillmann
  
  Third International Conference on Software Testing, Verification and Validation (ICST) | April 2010
  
  Publication Publication Project Project Project
- Qex: Symbolic SQL Query Explorer
  
  Margus Veanes, Nikolai Tillmann, Jonathan "Peli" de Halleux
  
  LPAR-16 | April 2010
  
  Publication Publication Project
- Symbolic Query Exploration
  
  Margus Veanes, Pavel Grigorenko, Jonathan "Peli" de Halleux, Nikolai Tillmann
  
  ICFEM'09 | December 2009
  
  Publication Project
- Model-Based Testing of Web Applications using NModel
  
  Juhan Ernits, Rivo Roo, Jonathan Jacky, Margus Veanes
  
  LNCS, TESTCOM/FATES 2009 | November 2009
  
  Publication Publication
- On Bounded Reachability of Programs with Set Comprehensions
  
  Margus Veanes, Ando Saabas
  
  LPAR'08 | November 2008
  
  LPAR'08
  
  Publication Project
- Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract)
  
  Margus Veanes, Ando Saabas
  
  ABZ'08 | September 2008
  
  This is an extended abstract.
  
  Publication Publication Project
- Protocol Modeling with Model Program Composition
  
  Margus Veanes, Wolfram Schulte
  
  FORTE'08 | June 2008
  
  ISBN: 978-3-540-68854-9
  
  Publication
- An SMT Approach to Bounded Reachability Analysis of Model Programs
  
  Margus Veanes, Nikolaj Bjørner, Alexander Raschke
  
  FORTE'08 | June 2008
  
  FORTE'08
  
  Publication Project Project
- Model-Based Testing of Robots with NModel
  
  Juhan Ernits, Margus Veanes, Johannes Helander
  
  TestCom/FATES 2008 Short Papers | June 2008
  
  TestCom/FATES 2008 Short Papers
  
  Publication
- Enabling the Future Auto with Model-Driven Services
  
  Johannes Helander, Margus Veanes
  
  National Workshop on High-Confidence Automotive Cyber-Physical Systems. | April 2008
  
  Publication
- Adapting Futures: Scalability for Real-World Computing
  
  Johannes Helander, Risto Serg, Margus Veanes, Pritam Roy
  
  RTSS'07 | December 2007
  
  Publication Publication
- Composition of Model Programs
  
  Margus Veanes, Colin Campbell, Wolfram Schulte
  
  FORTE | June 2007
  
  ISBN: 978-3-540-73195-5
  
  Publication Project
- State Isomorphism in Model Programs with Abstract Data Structures
  
  Margus Veanes, Juhan Ernits, Colin Campbell
  
  FORTE'07 | June 2007
  
  Publication Project
- Online Testing with Reinforcement Learning
  
  Margus Veanes, Pritam Roy, Colin Campbell
  
  Formal Approaches to Software Testing and Runtime Verification, FATES/RV 2006 | January 2006
  
  Publication
- Action Machines – Towards a Framework for Model Composition, Exploration and Conformance Testing Based on Symbolic Computation
  
  Nikolai Tillmann, Wolfram Schulte, Margus Veanes
  
  Quality Software, 2005. (QSIC 2005). Fifth International Conference on | September 2005
  
  Quality Software, 2005. (QSIC 2005). Fifth International Conference on
  
  ISBN: 0-7695-2399-4
  
  Publication Project
- Play to Test
  
  Andreas Blass, Yuri Gurevich, Lev Nachmanson, Margus Veanes
  
  FATES 2005 | July 2005
  
  Publication Project Project
- Multiplexing of Partially Ordered Events
  
  Colin Campbell, Margus Veanes, Jiale Huo, Alexandre Petrenko
  
  TestCom 2005 | June 2005
  
  Received Best paper award.
  
  Publication Project
- Online testing with model programs
  
  Margus Veanes, Colin Campbell, Wolfram Schulte, Nikolai Tillmann
  
  ESEC/SIGSOFT FSE | January 2005
  
  ESEC/SIGSOFT FSE
  
  ISBN: 1-59593-014-0
  
  Publication Project Project
- Testing Concurrent Object-Oriented Systems with Spec Explorer
  
  Colin Campbell, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  January 2005
  
  ISBN: 3-540-27882-6
  
  Publication Project Project Project
- Exploration with Multiple State Groupings
  
  Colin Campbell, Margus Veanes
  
  Abstract State Machines 2005 | January 2005
  
  Publication Project Project
- Optimal Strategies for Testing Nondeterministic Systems
  
  Lev Nachmanson, Margus Veanes, Wolfram Schulte, Nikolai Tillmann, Wolfgang Grieskamp
  
  ISSTA 2004 | January 2004
  
  ISBN: 1-58113-820-2
  
  Publication Project Project
- Towards a Tool Environment for Model-Based Testing with AsmL
  
  Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  FATES 2003 | January 2004
  
  Publication Project Project Project
- Scenario-oriented Modeling in AsmL and its Instrumentation for Testing
  
  Mike Barnett, Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  Proc. of 2nd International Workshop on Scenarios and State Machines: Models, Algorithms, and Tools held at ICSE 2003, International Conference on Software Engineering 2003 | January 2003
  
  Publication
- Validating Use-Cases with the AsmL Test Tool
  
  Wolfram Schulte, Nikolai Tillmann, Margus Veanes, Mike Barnett
  
  QSIC | January 2003
  
  QSIC
  
  ISBN: 0-7695-2015-4
  
  Publication Project Project
- Model-Based Testing with AsmL .NET
  
  Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  1st European Conference on Model-Driven Software Engineering | January 2003
  
  Publication Project Project Project
- Combined Algorithm for Approximating a Finite State Abstraction of a Large System
  
  Rostislav Yavorsky, Margus Veanes
  
  ICSE 2003/Scenarios Workshop | January 2003
  
  ICSE 2003/Scenarios Workshop
  
  Publication Project Project
- Generating finite state machines from abstract state machines
  
  Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
  
  ISSTA 2002 | July 2002
  
  Publication Project Project
- Universal Plug and Play Machine Models: Modeling with Distributed Abstract State Machines
  
  Uwe Glässer, Margus Veanes
  
  Design and Analysis of Distributed Embedded Systems, IFIP 17th World Computer Congress (DIPES 2002) | January 2002
  
  Publication Project
- High-level Executable Specification of the Universal Plug and Play Architecture
  
  Uwe Glässer, Yuri Gurevich, Margus Veanes
  
  HICSS 2002 | January 2002
  
  Publication Project
- Incremental Dead State Detection in Logarithmic Time
  
  Caleb Stanford , Margus Veanes
  
  January 2023
  
  Preliminary and extended version of paper that appears in CAV 2023
  
  DOI
- Universal Plug and Play Machine Models
  
  U. Glässer, Y. Gurevich, M. Veanes, Yuri Gurevich, Margus Veanes
  
  MSR-TR-2001-59 | June 2001
  
  Publication Project
- The Relation Between Second-Order Unification and Simultaneous Rigid E-Unification
  
  Margus Veanes
  
  MPI-I-98-2-005 | February 1998
  
  Publication
- The decidability of simultaneous rigid E-unification with one variable
  
  Paliath Narendran, Margus Veanes, Andrei Voronkov, Anatoli Degtyarev, Yuri Gurevich
  
  139 | April 1997
  
  Publication
- Some undecidable problems related to the Herbrand theorem
  
  Yuri Gurevich, Margus Veanes
  
  UPMAIL-TR-138 | March 1997
  
  Publication
- On Computational Complexity of Basic Decision Problems of Finite Tree Automata
  
  Margus Veanes
  
  133 | January 1997
  
  Publication
- Uniform representation of recursively enumerable sets with simultaneous rigid E-unification
  
  Margus Veanes
  
  126 | June 1996
  
  Publication
- Meta-programming with Theory Systems
  
  Jonas Barklund, Katrin Boberg, Pierangelo Dell'Acqua, Margus Veanes
  
  106 | May 1995
  
  This paper appears as a chapter in Metalogics and Logic Programming, edited by K. Apt and F. Turini, and published by MIT Press in 1995.
  
  Publication
- Cycletrees: Flexible Interconnection Graphs for Parallel Computing
  
  Margus Veanes, Jonas Barklund
  
  97 | February 1995
  
  Publication
- Derivative Based Nonbacktracking Real-World Regex Matching with Backtracking Semantics
  
  Dan Moseley, Mario Nishio, Jose Perez Rodriguez, Olli Saarikivi, Stephen Toub, Margus Veanes, Tiki Wan, Eric Xu
  
  MSR-TR-2023-15 | April 2023
  
  Published by Microsoft
  
  Extended version of paper that appears in PLDI 2023.
  
  Publication Author's Version Project
- Lost in Translation: from Linear Temporal Logic to Büchi Automata
  
  Margus Veanes, Olli Saarikivi, Thomas Ball
  
  MSR-TR-2022-26 | October 2022
  
  Published by Microsoft
  
  Publication Project
- Regex Matching with Counting-Set Automata
  
  Margus Veanes (margus), Lukas Holik, Ondrej Lengal, Olli Saarikivi (olsaarik), Lenka Turonova, Tomas Vojnar
  
  MSR-TR-2020-31 | September 2020
  
  Published by Microsoft
  
  The technical report includes detailed proofs of most of the theorems stated in the conference OOPSLA'2020 paper.
  
  DOI Project
- Symbolic Boolean Derivatives for Efficiently Solving Extended Regular Expression Constraints
  
  Caleb Stanford, Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2020-25 | August 2020
  
  Published by Microsoft
  
  Updated November 2020. Extended version of paper in PLDI'2021.
  
  Publication Author's Version Project
- Fusing Effectful Comprehensions
  
  Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi
  
  MSR-TR-2016-55 | October 2016
  
  Publication
- PrePose: Security and Privacy for Gesture-Based Programming
  
  Lucas Silva Figueiredo, Ben Livshits, David Molnar, Margus Veanes
  
  MSR-TR-2014-146 | November 2014
  
  Publication
- FAST: A Transducer-Based Language for Tree Manipulation
  
  Loris D'Antoni, Margus Veanes, Ben Livshits, David Molnar,
  
  MSR-TR-2013-121 | November 2013
  
  Publication
- Minimization of Symbolic Automata
  
  Margus Veanes
  
  MSR-TR-2013-48 | April 2013
  
  Publication
- Equivalence of Extended Symbolic Finite Transducers
  
  Loris D'Antoni, Margus Veanes,
  
  MSR-TR-2013-4 | January 2013
  
  Publication
- Data-Parallel String-Manipulating Programs
  
  Margus Veanes, David Molnar, Todd Mytkowicz, Ben Livshits
  
  MSR-TR-2012-72 | July 2012
  
  Publication Project Project
- Generating Fast String Manipulating Code Through Transducer Exploration and SIMD Integration
  
  Margus Veanes, David Molnar, Ben Livshits, Lubomir Litchev
  
  MSR-TR-2011-124 | November 2011
  
  Publication
- Symbolic Finite State Transducers: Algorithms and Applications
  
  Nikolaj Bjørner, Ben Livshits, David Molnar, Margus Veanes
  
  MSR-TR-2011-85 | July 2011
  
  Publication
- Decision Procedures for Composition and Equivalence of Symbolic Finite State Transducers
  
  Margus Veanes, David Molnar, Ben Livshits
  
  MSR-TR-2011-32 | March 2011
  
  Publication
- Symbolic Transducers
  
  Nikolaj Bjørner, Margus Veanes
  
  MSR-TR-2011-3 | January 2011
  
  Publication
- BEK: Modeling Imperative String Operations with Symbolic Transducers
  
  , Ben Livshits, David Molnar, Prateek Saxena, Margus Veanes
  
  MSR-TR-2010-154 | November 2010
  
  Publication
- An Evaluation of Automata Algorithms for String Analysis
  
  , Margus Veanes
  
  MSR-TR-2010-90 | July 2010
  
  Updated August, 2010
  
  Publication Project
- Modeling Imperative String Operations with Transducers
  
  Pieter Hooimeijer, David Molnar, Prateek Saxena, Margus Veanes
  
  MSR-TR-2010-96 | July 2010
  
  Publication
- Alternating Simulation and IOCO
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2010-38 | April 2010
  
  Extended version of paper with the same title in ICTSS 2010, LNCS vol 6435
  
  Publication
- Solving Extended Regular Constraints Symbolically
  
  Margus Veanes, Nikolaj Bjørner, Leonardo de Moura
  
  MSR-TR-2009-177 | December 2009
  
  Publication Project
- Rex: Symbolic Regular Expression Explorer
  
  Margus Veanes, Jonathan "Peli" de Halleux, Nikolai Tillmann
  
  MSR-TR-2009-137 | October 2009
  
  ICST'10
  
  Publication Publication Project
- Qex: Symbolic SQL Query Explorer
  
  Margus Veanes, Jonathan de Halleux, Nikolai Tillmann, Jonathan "Peli" de Halleux
  
  MSR-TR-2009-2015 | October 2009
  
  Updated January 2010
  
  Publication Project
- Input-Output Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-56 | May 2009
  
  Preliminary version of paper to appear in ICTAC'09, LNCS.
  
  Publication
- Symbolic Query Exploration
  
  Margus Veanes, Pavel Grigorenko, Jonathan "Peli" de Halleux, Nikolai Tillmann
  
  MSR-TR-2009-65 | May 2009
  
  Publication Project Project
- Symbolic Bounded Conformance Checking of Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-28 | March 2009
  
  This is an extended version of a paper to appear in PSI'09, LNCS.
  
  Publication Project
- Arranging Partitures for Models and Theorems
  
  Johannes Helander, Margus Veanes
  
  MSR-TR-2009-24 | March 2009
  
  Publication
- Bounded reachability of model programs
  
  Margus Veanes, Ando Saabas, Nikolaj Bjørner
  
  MSR-TR-2008-81 | May 2008
  
  Parts of this report are presented at FORTE'08 and LPAR'08.
  
  Publication Project
- Embedded Systems Research at DemoFest’07
  
  Oscar Almeida, Alessandro Forin, Philip Garcia, Johannes Helander, Nishith Khantal, Hong Lu, Karl Meier, Sibin Mohan, Henrik Frystyk Nielsen, Neil Pittman, Risto Serg, Bharat Sukhwani, Margus Veanes, Ben Zorn, Sarah Berry, Chris Boyce, David Chaszar, Brandon Culrich, Mikhail Kisin, Gabe Knezek, Warren Linam-Church, Steve Liu, Michael Stewart, Doug Toney
  
  MSR-TR-2007-94 | July 2007
  
  Publication Publication
- Play to Test
  
  Andreas Blass, Yuri Gurevich, Lev Nachmanson, Margus Veanes
  
  MSR-TR-2005-04 | January 2005
  
  A short version appears in: FATES 2005, LNCS vol. 3997, pp. 32-46
  
  Publication Project
- On-The-Fly Testing of Reactive Systems
  
  Margus Veanes, Colin Campbell, Wolfram Schulte, Pushmeet Kohli
  
  MSR-TR-2005-05 | January 2005
  
  Publication Project
- An Abstract Communication Model
  
  Uwe Glässer, Yuri Gurevich, Margus Veanes
  
  MSR-TR-2002-55 | May 2002
  
  Publication Publication Project
- Toward Industrial Strength Abstract State Machines
  
  Yuri Gurevich, Wolfram Schulte, Margus Veanes
  
  MSR-TR-2001-98 | October 2001
  
  Publication Project
- Decidability and Complexity of Simultaneous Rigid E-Unification with One Variable and Related Results
  
  Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, Andrei Voronkov
  
  Theoretical Computer Science | August 2000, Vol 243(1-2): pp. 167-184
  
  Publication
- Farmer’s Theorem revisited
  
  Margus Veanes
  
  Information Processing Letters | April 2000, Vol 74: pp. 47-53
  
  Publication
- On the Undecidability of Second-Order Unification
  
  Jordi Levy, Margus Veanes
  
  Information and Computation | January 2000, Vol 159: pp. 125-150
  
  Publication Publication
- Rigid Reachability, The Non-Symmetric Form of Rigid E-Unification
  
  Harald Ganzinger, Florent Jacquemard, Margus Veanes
  
  International Journal of Foundations of Computer Science | January 2000, pp. 3-27
  
  Publication
- Construction of natural cycletrees
  
  Margus Veanes, Jonas Barklund
  
  Information Processing Letters | January 1996, Vol 60: pp. 313-318
  
  Publication
- On the number of edges in cycletrees
  
  Margus Veanes, Jonas Barklund
  
  Information Processing Letters | January 1996, Vol 57: pp. 225-229
  
  Publication Publication
- Natural cycletrees: Flexible interconnection graphs
  
  Margus Veanes, Jonas Barklund
  
  Journal of Parallel and Distributed Computing | January 1996, Vol 33: pp. 44-54
  
  Publication Publication
- Monadic Decomposition
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  Journal of the ACM | May 2017, Vol 64
  
  Publication Publication Publication Project
- Prepose: Privacy, Security, and Reliability for Gesture-Based Programming
  
  Lucas Silva Figueiredo , David Molnar, Margus Veanes, Benjamin Livshits
  
  IEEE Security & Privacy | April 2017, Vol 15: pp. 14-23
  
  Publication Publication
- Prepose: Privacy, Security, and Reliability for Gesture-Based Programming
  
  Lucas Silva Figueiredo, David Molnar, Margus Veanes, Ben Livshits
  
  IEEE Journal of Security and Privacy | December 2016
  
  Publication
- FAST: A Transducer-Based Language for Tree Manipulation
  
  Lori D'Antoni, Margus Veanes, Ben Livshits, David Molnar
  
  ACM Transactions on Programming Languages and Systems (TOPLAS) | October 2015, Vol 38
  
  Publication Publication
- Extended symbolic finite automata and transducers
  
  Loris D’Antoni, Margus Veanes
  
  Formal Methods in System Design | July 2015
  
  Publication
- Symbolic Tree Automata
  
  Margus Veanes, Nikolaj Bjørner
  
  Information Processing Letters | March 2015, Vol 115(3): pp. 418-424
  
  Publication Publication
- Alternating simulation and IOCO
  
  Margus Veanes, Nikolaj Bjørner
  
  International Journal on Software Tools for Technology Transfer (STTT) | September 2011
  
  Publication Publication
- Composing Model Programs for Analysis
  
  Margus Veanes, Jonathan Jacky
  
  The Journal of Logic and Algebraic Programming | October 2010, Vol 79: pp. 467-482
  
  Publication Publication
- Symbolic Bounded Model Checking of Abstract State Machines
  
  Margus Veanes, Nikolaj Bjørner, Yuri Gurevich, Wolfram Schulte
  
  Int J Software Informatics | June 2009, pp. 149-170
  
  Publication Project
- Can Abstract State Machines Be Useful in Language Theory?
  
  Yuri Gurevich, Margus Veanes, Charles Wallace
  
  Theoretical Computer Science | January 2007, Vol 376: pp. 17-29
  
  Publication Project
- Abstract Communication Model for Distributed Systems
  
  Uwe Glässer, Yuri Gurevich, Margus Veanes
  
  IEEE Transactions on Software Engineering | July 2004, Vol 30(7): pp. 458-472
  
  Publication Project Project
- Instrumenting Scenarios in a Model-Driven Development Environment
  
  Wolfgang Grieskamp, Nikolai Tillmann, Margus Veanes
  
  Journal of Information and Software Technology | January 2004, Vol 46: pp. 1027-1036
  
  Publication Project Project Project
- Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer
  
  Margus Veanes, Colin Campbell, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, Lev Nachmanson
  
  Formal Methods and Testing | Published by Springer Verlag | 2008, Vol 4949
  
  ISBN: 978-3-540-78916-1
  
  The attached file is a preliminary version.
  
  Publication Project Project Project
- Model-Based Software Testing and Analysis with C#
  
  Jonathan Jacky, Margus Veanes, Colin Campbell, Wolfram Schulte
  
  Published by Cambridge University Press | January 2008
  
  ISBN: 9.78052E+12
  
  Publication
- On Simultaneous Rigid E-Unification
  
  Margus Veanes
  
  June 1997, pp. 120
  
  June 1997
  
  Publication Publication
- Cycletrees: a Novel Class of Interconnection Graphs
  
  Margus Veanes
  
  January 1993
  
  January 1993
  
  Publication