@inproceedings(dAH05,
 author       = "L. de Alfaro and T.A. Henzinger",
 year         = "2005",
 title        = "Interface-based design",
 editor       = "M. Broy and J. Gr{\"u}nbauer and D. Harel and C.A.R. Hoare",
 booktitle    = "Engineering Theories of Software-intensive Systems",
 series       = "NATO Science Series: Mathematics, Physics, and Chemistry 195",
 publisher    = "Springer",
 pages        = "83--104",
)
@inproceedings(Alu07,
 author       = "R. Alur",
 year         = "2007",
 title        = "Marrying words and trees",
 booktitle    = "Proc.\ 26th ACM Symp. on Principles of Database Systems",
 pages        = "233--242",
 doi          = "10.1007/978-3-540-74510-5\_3",
)
@article(AABEIL08,
 author       = "R. Alur and M. Arenas and P. Barcel{\'o} and K. Etessami and N. Immerman and L. Libkin",
 year         = "2008",
 title        = "First-Order and Temporal Logics for Nested Words",
 journal      = "Logical Methods in Computer Science",
 volume       = "4",
 number       = "4",
)
@article(ABEGRY05,
 author       = "R. Alur and M. Benedikt and K. Etessami and P. Godefroid and T. W. Reps and M. Yannakakis",
 year         = "2005",
 title        = "Analysis of recursive state machines",
 journal      = "ACM Transactions on Programming Languagues and Systems",
 volume       = "27",
 number       = "4",
 pages        = "786--818",
 doi          = "10.1145/1075382.1075387",
)
@inproceedings(AEM04,
 author       = "R. Alur and K. Etessami and P. Madhusudan",
 year         = "2004",
 title        = "A temporal logic of nested calls and returns",
 booktitle    = "Proc.\ 10th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems",
 series       = "Lecture Notes in Computer Science",
 volume       = "2725",
 publisher    = "Springer",
 pages        = "67--79",
)
@article(AM09,
 author       = "R. Alur and P. Madhusudan",
 year         = "2009",
 title        = "Adding nesting structure to words",
 journal      = "Journal of the ACM",
 volume       = "56",
 number       = "3",
 pages        = "1--43",
 doi          = "10.1007/11779148\_1",
)
@inproceedings(BCLR04,
 author       = "T. Ball and B. Cook and V. Levin and S.K. Rajamani",
 year         = "2004",
 title        = "SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft",
 booktitle    = "Integrated Formal Methods",
 pages        = "1--20",
 doi          = "10.1007/978-3-540-24756-2\_1",
)
@inproceedings(BCGLM03,
 author       = "D. Berardi and D. Calvanese and G. De Giacomo and M. Lenzerini and M. Mecella",
 year         = "2003",
 title        = "Automatic Composition of E-services That Export Their Behavior",
 booktitle    = "ICSOC",
 pages        = "43--58",
 doi          = "10.1007/978-3-540-24593-3\_4",
)
@article(HOL97,
 author       = "G.J. Holzmann",
 year         = "1997",
 title        = "The Model Checker {SPIN}",
 journal      = "IEEE Transactions on Software Engineering",
 volume       = "23",
 number       = "5",
 pages        = "279--295",
)
@inproceedings(KLVY11,
 author       = "O. Kupferman and Y. Lustig and M.Y. Vardi and M. Yannakakis",
 year         = "2011",
 title        = "Temporal Synthesis for Bounded Systems and Environments",
 booktitle    = "Proc. 28th Symp. on Theoretical Aspects of Computer Science",
 pages        = "615--626",
)
@inproceedings(KV05c,
 author       = "O. Kupferman and M.Y. Vardi",
 year         = "2005",
 title        = "Safraless Decision Procedures",
 booktitle    = "Proc.\ 46th IEEE Symp. on Foundations of Computer Science",
 pages        = "531--540",
 doi          = "10.1109/SFCS.2005.66",
)
@inproceedings(LV09,
 author       = "Y. Lustig and Moshe Y. Vardi",
 year         = "2009",
 title        = "Synthesis from Component Libraries",
 booktitle    = "Proc. 12th International Conference on Foundations of Software Science and Computational Structures (FOSSACS)",
 series       = "Lecture Notes in Computer Science",
 volume       = "5504",
 publisher    = "Springer",
 pages        = "395 -- 409",
 doi          = "10.1007/978-3-642-00596-1\_28",
)
@inproceedings(PV01,
 author       = "N. Piterman and M. Vardi",
 year         = "2001",
 title        = "From Bidirectionality to Alternation",
 booktitle    = "26th Int. Symp. on Mathematical Foundations of Computer Science",
 series       = "Lecture Notes in Computer Science",
 volume       = "2136",
 publisher    = "Springer",
 pages        = "598--609",
 doi          = "10.1016/S0304-3975(02)00410-3",
)
@inproceedings(PR89a,
 author       = "A. Pnueli and R. Rosner",
 year         = "1989",
 title        = "On the Synthesis of a Reactive Module",
 booktitle    = "Proc.\ 16th ACM Symp. on Principles of Programming Languages",
 pages        = "179--190",
)
@inproceedings(SPG07,
 author       = "S. Sardi{\~n}a and F. Patrizi and G. {De Giacomo}",
 year         = "2007",
 title        = "Automatic Synthesis of a Global Behavior from Multiple Distributed Behaviors",
 booktitle    = "AAAI",
 pages        = "1063--1069",
)
@inproceedings(Sif05,
 author       = "J. Sifakis",
 year         = "2005",
 title        = "A Framework for Component-based Construction Extended Abstract",
 booktitle    = "Proc. 3rd Int. Conf. on Software Engineering and Formal Methods",
 publisher    = "IEEE Computer Society",
 pages        = "293--300",
 doi          = "10.1109/SEFM.2005.3",
)
@inproceedings(Var98,
 author       = "M.Y. Vardi",
 year         = "1998",
 title        = "Reasoning about the past with two-way automata",
 booktitle    = "Proc.\ 25th Int. Colloq. on Automata, Languages, and Programming",
 series       = "Lecture Notes in Computer Science",
 volume       = "1443",
 publisher    = "Springer, Berlin",
 pages        = "628--641",
)
@article(VW94,
 author       = "M.Y. Vardi and P. Wolper",
 year         = "1994",
 title        = "Reasoning about Infinite Computations",
 journal      = "Information and Computation",
 volume       = "115",
 number       = "1",
 pages        = "1--37",
)