@article(AK,
 author       = "Krzysztof R. Apt and Dexter Kozen",
 year         = "1986",
 title        = "Limits for Automatic Verification of Finite-State Concurrent Systems",
 journal      = "Inf. Process. Lett.",
 volume       = "22",
 number       = "6",
 pages        = "307--309",
 doi          = "10.1016/0020-0190(86)90071-2",
)
@book(gpintro,
 author       = "W. Banzhaf and P. Nordin and R. E. Keller and F. D. Francone",
 year         = "2001",
 title        = "Genetic Programming -- An Introduction; On the Automatic Evolution of Computer Programs and its Applications (3rd edition)",
 publisher    = "Morgan Kaufmann, dpunkt.verlag",
)
@inproceedings(BT,
 author       = "Yoah Bar-David and Gadi Taubenfeld",
 year         = "2003",
 title        = "Automatic discovery of mutual exclusion algorithms",
 booktitle    = "PODC",
 pages        = "305",
 doi          = "10.1145/872035.872080",
)
@article(one-bit,
 author       = "James E. Burns and Nancy A. Lynch",
 year         = "1993",
 title        = "Bounds on Shared Memory for Mutual Exclusion",
 journal      = "Information and Computation",
 volume       = "107",
 number       = "2",
 pages        = "171--184",
 doi          = "10.1006/inco.1993.1065",
)
@article(Dijkstra,
 author       = "Edsger W. Dijkstra",
 year         = "1965",
 title        = "Solution of a problem in concurrent programming control",
 journal      = "Commun. ACM",
 volume       = "8",
 number       = "9",
 pages        = "569",
 doi          = "10.1145/365559.365617",
)
@inproceedings(EN,
 author       = "E. Allen Emerson and Kedar S. Namjoshi",
 year         = "1995",
 title        = "Reasoning about Rings",
 booktitle    = "POPL",
 pages        = "85--94",
 doi          = "10.1145/199448.199468",
)
@inproceedings(Gul1,
 author       = "Sumit Gulwani and Susmit Jha and Ashish Tiwari and Ramarathnam Venkatesan",
 year         = "2011",
 title        = "Synthesis of loop-free programs",
 booktitle    = "PLDI",
 pages        = "62--73",
 doi          = "10.1145/1993498.1993506",
)
@inproceedings(KP1,
 author       = "Gal Katz and Doron Peled",
 year         = "2008",
 title        = "Genetic Programming and Model Checking: Synthesizing New Mutual Exclusion Algorithms",
 booktitle    = "ATVA",
 series       = "LNCS",
 volume       = "5311",
 pages        = "33--47",
 doi          = "10.1007/978-3-540-88387-6\_5",
)
@inproceedings(KP2,
 author       = "Gal Katz and Doron Peled",
 year         = "2008",
 title        = "Model Checking-Based Genetic Programming with an Application to Mutual Exclusion",
 booktitle    = "TACAS",
 series       = "LNCS",
 volume       = "4963",
 pages        = "141--156",
 doi          = "10.1007/978-3-540-78800-3\_11",
)
@inproceedings(KP4,
 author       = "Gal Katz and Doron Peled",
 year         = "2009",
 title        = "Synthesizing Solutions to the Leader Election Problem using Model Checking and Genetic Programming",
 booktitle    = "HVC",
 series       = "LNCS",
 volume       = "6405",
 pages        = "117--132",
 doi          = "10.1007/978-3-642-19237-1\_13",
)
@inproceedings(KP5,
 author       = "Gal Katz and Doron Peled",
 year         = "2010",
 title        = "Code Mutation in Verification and Automatic Code Correction",
 booktitle    = "TACAS",
 series       = "LNCS",
 pages        = "435--450",
 doi          = "10.1007/978-3-642-12002-2\_36",
)
@inproceedings(KP6,
 author       = "Gal Katz and Doron Peled",
 year         = "2010",
 title        = "MCGP: A Software Synthesis Tool Based on Model Checking and Genetic Programming",
 booktitle    = "ATVA",
 pages        = "359--364",
 doi          = "10.1007/978-3-642-15643-4\_28",
)
@article(Kessels,
 author       = "Joep L. W. Kessels",
 year         = "1982",
 title        = "Arbitration Without Common Modifiable Variables",
 journal      = "Acta Inf.",
 volume       = "17",
 pages        = "135--141",
 doi          = "10.1007/BF00288966",
)
@inproceedings(z3,
 author       = "Leonardo Mendon\c {c}a de Moura and Nikolaj Bj{\o }rner",
 year         = "2008",
 title        = "Z3: An Efficient SMT Solver",
 booktitle    = "TACAS",
 pages        = "337--340",
 doi          = "10.1007/978-3-540-78800-3\_24",
)
@inproceedings(NPP,
 author       = "Peter Niebert and Doron Peled and Amir Pnueli",
 year         = "2008",
 title        = "Discriminative Model Checking",
 booktitle    = "CAV",
 series       = "LNCS",
 volume       = "5123",
 publisher    = "Springer",
 pages        = "504--516",
 doi          = "10.1007/978-3-540-70545-1\_48",
)
@book(SRM,
 author       = "Doron Peled",
 year         = "2001",
 title        = "Software Reliability Methods",
 publisher    = "Springer",
 doi          = "10.1007/978-1-4757-3540-6",
)
@article(alpha,
 author       = "Jose Antonio Perez and Rafael Corchuelo and Miguel Toro",
 year         = "2004",
 title        = "An order-based algorithm for implementing multiparty synchronization",
 journal      = "Concurrency - Practice and Experience",
 volume       = "16",
 number       = "12",
 pages        = "1173--1206",
 doi          = "10.1002/cpe.903",
)
@inproceedings(PetersonF77,
 author       = "Peterson and Fischer",
 year         = "1977",
 title        = "Economical Solutions to the Critical Section Problem in a Distributed System",
 booktitle    = "STOC: ACM Symposium on Theory of Computing (STOC)",
 pages        = "91--97",
 doi          = "10.1145/800105.803398",
)
@inproceedings(PR1,
 author       = "Amir Pnueli and Roni Rosner",
 year         = "1989",
 title        = "On the Synthesis of a Reactive Module",
 booktitle    = "POPL",
 pages        = "179--190",
 doi          = "10.1145/75277.75293",
)
@inproceedings(PR2,
 author       = "Amir Pnueli and Roni Rosner",
 year         = "1990",
 title        = "Distributed Reactive Systems Are Hard to Synthesize",
 booktitle    = "FOCS",
 pages        = "746--757",
 doi          = "10.1109/FSCS.1990.89597",
)
@inproceedings(Tsay,
 author       = "Yih-Kuen Tsay",
 year         = "1998",
 title        = "Deriving a Scalable Algorithm for Mutual Exclusion",
 booktitle    = "DISC",
 pages        = "393--407",
 doi          = "10.1007/BFb0056497",
)
@book(hack,
 author       = "Henry S. Warren",
 year         = "2002",
 title        = "Hacker's Delight",
 publisher    = "Addison-Wesley Longman Publishing Co., Inc.",
 address      = "Boston, MA, USA",
)