Regex Decision Procedures in Extended RE#
Ian Erik Varatalu, Margus Veanes, Ekaterina Zhuchko, Juhan Ernits
CAV 2025 | July 2025
編集者: R. Piskac and Z. Rakamaric
Published in LNCS vol. 15933
Margus Veanes
Principal Researcher
出版物
-
-
-
RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement, and Restricted Lookarounds
Ian Erik Varatalu, Margus Veanes, Juhan Ernits
POPL | January 2025
-
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
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
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
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
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
編集者: 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, 巻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, 巻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, 巻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, 巻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, 巻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 | 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, 巻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, 巻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, 巻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, 巻243(1-2): pp. 167-184
-
Farmer’s Theorem revisited
Information Processing Letters | April 2000, 巻74: pp. 47-53
-
On the Undecidability of Second-Order Unification
Jordi Levy, Margus Veanes
Information and Computation | January 2000, 巻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, 巻60: pp. 313-318
-
Natural cycletrees: Flexible interconnection graphs
Margus Veanes, Jonas Barklund
Journal of Parallel and Distributed Computing | January 1996, 巻33: pp. 44-54
-
On the number of edges in cycletrees
Margus Veanes, Jonas Barklund
Information Processing Letters | January 1996, 巻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
-
-
-
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, 巻243(1-2): pp. 167-184
-
Farmer’s Theorem revisited
Information Processing Letters | April 2000, 巻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, 巻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
-
Regex Decision Procedures in Extended RE#
Ian Erik Varatalu, Margus Veanes, Ekaterina Zhuchko, Juhan Ernits
CAV 2025 | July 2025
編集者: R. Piskac and Z. Rakamaric
Published in LNCS vol. 15933
-
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
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
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
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
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
編集者: 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, 巻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, 巻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, 巻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 | 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, 巻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, 巻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, 巻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, 巻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
編集者: 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, 巻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, 巻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, 巻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, 巻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
-
-
-
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
-
Regex Decision Procedures in Extended RE#
Ian Erik Varatalu, Margus Veanes, Ekaterina Zhuchko, Juhan Ernits
CAV 2025 | July 2025
編集者: R. Piskac and Z. Rakamaric
Published in LNCS vol. 15933
-
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
編集者: 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
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
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
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
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, 巻243(1-2): pp. 167-184
-
Farmer’s Theorem revisited
Information Processing Letters | April 2000, 巻74: pp. 47-53
-
On the Undecidability of Second-Order Unification
Jordi Levy, Margus Veanes
Information and Computation | January 2000, 巻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, 巻60: pp. 313-318
-
On the number of edges in cycletrees
Margus Veanes, Jonas Barklund
Information Processing Letters | January 1996, 巻57: pp. 225-229
-
Natural cycletrees: Flexible interconnection graphs
Margus Veanes, Jonas Barklund
Journal of Parallel and Distributed Computing | January 1996, 巻33: pp. 44-54
-
Monadic Decomposition
Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
Journal of the ACM | May 2017, 巻64
-
Prepose: Privacy, Security, and Reliability for Gesture-Based Programming
Lucas Silva Figueiredo , David Molnar, Margus Veanes, Benjamin Livshits
IEEE Security & Privacy | April 2017, 巻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, 巻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, 巻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, 巻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, 巻376: pp. 17-29
-
Abstract Communication Model for Distributed Systems
Uwe Glässer, Yuri Gurevich, Margus Veanes
IEEE Transactions on Software Engineering | July 2004, 巻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, 巻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 | 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
-