@inbook(productprograms,
 author       = {Gilles Barthe and Juan Manuel Crespo and C{\'e}sar Kunz},
 year         = {2011},
 title        = {Relational Verification Using Product Programs},
 pages        = {200--214},
 publisher    = {Springer Berlin Heidelberg},
 doi          = {10.1007/978-3-642-21437-0_17},
)
@article(arxiv,
 author       = {B. {Beckert} and T. {Bingmann} and M. {Kiefer} and P. {Sanders} and M. {Ulbrich} and A. {Weigl}},
 year         = {2018},
 title        = {{Relational Equivalence Proofs Between Imperative and MapReduce Algorithms}},
 journal      = {ArXiv e-prints},
 url          = {https://arxiv.org/abs/1801.08766},
)
@inproceedings(Thrill,
 author       = {Timo Bingmann and Michael Axtmann and Emanuel J{\"{o}}bstl and Sebastian Lamm and Huyen Chau Nguyen and Alexander Noe and Sebastian Schlag and Matthias Stumpp and Tobias Sturm and Peter Sanders},
 year         = {2016},
 title        = {{Thrill}: High-Performance Algorithmic Distributed Batch Data Processing with {C++}},
 booktitle    = {IEEE International Conference on Big Data},
 organization = {IEEE},
 pages        = {172--183},
 doi          = {10.1109/BigData.2016.7840603},
 note         = {Preprint \href{https://arxiv.org/abs/1608.05634}{arXiv:1608.05634}},
)
@misc(sparkspecification,
 author       = {Yu-Fang Chen and Chih-Duo Hong and Ond\v{r}ej Leng\'al and Shin-Cheng Mu and Nishant Sinha and Bow-Yaw Wang},
 year         = {2017},
 title        = {An Executable Sequential Specification for Spark Aggregation},
 url          = {https://arxiv.org/abs/1702.02439},
)
@inproceedings(DeAngelis16,
 author       = {{De Angelis}, Emanuele and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti},
 year         = {2016},
 title        = {Relational Verification Through Horn Clause Transformation},
 editor       = {Xavier Rival},
 booktitle    = {Static Analysis - 23rd International Symposium, {SAS} 2016, Edinburgh, UK, September 8-10, 2016, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {9837},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {147--169},
 doi          = {10.1007/978-3-662-53413-7_8},
)
@article(mapreduce,
 author       = {Jeffrey Dean and Sanjay Ghemawat},
 year         = {2008},
 title        = {{MapReduce}: Simplified Data Processing on Large Clusters},
 journal      = {Commun. ACM},
 volume       = {51},
 number       = {1},
 pages        = {107--113},
 doi          = {10.1145/1327452.1327492},
)
@inproceedings(automatingregver,
 author       = {Dennis Felsing and Sarah Grebing and Vladimir Klebanov and Philipp R\"{u}mmer and Mattias Ulbrich},
 year         = {2014},
 title        = {Automating Regression Verification},
 booktitle    = {Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering},
 series       = {ASE '14},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {349--360},
 doi          = {10.1145/2642937.2642987},
)
@inproceedings(rvt,
 author       = {Benny Godlin and Ofer Strichman},
 year         = {2009},
 title        = {Regression Verification},
 booktitle    = {Proceedings of the 46th Annual Design Automation Conference},
 series       = {DAC '09},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {466--471},
 doi          = {10.1145/1629911.1630034},
)
@inbook(equivalencespark,
 author       = {Shelly Grossman and Sara Cohen and Shachar Itzhaky and Noam Rinetzky and Mooly Sagiv},
 year         = {2017},
 title        = {Verifying Equivalence of Spark Programs},
 pages        = {282--300},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 doi          = {10.1007/978-3-319-63390-9_15},
)
@inproceedings(mutualsummaries,
 author       = {Chris Hawblitzel and Ming Kawaguchi and Shuvendu Lahiri and Henrique Reb\^elo},
 year         = {2011},
 title        = {Mutual Summaries: Unifying Program Comparison Techniques},
 booktitle    = {Informal proceedings of BOOGIE 2011 workshop},
 url          = {https://www.microsoft.com/en-us/research/publication/mutual-summaries-unifying-program-comparison-techniques/},
)
@article(translatingimperative,
 author       = {Cosmin Radoi and Stephen J. Fink and Rodric Rabbah and Manu Sridharan},
 year         = {2014},
 title        = {Translating Imperative Code to MapReduce},
 journal      = {SIGPLAN Not.},
 volume       = {49},
 number       = {10},
 pages        = {909--927},
 doi          = {10.1145/2714064.2660228},
)
@manual(Coq,
 author       = {The Coq development team},
 year         = {2004},
 title        = {The Coq proof assistant reference manual},
 organization = {LogiCal Project},
 url          = {http://coq.inria.fr},
 note         = {Version 8.6},
)
@book(white2012hadoop,
 author       = {Tom White},
 year         = {2012},
 title        = {Hadoop: The definitive guide},
 publisher    = {O'Reilly Media, Inc.},
)
@inproceedings(spark,
 author       = {Matei Zaharia and Mosharaf Chowdhury and Michael J. Franklin and Scott Shenker and Ion Stoica},
 year         = {2010},
 title        = {Spark: Cluster Computing with Working Sets},
 booktitle    = {Proceedings of the 2nd USENIX Conference on Hot Topics in Cloud Computing},
 series       = {HotCloud'10},
 publisher    = {USENIX Association},
 address      = {Berkeley, CA, USA},
 pages        = {10--10},
 url          = {http://dl.acm.org/citation.cfm?id=1863103.1863113},
)