@inproceedings(DBLP:conf/fmcad/AlurBJMRSSSTU13,
 author       = "Rajeev Alur and Rastislav Bod\'{\i }k and Garvit Juniwal and Milo M. K. Martin and Mukund Raghothaman and Sanjit A. Seshia and Rishabh Singh and Armando Solar-Lezama and Emina Torlak and Abhishek Udupa",
 year         = "2013",
 title        = "Syntax-guided synthesis",
 booktitle    = "FMCAD",
 pages        = "1--17",
 doi          = "10.1109/FMCAD.2013.6679385",
)
@inproceedings(bloqqer,
 author       = "A. Biere and F. Lonsing and M. Seidl",
 year         = "2011",
 title        = "Blocked Clause Elimination for {QBF}",
 booktitle    = "CADE",
 pages        = "101--115",
 doi          = "10.1007/978-3-642-22438-6\_10",
)
@inproceedings(DBLP:conf/vmcai/BloemKS14,
 author       = "Roderick Bloem and Robert K{\"o}nighofer and Martina Seidl",
 year         = "2014",
 title        = "SAT-Based Synthesis Methods for Safety Specs",
 booktitle    = "VMCAI",
 pages        = "1--20",
 doi          = "10.1007/978-3-642-54013-4\_1",
)
@article(DBLP:journals/corr/ChengSRB13,
 author       = "Chih-Hong Cheng and Natarajan Shankar and Harald Ruess and Saddek Bensalem",
 year         = "2013",
 title        = "{EFSMT}: A Logical Framework for Cyber-Physical Systems",
 journal      = "CoRR",
 volume       = "abs/1306.3456",
 url          = "http://arxiv.org/abs/1306.3456",
)
@article(DBLP:journals/cacm/Dijkstra74,
 author       = "Edsger W. Dijkstra",
 year         = "1974",
 title        = "Self-stabilizing Systems in Spite of Distributed Control",
 journal      = "Commun. ACM",
 volume       = "17",
 number       = "11",
 pages        = "643--644",
 doi          = "10.1145/361179.361202",
)
@article(DBLP:journals/sttt/FinkbeinerS13,
 author       = "Bernd Finkbeiner and Sven Schewe",
 year         = "2013",
 title        = "Bounded synthesis",
 journal      = "STTT",
 volume       = "15",
 number       = "5-6",
 pages        = "519--539",
 doi          = "10.1007/s10009-012-0228-z",
)
@misc(supporting-sal-models,
 author       = "Adri{\`a} Gasc{\'o}n and Ashish Tiwari",
 title        = "Sal modules of the running example",
 howpublished = "Available at: \url {http://www.csl.sri.com/users/tiwari/softwares/synth_distributed}",
)
@inproceedings(DBLP:conf/nfm/GasconT14,
 author       = "Adria Gasc{\'o}n and Ashish Tiwari",
 year         = "2014",
 title        = "A Synthesized Algorithm for Interactive Consistency",
 booktitle    = "NASA Formal Methods",
 pages        = "270--284",
 doi          = "10.1007/978-3-319-06200-6\_23",
)
@inproceedings(rareqs,
 author       = "M. Janota and W. Klieber and J. Marques-Silva and E. M. Clarke",
 year         = "2012",
 title        = "Solving {QBF} with Counterexample Guided Refinement",
 booktitle    = "SAT",
 pages        = "114--128",
 doi          = "10.1007/978-3-642-31612-8\_10",
)
@inproceedings(DBLP:conf/lpar/JanotaGM13,
 author       = "Mikol{\'a}s Janota and Radu Grigore and Joao Marques-Silva",
 year         = "2013",
 title        = "On {QBF} Proofs and Preprocessing",
 booktitle    = "LPAR",
 pages        = "473--489",
 url          = "10.1007/978-3-642-45221-5\_32",
)
@inproceedings(DBLP:conf/sat/JanotaKMC12,
 author       = "Mikol{\'a}s Janota and William Klieber and Jo{\~a}o Marques-Silva and Edmund M. Clarke",
 year         = "2012",
 title        = "Solving {QBF} with Counterexample Guided Refinement",
 booktitle    = "SAT",
 pages        = "114--128",
 doi          = "10.1007/978-3-642-31612-8\_10",
)
@inproceedings(parametric-verification-helmut-veith,
 author       = "Annu John and Igor Konnov and Ulrich Schmid and Helmut Veith and Josef Widder",
 year         = "2013",
 title        = "Parameterized model checking of fault-tolerant distributed algorithms by abstraction",
 booktitle    = "FMCAD",
 pages        = "201--209",
 doi          = "10.1109/FMCAD.2013.6679411",
)
@article(byzantine-generals,
 author       = "Leslie Lamport and Robert E. Shostak and Marshall C. Pease",
 year         = "1982",
 title        = "The Byzantine Generals Problem",
 journal      = "ACM Trans. Program. Lang. Syst.",
 volume       = "4",
 number       = "3",
 pages        = "382--401",
 doi          = "10.1145/357172.357176",
)
@inproceedings(rushbyLincoln,
 author       = "Patrick Lincoln and John M. Rushby",
 year         = "1993",
 title        = "The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model",
 booktitle    = "CAV",
 pages        = "292--304",
 doi          = "10.1007/3-540-56922-7\_24",
)
@article(DBLP:journals/jsat/LonsingB10,
 author       = "Florian Lonsing and Armin Biere",
 year         = "2010",
 title        = "Dep{QBF}: A Dependency-Aware {QBF} Solver",
 journal      = "JSAT",
 volume       = "7",
 number       = "2-3",
 pages        = "71--76",
 url          = "http://jsat.ewi.tudelft.nl/content/volume7/JSAT7_6_Lonsing.pdf",
)
@book(lynch-book,
 author       = "Nancy A. Lynch",
 year         = "1996",
 title        = "Distributed Algorithms",
 publisher    = "Morgan Kaufmann",
)
@inproceedings(DBLP:conf/cav/MouraORRSST04,
 author       = "Leonardo Mendon\c {c}a de Moura and Sam Owre and Harald Rue{\ss } and John M. Rushby and Natarajan Shankar and Maria Sorea and Ashish Tiwari",
 year         = "2004",
 title        = "SAL 2",
 booktitle    = "CAV",
 pages        = "496--500",
 doi          = "10.1007/978-3-540-27813-9\_45",
)
@inproceedings(DBLP:conf/sat/NiemetzPLSB12,
 author       = "Aina Niemetz and Mathias Preiner and Florian Lonsing and Martina Seidl and Armin Biere",
 year         = "2012",
 title        = "Resolution-Based Certificate Extraction for {QBF} - (Tool Presentation)",
 booktitle    = "SAT",
 pages        = "430--435",
 doi          = "10.1007/978-3-642-31612-8\_33",
)
@inproceedings(DBLP:conf/cp/OlivoE11,
 author       = "Oswaldo Olivo and E. Allen Emerson",
 year         = "2011",
 title        = "A More Efficient BDD-Based {QBF} Solver",
 booktitle    = "CP",
 pages        = "675--690",
 doi          = "10.1007/978-3-642-23786-7\_51",
)
@inproceedings(ShankarRushbyVonHenkeOwre,
 author       = "Sam Owre and John M. Rushby and Natarajan Shankar and Friedrich W. von Henke",
 year         = "1993",
 title        = "Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned",
 booktitle    = "FME",
 pages        = "482--500",
 doi          = "10.1007/BFb0024663",
)
@inproceedings(DBLP:conf/sat/RanjanTM04,
 author       = "Darsh P. Ranjan and Daijue Tang and Sharad Malik",
 year         = "2004",
 title        = "A Comparative Study of {2QBF} Algorithms",
 booktitle    = "SAT",
 url          = "http://www.satisfiability.org/SAT04/programme/113.pdf",
)
@article(RushbyVonHenke,
 author       = "John M. Rushby and Friedrich W. von Henke",
 year         = "1993",
 title        = "Formal Verification of Algorithms for Critical Systems",
 journal      = "IEEE Trans. Software Eng.",
 volume       = "19",
 number       = "1",
 pages        = "13--23",
 doi          = "10.1109/32.210304",
)
@misc(sal-language,
 year         = "2003",
 title        = "The {SAL} intermediate language",
 note         = "Computer Science Laboratory, SRI International, Menlo Park, CA. \url {http://sal.csl.sri.com/}",
)
@inproceedings(Shankar,
 author       = "Natarajan Shankar",
 year         = "1992",
 title        = "Mechanical Verification of a Generalized Protocol for Byzantine Fault Tolerant Clock Synchronization",
 booktitle    = "FTRTFT",
 pages        = "217--236",
 doi          = "10.1007/3-540-55092-5\_12",
)
@inproceedings(DBLP:conf/pldi/Solar-LezamaRBE05,
 author       = "Armando Solar-Lezama and Rodric M. Rabbah and Rastislav Bod\'{\i }k and Kemal Ebcioglu",
 year         = "2005",
 title        = "Programming by sketching for bit-streaming programs",
 booktitle    = "PLDI",
 pages        = "281--294",
 doi          = "10.1145/1065010.1065045",
)
@inproceedings(DBLP:conf/asplos/Solar-LezamaTBSS06,
 author       = "Armando Solar-Lezama and Liviu Tancau and Rastislav Bod\'{\i }k and Sanjit A. Seshia and Vijay A. Saraswat",
 year         = "2006",
 title        = "Combinatorial Sketching for Finite Programs",
 booktitle    = "ASPLOS",
 pages        = "404--415",
 doi          = "10.1145/1168857.1168907",
)
@inproceedings(DBLP:conf/popl/SrivastavaGF10,
 author       = "Saurabh Srivastava and Sumit Gulwani and Jeffrey S. Foster",
 year         = "2010",
 title        = "From program verification to program synthesis",
 booktitle    = "POPL",
 pages        = "313--326",
 doi          = "10.1145/1706299.1706337",
)
@inproceedings(DBLP:conf/pldi/UdupaRDMMA13,
 author       = "Abhishek Udupa and Arun Raghavan and Jyotirmoy V. Deshmukh and Sela Mador-Haim and Milo M. K. Martin and Rajeev Alur",
 year         = "2013",
 title        = "TRANSIT: specifying protocols with concolic snippets",
 booktitle    = "PLDI",
 pages        = "287--296",
 doi          = "10.1145/2462156.2462174",
)
@inproceedings(DBLP:conf/aspdac/YuM05,
 author       = "Yinlei Yu and Sharad Malik",
 year         = "2005",
 title        = "Validating the result of a Quantified Boolean Formula ({QBF}) solver: theory and practice",
 booktitle    = "ASP-DAC",
 pages        = "1047--1051",
 doi          = "10.1145/1120725.1120821",
)