RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement, and Restricted Lookarounds
Ian Erik Varatalu, Margus Veanes, Juhan Ernits
POPL | January 2025
Margus Veanes
Principal Researcher
Publications
Publications by Year
-
Symbolic Automata: Omega-Regularity Modulo Theories
Margus Veanes, Thomas Ball, Gabriel Ebner, Ekaterina Zhuchko
POPL | January 2025
-
Lean Formalization of Extended Regular Expression Matching with Lookarounds
Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner
CPP | January 2024
-
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.
Incremental Dead State Detection in Logarithmic Time
Caleb Stanford , Margus Veanes
January 2023
Preliminary and extended version of paper that appears in CAV 2023
-
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
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
-
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.
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.
-
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
Symbolic Regex Matcher
Margus Veanes (margus), Olli Saarikivi (olsaarik), Tiki Wan, Eric Xu
TACAS | April 2019
-
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.
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
-
Minimization of Symbolic Transducers
Olli Saarikivi, Margus Veanes
Computer Aided Verification, 29th International Conference (CAV 2017) | July 2017
The power of symbolic automata and transducers
Loris D'Antoni, Margus Veanes
Computer Aided Verification, 29th International Conference (CAV'17) | July 2017
Fusing Effectful Comprehensions
Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017) | June 2017
Monadic Decomposition
Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
Journal of the ACM | May 2017, Vol 64
Forward Bisimulations for Nondeterministic Symbolic Finite Automata
Loris D'Antoni, Margus Veanes
TACAS | April 2017
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
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
Monadic Second-Order Logic on Finite Sequences
Loris D'Antoni, Margus Veanes
POPL'2017 | January 2017
-
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
Fusing Effectful Comprehensions
Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi
MSR-TR-2016-55 | October 2016
Minimization of Symbolic Tree Automata
LICS | July 2016
LICS
-
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
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
Extended symbolic finite automata and transducers
Loris D’Antoni, Margus Veanes
Formal Methods in System Design | July 2015
Symbolic Tree Automata
Margus Veanes, Nikolaj Bjørner
Information Processing Letters | March 2015, Vol 115(3): pp. 418-424
Symbolic String Transformations with Regular Lookahead and Rollback
PSI 2014 | February 2015
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
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
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
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
-
PrePose: Security and Privacy for Gesture-Based Programming
Lucas Silva Figueiredo, Ben Livshits, David Molnar, Margus Veanes
MSR-TR-2014-146 | November 2014
Skolemization Modulo Theories
Konstantin Korovin, Margus Veanes
ICMS'14 | August 2014
Monadic Decomposition
Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
CAV'14 | July 2014
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
Minimization of Symbolic Automata
Loris D'Antoni, Margus Veanes
POPL'14 | January 2014
POPL'14
-
Effectively Monadic Predicates
Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
LPAR-19 | December 2013
FAST: A Transducer-Based Language for Tree Manipulation
Loris D'Antoni, Margus Veanes, Ben Livshits, David Molnar,
MSR-TR-2013-121 | November 2013
Applications of Symbolic Finite Automata
CIAA'13 | July 2013
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.
Minimization of Symbolic Automata
MSR-TR-2013-48 | April 2013
Equivalence of Extended Symbolic Finite Transducers
Loris D'Antoni, Margus Veanes,
MSR-TR-2013-4 | January 2013
Static Analysis of String Encoders and Decoders
Margus Veanes, Loris D'Antoni
VMCAI 2013 | January 2013
-
Data-Parallel String-Manipulating Programs
Margus Veanes, David Molnar, Todd Mytkowicz, Ben Livshits
MSR-TR-2012-72 | July 2012
Symbolic Automata: The Toolkit
Margus Veanes, Nikolaj Bjørner
TACAS'12 | March 2012
Symbolic Finite State Transducers: Algorithms and Applications
Margus Veanes, Pieter Hooimeijer, David Molnar, Nikolaj Bjorner, Ben Livshits
POPL'12 | January 2012
-
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
Alternating simulation and IOCO
Margus Veanes, Nikolaj Bjørner
International Journal on Software Tools for Technology Transfer (STTT) | September 2011
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
Symbolic Finite State Transducers: Algorithms and Applications
Nikolaj Bjørner, Ben Livshits, David Molnar, Margus Veanes
MSR-TR-2011-85 | July 2011
Decision Procedures for Composition and Equivalence of Symbolic Finite State Transducers
Margus Veanes, David Molnar, Ben Livshits
MSR-TR-2011-32 | March 2011
Symbolic Transducers
Nikolaj Bjørner, Margus Veanes
MSR-TR-2011-3 | January 2011
Symbolic Tree Transducers
Margus Veanes, Nikolaj Bjørner
Ershov Informatics Conference (PSI'11) | January 2011
-
BEK: Modeling Imperative String Operations with Symbolic Transducers
, Ben Livshits, David Molnar, Prateek Saxena, Margus Veanes
MSR-TR-2010-154 | November 2010
Composing Model Programs for Analysis
Margus Veanes, Jonathan Jacky
The Journal of Logic and Algebraic Programming | October 2010, Vol 79: pp. 467-482
An Evaluation of Automata Algorithms for String Analysis
MSR-TR-2010-90 | July 2010
Updated August, 2010
Modeling Imperative String Operations with Transducers
Pieter Hooimeijer, David Molnar, Prateek Saxena, Margus Veanes
MSR-TR-2010-96 | July 2010
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
Qex: Symbolic SQL Query Explorer
Margus Veanes, Nikolai Tillmann, Jonathan "Peli" de Halleux
LPAR-16 | April 2010
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
-
Solving Extended Regular Constraints Symbolically
Margus Veanes, Nikolaj Bjørner, Leonardo de Moura
MSR-TR-2009-177 | December 2009
Symbolic Query Exploration
Margus Veanes, Pavel Grigorenko, Jonathan "Peli" de Halleux, Nikolai Tillmann
ICFEM'09 | December 2009
Model-Based Testing of Web Applications using NModel
Juhan Ernits, Rivo Roo, Jonathan Jacky, Margus Veanes
LNCS, TESTCOM/FATES 2009 | November 2009
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
Rex: Symbolic Regular Expression Explorer
Margus Veanes, Jonathan "Peli" de Halleux, Nikolai Tillmann
MSR-TR-2009-137 | October 2009
ICST'10
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
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.
Symbolic Query Exploration
Margus Veanes, Pavel Grigorenko, Jonathan "Peli" de Halleux, Nikolai Tillmann
MSR-TR-2009-65 | May 2009
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.
Arranging Partitures for Models and Theorems
Johannes Helander, Margus Veanes
MSR-TR-2009-24 | March 2009
-
On Bounded Reachability of Programs with Set Comprehensions
Margus Veanes, Ando Saabas
LPAR'08 | November 2008
LPAR'08
Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract)
Margus Veanes, Ando Saabas
ABZ'08 | September 2008
This is an extended abstract.
An SMT Approach to Bounded Reachability Analysis of Model Programs
Margus Veanes, Nikolaj Bjørner, Alexander Raschke
FORTE'08 | June 2008
FORTE'08
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
Protocol Modeling with Model Program Composition
Margus Veanes, Wolfram Schulte
FORTE'08 | June 2008
ISBN: 978-3-540-68854-9
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.
Enabling the Future Auto with Model-Driven Services
Johannes Helander, Margus Veanes
National Workshop on High-Confidence Automotive Cyber-Physical Systems. | April 2008
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
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.
-
Adapting Futures: Scalability for Real-World Computing
Johannes Helander, Risto Serg, Margus Veanes, Pritam Roy
RTSS'07 | December 2007
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
Composition of Model Programs
Margus Veanes, Colin Campbell, Wolfram Schulte
FORTE | June 2007
ISBN: 978-3-540-73195-5
State Isomorphism in Model Programs with Abstract Data Structures
Margus Veanes, Juhan Ernits, Colin Campbell
FORTE'07 | June 2007
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
-
Online Testing with Reinforcement Learning
Margus Veanes, Pritam Roy, Colin Campbell
Formal Approaches to Software Testing and Runtime Verification, FATES/RV 2006 | January 2006
-
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
Play to Test
Andreas Blass, Yuri Gurevich, Lev Nachmanson, Margus Veanes
FATES 2005 | July 2005
Multiplexing of Partially Ordered Events
Colin Campbell, Margus Veanes, Jiale Huo, Alexandre Petrenko
TestCom 2005 | June 2005
Received Best paper award.
Exploration with Multiple State Groupings
Colin Campbell, Margus Veanes
Abstract State Machines 2005 | January 2005
On-The-Fly Testing of Reactive Systems
Margus Veanes, Colin Campbell, Wolfram Schulte, Pushmeet Kohli
MSR-TR-2005-05 | January 2005
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
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
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
-
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
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
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
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
-
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
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
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
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
-
Generating finite state machines from abstract state machines
Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
ISSTA 2002 | July 2002
An Abstract Communication Model
Uwe Glässer, Yuri Gurevich, Margus Veanes
MSR-TR-2002-55 | May 2002
High-level Executable Specification of the Universal Plug and Play Architecture
Uwe Glässer, Yuri Gurevich, Margus Veanes
HICSS 2002 | January 2002
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
-
Universal Plug and Play Machine Models
U. Glässer, Y. Gurevich, M. Veanes, Yuri Gurevich, Margus Veanes
MSR-TR-2001-59 | June 2001
Conformance Testing with Abstract State Machines
Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
EUROCAST 2001 | February 2001
Toward Industrial Strength Abstract State Machines
Yuri Gurevich, Wolfram Schulte, Margus Veanes
MSR-TR-2001-98 | October 2001
-
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
Farmer’s Theorem revisited
Information Processing Letters | April 2000, Vol 74: pp. 47-53
On the Undecidability of Second-Order Unification
Jordi Levy, Margus Veanes
Information and Computation | January 2000, Vol 159: pp. 125-150
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
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
-
Logic with Equality: Partisan Corroboration and Shifted Pairing
Yuri Gurevich, Margus Veanes
August 1999
Decidable Fragments of Simultaneous Rigid Reachability
Véronique Cortier, Harald Ganzinger, Florent Jacquemard, Margus Veanes
ICALP 1999 | January 1999
The Two-Variable Guarded Fragment with Transitive Relations
Harald Ganzinger, Christoph Meyer, Margus Veanes
LICS 1999 | January 1999
-
The relation between second-order unification and simultaneous rigid E-unification
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)
The Relation Between Second-Order Unification and Simultaneous Rigid E-Unification
MPI-I-98-2-005 | February 1998
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
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
The Decidability of Simultaneous Rigid E-Unification with One Variable
Paliath Narendran, Margus Veanes, Andrei Voronkov, Anatoli Degtyarev, Yuri Gurevich
RTA'98 | January 1998
-
On Simultaneous Rigid E-Unification
June 1997, pp. 120
June 1997
The decidability of simultaneous rigid E-unification with one variable
Paliath Narendran, Margus Veanes, Andrei Voronkov, Anatoli Degtyarev, Yuri Gurevich
139 | April 1997
Some undecidable problems related to the Herbrand theorem
Yuri Gurevich, Margus Veanes
UPMAIL-TR-138 | March 1997
On Computational Complexity of Basic Decision Problems of Finite Tree Automata
133 | January 1997
The undecidability of simultaneous rigid E-unification with two variables
5th Kurt Gödel Colloquium (KGC'97) | January 1997
-
Uniform representation of recursively enumerable sets with simultaneous rigid E-unification
126 | June 1996
Construction of natural cycletrees
Margus Veanes, Jonas Barklund
Information Processing Letters | January 1996, Vol 60: pp. 313-318
Natural cycletrees: Flexible interconnection graphs
Margus Veanes, Jonas Barklund
Journal of Parallel and Distributed Computing | January 1996, Vol 33: pp. 44-54
On the number of edges in cycletrees
Margus Veanes, Jonas Barklund
Information Processing Letters | January 1996, Vol 57: pp. 225-229
-
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.
Cycletrees: Flexible Interconnection Graphs for Parallel Computing
Margus Veanes, Jonas Barklund
97 | February 1995
-
Cycletrees: a Novel Class of Interconnection Graphs
January 1993
January 1993
Publications by Research Area
-
Universal Plug and Play Machine Models
U. Glässer, Y. Gurevich, M. Veanes, Yuri Gurevich, Margus Veanes
MSR-TR-2001-59 | June 2001
Conformance Testing with Abstract State Machines
Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
EUROCAST 2001 | February 2001
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
Farmer’s Theorem revisited
Information Processing Letters | April 2000, Vol 74: pp. 47-53
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
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
Decidable Fragments of Simultaneous Rigid Reachability
Véronique Cortier, Harald Ganzinger, Florent Jacquemard, Margus Veanes
ICALP 1999 | January 1999
On Simultaneous Rigid E-Unification
June 1997, pp. 120
June 1997
On Computational Complexity of Basic Decision Problems of Finite Tree Automata
133 | January 1997
Construction of natural cycletrees
Margus Veanes, Jonas Barklund
Information Processing Letters | January 1996, Vol 60: pp. 313-318
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.
Cycletrees: Flexible Interconnection Graphs for Parallel Computing
Margus Veanes, Jonas Barklund
97 | February 1995
Cycletrees: a Novel Class of Interconnection Graphs
January 1993
January 1993
Symbolic Automata: Omega-Regularity Modulo Theories
Margus Veanes, Thomas Ball, Gabriel Ebner, Ekaterina Zhuchko
POPL | January 2025
RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement, and Restricted Lookarounds
Ian Erik Varatalu, Margus Veanes, Juhan Ernits
POPL | January 2025
Lean Formalization of Extended Regular Expression Matching with Lookarounds
Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner
CPP | January 2024
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.
Incremental Dead State Detection in Logarithmic Time
Caleb Stanford , Margus Veanes
January 2023
Preliminary and extended version of paper that appears in CAV 2023
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
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.
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.
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
Symbolic Regex Matcher
Margus Veanes (margus), Olli Saarikivi (olsaarik), Tiki Wan, Eric Xu
TACAS | April 2019
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.
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
The power of symbolic automata and transducers
Loris D'Antoni, Margus Veanes
Computer Aided Verification, 29th International Conference (CAV'17) | July 2017
Minimization of Symbolic Transducers
Olli Saarikivi, Margus Veanes
Computer Aided Verification, 29th International Conference (CAV 2017) | July 2017
Fusing Effectful Comprehensions
Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017) | June 2017
Monadic Decomposition
Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
Journal of the ACM | May 2017, Vol 64
Forward Bisimulations for Nondeterministic Symbolic Finite Automata
Loris D'Antoni, Margus Veanes
TACAS | April 2017
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
Monadic Second-Order Logic on Finite Sequences
Loris D'Antoni, Margus Veanes
POPL'2017 | January 2017
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
Fusing Effectful Comprehensions
Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi
MSR-TR-2016-55 | October 2016
Minimization of Symbolic Tree Automata
LICS | July 2016
LICS
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
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
Symbolic String Transformations with Regular Lookahead and Rollback
PSI 2014 | February 2015
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
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
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
Skolemization Modulo Theories
Konstantin Korovin, Margus Veanes
ICMS'14 | August 2014
Monadic Decomposition
Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
CAV'14 | July 2014
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
Minimization of Symbolic Automata
Loris D'Antoni, Margus Veanes
POPL'14 | January 2014
POPL'14
FAST: A Transducer-Based Language for Tree Manipulation
Loris D'Antoni, Margus Veanes, Ben Livshits, David Molnar,
MSR-TR-2013-121 | November 2013
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.
Applications of Symbolic Finite Automata
CIAA'13 | July 2013
Minimization of Symbolic Automata
MSR-TR-2013-48 | April 2013
Static Analysis of String Encoders and Decoders
Margus Veanes, Loris D'Antoni
VMCAI 2013 | January 2013
Equivalence of Extended Symbolic Finite Transducers
Loris D'Antoni, Margus Veanes,
MSR-TR-2013-4 | January 2013
Symbolic Automata: The Toolkit
Margus Veanes, Nikolaj Bjørner
TACAS'12 | March 2012
Symbolic Finite State Transducers: Algorithms and Applications
Margus Veanes, Pieter Hooimeijer, David Molnar, Nikolaj Bjorner, Ben Livshits
POPL'12 | January 2012
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
Alternating simulation and IOCO
Margus Veanes, Nikolaj Bjørner
International Journal on Software Tools for Technology Transfer (STTT) | September 2011
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
Decision Procedures for Composition and Equivalence of Symbolic Finite State Transducers
Margus Veanes, David Molnar, Ben Livshits
MSR-TR-2011-32 | March 2011
Symbolic Transducers
Nikolaj Bjørner, Margus Veanes
MSR-TR-2011-3 | January 2011
Symbolic Tree Transducers
Margus Veanes, Nikolaj Bjørner
Ershov Informatics Conference (PSI'11) | January 2011
BEK: Modeling Imperative String Operations with Symbolic Transducers
, Ben Livshits, David Molnar, Prateek Saxena, Margus Veanes
MSR-TR-2010-154 | November 2010
Composing Model Programs for Analysis
Margus Veanes, Jonathan Jacky
The Journal of Logic and Algebraic Programming | October 2010, Vol 79: pp. 467-482
An Evaluation of Automata Algorithms for String Analysis
MSR-TR-2010-90 | July 2010
Updated August, 2010
Modeling Imperative String Operations with Transducers
Pieter Hooimeijer, David Molnar, Prateek Saxena, Margus Veanes
MSR-TR-2010-96 | July 2010
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
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
Qex: Symbolic SQL Query Explorer
Margus Veanes, Nikolai Tillmann, Jonathan "Peli" de Halleux
LPAR-16 | April 2010
Symbolic Query Exploration
Margus Veanes, Pavel Grigorenko, Jonathan "Peli" de Halleux, Nikolai Tillmann
ICFEM'09 | December 2009
Solving Extended Regular Constraints Symbolically
Margus Veanes, Nikolaj Bjørner, Leonardo de Moura
MSR-TR-2009-177 | December 2009
Model-Based Testing of Web Applications using NModel
Juhan Ernits, Rivo Roo, Jonathan Jacky, Margus Veanes
LNCS, TESTCOM/FATES 2009 | November 2009
Rex: Symbolic Regular Expression Explorer
Margus Veanes, Jonathan "Peli" de Halleux, Nikolai Tillmann
MSR-TR-2009-137 | October 2009
ICST'10
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
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
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.
Symbolic Query Exploration
Margus Veanes, Pavel Grigorenko, Jonathan "Peli" de Halleux, Nikolai Tillmann
MSR-TR-2009-65 | May 2009
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.
Arranging Partitures for Models and Theorems
Johannes Helander, Margus Veanes
MSR-TR-2009-24 | March 2009
On Bounded Reachability of Programs with Set Comprehensions
Margus Veanes, Ando Saabas
LPAR'08 | November 2008
LPAR'08
Protocol Modeling with Model Program Composition
Margus Veanes, Wolfram Schulte
FORTE'08 | June 2008
ISBN: 978-3-540-68854-9
An SMT Approach to Bounded Reachability Analysis of Model Programs
Margus Veanes, Nikolaj Bjørner, Alexander Raschke
FORTE'08 | June 2008
FORTE'08
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
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.
Enabling the Future Auto with Model-Driven Services
Johannes Helander, Margus Veanes
National Workshop on High-Confidence Automotive Cyber-Physical Systems. | April 2008
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.
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
Adapting Futures: Scalability for Real-World Computing
Johannes Helander, Risto Serg, Margus Veanes, Pritam Roy
RTSS'07 | December 2007
Composition of Model Programs
Margus Veanes, Colin Campbell, Wolfram Schulte
FORTE | June 2007
ISBN: 978-3-540-73195-5
State Isomorphism in Model Programs with Abstract Data Structures
Margus Veanes, Juhan Ernits, Colin Campbell
FORTE'07 | June 2007
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
Online Testing with Reinforcement Learning
Margus Veanes, Pritam Roy, Colin Campbell
Formal Approaches to Software Testing and Runtime Verification, FATES/RV 2006 | January 2006
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
Play to Test
Andreas Blass, Yuri Gurevich, Lev Nachmanson, Margus Veanes
FATES 2005 | July 2005
Multiplexing of Partially Ordered Events
Colin Campbell, Margus Veanes, Jiale Huo, Alexandre Petrenko
TestCom 2005 | June 2005
Received Best paper award.
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
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
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
Exploration with Multiple State Groupings
Colin Campbell, Margus Veanes
Abstract State Machines 2005 | January 2005
On-The-Fly Testing of Reactive Systems
Margus Veanes, Colin Campbell, Wolfram Schulte, Pushmeet Kohli
MSR-TR-2005-05 | January 2005
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
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
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
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
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
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
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
Generating finite state machines from abstract state machines
Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
ISSTA 2002 | July 2002
An Abstract Communication Model
Uwe Glässer, Yuri Gurevich, Margus Veanes
MSR-TR-2002-55 | May 2002
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
High-level Executable Specification of the Universal Plug and Play Architecture
Uwe Glässer, Yuri Gurevich, Margus Veanes
HICSS 2002 | January 2002
-
On the Undecidability of Second-Order Unification
Jordi Levy, Margus Veanes
Information and Computation | January 2000, Vol 159: pp. 125-150
Logic with Equality: Partisan Corroboration and Shifted Pairing
Yuri Gurevich, Margus Veanes
August 1999
The relation between second-order unification and simultaneous rigid E-unification
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)
The Relation Between Second-Order Unification and Simultaneous Rigid E-Unification
MPI-I-98-2-005 | February 1998
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
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
The Decidability of Simultaneous Rigid E-Unification with One Variable
Paliath Narendran, Margus Veanes, Andrei Voronkov, Anatoli Degtyarev, Yuri Gurevich
RTA'98 | January 1998
Some undecidable problems related to the Herbrand theorem
Yuri Gurevich, Margus Veanes
UPMAIL-TR-138 | March 1997
The undecidability of simultaneous rigid E-unification with two variables
5th Kurt Gödel Colloquium (KGC'97) | January 1997
Natural cycletrees: Flexible interconnection graphs
Margus Veanes, Jonas Barklund
Journal of Parallel and Distributed Computing | January 1996, Vol 33: pp. 44-54
Cycletrees: a Novel Class of Interconnection Graphs
January 1993
January 1993
Symbolic Automata: Omega-Regularity Modulo Theories
Margus Veanes, Thomas Ball, Gabriel Ebner, Ekaterina Zhuchko
POPL | January 2025
RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement, and Restricted Lookarounds
Ian Erik Varatalu, Margus Veanes, Juhan Ernits
POPL | January 2025
Incremental Dead State Detection in Logarithmic Time
Caleb Stanford , Margus Veanes
January 2023
Preliminary and extended version of paper that appears in CAV 2023
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.
Monadic Second-Order Logic on Finite Sequences
Loris D'Antoni, Margus Veanes
POPL'2017 | January 2017
Minimization of Symbolic Tree Automata
LICS | July 2016
LICS
Extended symbolic finite automata and transducers
Loris D’Antoni, Margus Veanes
Formal Methods in System Design | July 2015
Symbolic Tree Automata
Margus Veanes, Nikolaj Bjørner
Information Processing Letters | March 2015, Vol 115(3): pp. 418-424
Symbolic String Transformations with Regular Lookahead and Rollback
PSI 2014 | February 2015
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
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
Skolemization Modulo Theories
Konstantin Korovin, Margus Veanes
ICMS'14 | August 2014
Monadic Decomposition
Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
CAV'14 | July 2014
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
Minimization of Symbolic Automata
Loris D'Antoni, Margus Veanes
POPL'14 | January 2014
POPL'14
Effectively Monadic Predicates
Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
LPAR-19 | December 2013
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.
Applications of Symbolic Finite Automata
CIAA'13 | July 2013
Minimization of Symbolic Automata
MSR-TR-2013-48 | April 2013
Static Analysis of String Encoders and Decoders
Margus Veanes, Loris D'Antoni
VMCAI 2013 | January 2013
Equivalence of Extended Symbolic Finite Transducers
Loris D'Antoni, Margus Veanes,
MSR-TR-2013-4 | January 2013
Symbolic Finite State Transducers: Algorithms and Applications
Margus Veanes, Pieter Hooimeijer, David Molnar, Nikolaj Bjorner, Ben Livshits
POPL'12 | January 2012
Alternating simulation and IOCO
Margus Veanes, Nikolaj Bjørner
International Journal on Software Tools for Technology Transfer (STTT) | September 2011
Symbolic Finite State Transducers: Algorithms and Applications
Nikolaj Bjørner, Ben Livshits, David Molnar, Margus Veanes
MSR-TR-2011-85 | July 2011
Decision Procedures for Composition and Equivalence of Symbolic Finite State Transducers
Margus Veanes, David Molnar, Ben Livshits
MSR-TR-2011-32 | March 2011
Symbolic Tree Transducers
Margus Veanes, Nikolaj Bjørner
Ershov Informatics Conference (PSI'11) | January 2011
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
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.
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.
-
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
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
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
PrePose: Security and Privacy for Gesture-Based Programming
Lucas Silva Figueiredo, Ben Livshits, David Molnar, Margus Veanes
MSR-TR-2014-146 | November 2014
Symbolic Finite State Transducers: Algorithms and Applications
Margus Veanes, Pieter Hooimeijer, David Molnar, Nikolaj Bjorner, Ben Livshits
POPL'12 | January 2012
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
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
Decision Procedures for Composition and Equivalence of Symbolic Finite State Transducers
Margus Veanes, David Molnar, Ben Livshits
MSR-TR-2011-32 | March 2011
Symbolic Transducers
Nikolaj Bjørner, Margus Veanes
MSR-TR-2011-3 | January 2011
BEK: Modeling Imperative String Operations with Symbolic Transducers
, Ben Livshits, David Molnar, Prateek Saxena, Margus Veanes
MSR-TR-2010-154 | November 2010
-
The decidability of simultaneous rigid E-unification with one variable
Paliath Narendran, Margus Veanes, Andrei Voronkov, Anatoli Degtyarev, Yuri Gurevich
139 | April 1997
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
-
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
PrePose: Security and Privacy for Gesture-Based Programming
Lucas Silva Figueiredo, Ben Livshits, David Molnar, Margus Veanes
MSR-TR-2014-146 | November 2014
-
Data-Parallel String-Manipulating Programs
Margus Veanes, David Molnar, Todd Mytkowicz, Ben Livshits
MSR-TR-2012-72 | July 2012
-
The Two-Variable Guarded Fragment with Transitive Relations
Harald Ganzinger, Christoph Meyer, Margus Veanes
LICS 1999 | January 1999
Uniform representation of recursively enumerable sets with simultaneous rigid E-unification
126 | June 1996
Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract)
Margus Veanes, Ando Saabas
ABZ'08 | September 2008
This is an extended abstract.
Toward Industrial Strength Abstract State Machines
Yuri Gurevich, Wolfram Schulte, Margus Veanes
MSR-TR-2001-98 | October 2001
-
On the number of edges in cycletrees
Margus Veanes, Jonas Barklund
Information Processing Letters | January 1996, Vol 57: pp. 225-229
Enabling the Future Auto with Model-Driven Services
Johannes Helander, Margus Veanes
National Workshop on High-Confidence Automotive Cyber-Physical Systems. | April 2008
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
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
-
On-The-Fly Testing of Reactive Systems
Margus Veanes, Colin Campbell, Wolfram Schulte, Pushmeet Kohli
MSR-TR-2005-05 | January 2005
Publications by Type
-
Conformance Testing with Abstract State Machines
Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
EUROCAST 2001 | February 2001
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
Logic with Equality: Partisan Corroboration and Shifted Pairing
Yuri Gurevich, Margus Veanes
August 1999
Decidable Fragments of Simultaneous Rigid Reachability
Véronique Cortier, Harald Ganzinger, Florent Jacquemard, Margus Veanes
ICALP 1999 | January 1999
The Two-Variable Guarded Fragment with Transitive Relations
Harald Ganzinger, Christoph Meyer, Margus Veanes
LICS 1999 | January 1999
The relation between second-order unification and simultaneous rigid E-unification
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)
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
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
The Decidability of Simultaneous Rigid E-Unification with One Variable
Paliath Narendran, Margus Veanes, Andrei Voronkov, Anatoli Degtyarev, Yuri Gurevich
RTA'98 | January 1998
The undecidability of simultaneous rigid E-unification with two variables
5th Kurt Gödel Colloquium (KGC'97) | January 1997
Symbolic Automata: Omega-Regularity Modulo Theories
Margus Veanes, Thomas Ball, Gabriel Ebner, Ekaterina Zhuchko
POPL | January 2025
RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement, and Restricted Lookarounds
Ian Erik Varatalu, Margus Veanes, Juhan Ernits
POPL | January 2025
Lean Formalization of Extended Regular Expression Matching with Lookarounds
Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner
CPP | January 2024
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
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
Symbolic Regex Matcher
Margus Veanes (margus), Olli Saarikivi (olsaarik), Tiki Wan, Eric Xu
TACAS | April 2019
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.
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
The power of symbolic automata and transducers
Loris D'Antoni, Margus Veanes
Computer Aided Verification, 29th International Conference (CAV'17) | July 2017
Minimization of Symbolic Transducers
Olli Saarikivi, Margus Veanes
Computer Aided Verification, 29th International Conference (CAV 2017) | July 2017
Fusing Effectful Comprehensions
Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017) | June 2017
Forward Bisimulations for Nondeterministic Symbolic Finite Automata
Loris D'Antoni, Margus Veanes
TACAS | April 2017
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
Monadic Second-Order Logic on Finite Sequences
Loris D'Antoni, Margus Veanes
POPL'2017 | January 2017
Minimization of Symbolic Tree Automata
LICS | July 2016
LICS
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
Symbolic String Transformations with Regular Lookahead and Rollback
PSI 2014 | February 2015
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
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
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
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
Skolemization Modulo Theories
Konstantin Korovin, Margus Veanes
ICMS'14 | August 2014
Monadic Decomposition
Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
CAV'14 | July 2014
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
Minimization of Symbolic Automata
Loris D'Antoni, Margus Veanes
POPL'14 | January 2014
POPL'14
Effectively Monadic Predicates
Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
LPAR-19 | December 2013
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.
Applications of Symbolic Finite Automata
CIAA'13 | July 2013
Static Analysis of String Encoders and Decoders
Margus Veanes, Loris D'Antoni
VMCAI 2013 | January 2013
Symbolic Automata: The Toolkit
Margus Veanes, Nikolaj Bjørner
TACAS'12 | March 2012
Symbolic Finite State Transducers: Algorithms and Applications
Margus Veanes, Pieter Hooimeijer, David Molnar, Nikolaj Bjorner, Ben Livshits
POPL'12 | January 2012
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
Symbolic Tree Transducers
Margus Veanes, Nikolaj Bjørner
Ershov Informatics Conference (PSI'11) | January 2011
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
Qex: Symbolic SQL Query Explorer
Margus Veanes, Nikolai Tillmann, Jonathan "Peli" de Halleux
LPAR-16 | April 2010
Symbolic Query Exploration
Margus Veanes, Pavel Grigorenko, Jonathan "Peli" de Halleux, Nikolai Tillmann
ICFEM'09 | December 2009
Model-Based Testing of Web Applications using NModel
Juhan Ernits, Rivo Roo, Jonathan Jacky, Margus Veanes
LNCS, TESTCOM/FATES 2009 | November 2009
On Bounded Reachability of Programs with Set Comprehensions
Margus Veanes, Ando Saabas
LPAR'08 | November 2008
LPAR'08
Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract)
Margus Veanes, Ando Saabas
ABZ'08 | September 2008
This is an extended abstract.
Protocol Modeling with Model Program Composition
Margus Veanes, Wolfram Schulte
FORTE'08 | June 2008
ISBN: 978-3-540-68854-9
An SMT Approach to Bounded Reachability Analysis of Model Programs
Margus Veanes, Nikolaj Bjørner, Alexander Raschke
FORTE'08 | June 2008
FORTE'08
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
Enabling the Future Auto with Model-Driven Services
Johannes Helander, Margus Veanes
National Workshop on High-Confidence Automotive Cyber-Physical Systems. | April 2008
Adapting Futures: Scalability for Real-World Computing
Johannes Helander, Risto Serg, Margus Veanes, Pritam Roy
RTSS'07 | December 2007
Composition of Model Programs
Margus Veanes, Colin Campbell, Wolfram Schulte
FORTE | June 2007
ISBN: 978-3-540-73195-5
State Isomorphism in Model Programs with Abstract Data Structures
Margus Veanes, Juhan Ernits, Colin Campbell
FORTE'07 | June 2007
Online Testing with Reinforcement Learning
Margus Veanes, Pritam Roy, Colin Campbell
Formal Approaches to Software Testing and Runtime Verification, FATES/RV 2006 | January 2006
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
Play to Test
Andreas Blass, Yuri Gurevich, Lev Nachmanson, Margus Veanes
FATES 2005 | July 2005
Multiplexing of Partially Ordered Events
Colin Campbell, Margus Veanes, Jiale Huo, Alexandre Petrenko
TestCom 2005 | June 2005
Received Best paper award.
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
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
Exploration with Multiple State Groupings
Colin Campbell, Margus Veanes
Abstract State Machines 2005 | January 2005
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
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
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
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
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
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
Generating finite state machines from abstract state machines
Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
ISSTA 2002 | July 2002
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
High-level Executable Specification of the Universal Plug and Play Architecture
Uwe Glässer, Yuri Gurevich, Margus Veanes
HICSS 2002 | January 2002
-
Incremental Dead State Detection in Logarithmic Time
Caleb Stanford , Margus Veanes
January 2023
Preliminary and extended version of paper that appears in CAV 2023
-
Universal Plug and Play Machine Models
U. Glässer, Y. Gurevich, M. Veanes, Yuri Gurevich, Margus Veanes
MSR-TR-2001-59 | June 2001
The Relation Between Second-Order Unification and Simultaneous Rigid E-Unification
MPI-I-98-2-005 | February 1998
The decidability of simultaneous rigid E-unification with one variable
Paliath Narendran, Margus Veanes, Andrei Voronkov, Anatoli Degtyarev, Yuri Gurevich
139 | April 1997
Some undecidable problems related to the Herbrand theorem
Yuri Gurevich, Margus Veanes
UPMAIL-TR-138 | March 1997
On Computational Complexity of Basic Decision Problems of Finite Tree Automata
133 | January 1997
Uniform representation of recursively enumerable sets with simultaneous rigid E-unification
126 | June 1996
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.
Cycletrees: Flexible Interconnection Graphs for Parallel Computing
Margus Veanes, Jonas Barklund
97 | February 1995
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.
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
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.
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.
Fusing Effectful Comprehensions
Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi
MSR-TR-2016-55 | October 2016
PrePose: Security and Privacy for Gesture-Based Programming
Lucas Silva Figueiredo, Ben Livshits, David Molnar, Margus Veanes
MSR-TR-2014-146 | November 2014
FAST: A Transducer-Based Language for Tree Manipulation
Loris D'Antoni, Margus Veanes, Ben Livshits, David Molnar,
MSR-TR-2013-121 | November 2013
Minimization of Symbolic Automata
MSR-TR-2013-48 | April 2013
Equivalence of Extended Symbolic Finite Transducers
Loris D'Antoni, Margus Veanes,
MSR-TR-2013-4 | January 2013
Data-Parallel String-Manipulating Programs
Margus Veanes, David Molnar, Todd Mytkowicz, Ben Livshits
MSR-TR-2012-72 | July 2012
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
Symbolic Finite State Transducers: Algorithms and Applications
Nikolaj Bjørner, Ben Livshits, David Molnar, Margus Veanes
MSR-TR-2011-85 | July 2011
Decision Procedures for Composition and Equivalence of Symbolic Finite State Transducers
Margus Veanes, David Molnar, Ben Livshits
MSR-TR-2011-32 | March 2011
Symbolic Transducers
Nikolaj Bjørner, Margus Veanes
MSR-TR-2011-3 | January 2011
BEK: Modeling Imperative String Operations with Symbolic Transducers
, Ben Livshits, David Molnar, Prateek Saxena, Margus Veanes
MSR-TR-2010-154 | November 2010
An Evaluation of Automata Algorithms for String Analysis
MSR-TR-2010-90 | July 2010
Updated August, 2010
Modeling Imperative String Operations with Transducers
Pieter Hooimeijer, David Molnar, Prateek Saxena, Margus Veanes
MSR-TR-2010-96 | July 2010
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
Solving Extended Regular Constraints Symbolically
Margus Veanes, Nikolaj Bjørner, Leonardo de Moura
MSR-TR-2009-177 | December 2009
Rex: Symbolic Regular Expression Explorer
Margus Veanes, Jonathan "Peli" de Halleux, Nikolai Tillmann
MSR-TR-2009-137 | October 2009
ICST'10
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
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.
Symbolic Query Exploration
Margus Veanes, Pavel Grigorenko, Jonathan "Peli" de Halleux, Nikolai Tillmann
MSR-TR-2009-65 | May 2009
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.
Arranging Partitures for Models and Theorems
Johannes Helander, Margus Veanes
MSR-TR-2009-24 | March 2009
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.
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
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
On-The-Fly Testing of Reactive Systems
Margus Veanes, Colin Campbell, Wolfram Schulte, Pushmeet Kohli
MSR-TR-2005-05 | January 2005
An Abstract Communication Model
Uwe Glässer, Yuri Gurevich, Margus Veanes
MSR-TR-2002-55 | May 2002
Toward Industrial Strength Abstract State Machines
Yuri Gurevich, Wolfram Schulte, Margus Veanes
MSR-TR-2001-98 | October 2001
-
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
Farmer’s Theorem revisited
Information Processing Letters | April 2000, Vol 74: pp. 47-53
On the Undecidability of Second-Order Unification
Jordi Levy, Margus Veanes
Information and Computation | January 2000, Vol 159: pp. 125-150
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
Construction of natural cycletrees
Margus Veanes, Jonas Barklund
Information Processing Letters | January 1996, Vol 60: pp. 313-318
On the number of edges in cycletrees
Margus Veanes, Jonas Barklund
Information Processing Letters | January 1996, Vol 57: pp. 225-229
Natural cycletrees: Flexible interconnection graphs
Margus Veanes, Jonas Barklund
Journal of Parallel and Distributed Computing | January 1996, Vol 33: pp. 44-54
Monadic Decomposition
Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
Journal of the ACM | May 2017, Vol 64
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
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
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
Extended symbolic finite automata and transducers
Loris D’Antoni, Margus Veanes
Formal Methods in System Design | July 2015
Symbolic Tree Automata
Margus Veanes, Nikolaj Bjørner
Information Processing Letters | March 2015, Vol 115(3): pp. 418-424
Alternating simulation and IOCO
Margus Veanes, Nikolaj Bjørner
International Journal on Software Tools for Technology Transfer (STTT) | September 2011
Composing Model Programs for Analysis
Margus Veanes, Jonathan Jacky
The Journal of Logic and Algebraic Programming | October 2010, Vol 79: pp. 467-482
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
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
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
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
-
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.
-
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
-
On Simultaneous Rigid E-Unification
June 1997, pp. 120
June 1997
-
Cycletrees: a Novel Class of Interconnection Graphs
January 1993
January 1993