@inproceedings(aguirre17,
 author       = {Alejandro Aguirre and Gilles Barthe and Marco Gaboardi and Deepak Garg and Pierre-Yves Strub},
 year         = {2017},
 title        = {A Relational Logic for Higher-Order Programs},
 booktitle    = {{ICFP}},
 doi          = {10.1145/3110265},
)
@inproceedings(albarg13,
 author       = {Aws Albarghouthi and Kenneth L. McMillan},
 year         = {2013},
 title        = {Beautiful Interpolants},
 booktitle    = {{CAV}},
 doi          = {10.1007/978-3-642-39799-8_22},
)
@inproceedings(banerjee16,
 author       = {Anindya Banerjee, David A. Naumann and Mohammad Nikouei},
 year         = {2016},
 title        = {Relational Logic with Framing and Hypotheses},
 booktitle    = {FSTTCS},
 doi          = {10.4230/LIPIcs.FSTTCS.2016.11},
)
@inproceedings(backes13,
 author       = {John D. Backes and Suzette Person and Neha Rungta and Oksana Tkachuk},
 year         = {2013},
 title        = {Regression Verification Using Impact Summaries},
 booktitle    = {{SPIN}},
 doi          = {10.1007/978-3-642-39176-7_7},
)
@inproceedings(barthe11,
 author       = {Gilles Barthe and Juan Manuel Crespo and C{\'{e}}sar Kunz},
 year         = {2011},
 title        = {Relational Verification Using Product Programs},
 booktitle    = {{FM}},
 doi          = {10.1007/978-3-642-21437-0_17},
)
@inproceedings(barthe13,
 author       = {Gilles Barthe and Juan Manuel Crespo and C{\'{e}}sar Kunz},
 year         = {2013},
 title        = {Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification},
 booktitle    = {{LNCS}},
 doi          = {10.1007/978-3-642-35722-0_3},
)
@inproceedings(barthe16,
 author       = {Gilles Barthe and Juan Manuel Crespo and C{\'{e}}sar Kunz},
 year         = {2016},
 title        = {Product Programs and Relational Program Logics},
 booktitle    = {{JLAMP}},
 doi          = {10.1016/j.jlamp.2016.05.004},
)
@inproceedings(barthe04,
 author       = {Gilles Barthe and Pedro R. D'Argenio and Tamara Rezk},
 year         = {2004},
 title        = {Secure Information Flow by Self-Composition},
 booktitle    = {{CSFW-17}},
 doi          = {10.1017/S0960129511000193},
)
@inproceedings(beringer11,
 author       = {Lennart Beringer},
 year         = {2011},
 title        = {Relational Decomposition},
 booktitle    = {ITP},
 doi          = {10.1007/978-3-642-22863-6_6},
)
@inproceedings(bjorner13,
 author       = {Bj{\o}rner, Nikolaj and Kenneth L. McMillan and Andrey Rybalchenko},
 year         = {2013},
 title        = {On Solving Universally Quantified {Horn} Clauses},
 booktitle    = {{SAS}},
 doi          = {10.1007/978-3-642-38856-9_8},
)
@inproceedings(bohme13,
 author       = {Marcel B{\"{o}}hme and Bruno C. d. S. Oliveira and Abhik Roychoudhury},
 year         = {2013},
 title        = {Partition-based regression verification},
 booktitle    = {{ICSE}},
 doi          = {10.1109/ICSE.2013.6606576},
)
@inproceedings(deangelis16,
 author       = {Alberto Pettorossi Emanuele De Angelis, Fabio Fioravanti and Maurizio Proietti},
 year         = {2016},
 title        = {Verifying Relational Program Properties by Transforming Constrained {Horn} Clauses},
 booktitle    = {{CILC}},
)
@inproceedings(felsing14,
 author       = {Dennis Felsing and Sarah Grebing and Vladimir Klebanov and Philipp R{\"{u}}mmer and Mattias Ulbrich},
 year         = {2014},
 title        = {Automating regression verification},
 booktitle    = {{ASE}},
 doi          = {10.1145/2642937.2642987},
)
@inproceedings(godlin09,
 author       = {Benny Godlin and Ofer Strichman},
 year         = {2009},
 title        = {Regression verification},
 booktitle    = {{DAC}},
 doi          = {10.1145/1629911.1630034},
)
@inproceedings(hawblitzel13,
 author       = {Chris Hawblitzel and Ming Kawaguchi and Shuvendu K. Lahiri and Henrique Reb{\^{e}}lo},
 year         = {2013},
 title        = {Towards Modularly Comparing Programs Using Automated Theorem Provers},
 booktitle    = {{CADE-24}},
 doi          = {10.1007/978-3-642-38574-2_20},
)
@misc(leetcode,
 year         = {2016},
 title        = {LeetCode Online Judge},
 howpublished = {\url{https://leetcode.com/}},
 note         = {Accessed: 2015 Nov 16},
)
@article(lopes16,
 author       = {Nuno P. Lopes and Jos{\'{e}} Monteiro},
 year         = {2016},
 title        = {Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic},
 journal      = {{STTT}},
 volume       = {18},
 number       = {4},
 doi          = {10.1007/s10009-015-0366-1},
)
@inproceedings(kiefer16,
 author       = {Mattias Ulbrich Moritz Kiefer, Vladimir Klevanov},
 year         = {2016},
 title        = {Relational Program Reasoning Using Compiler IR},
 booktitle    = {{VSTTE}},
 doi          = {10.1007/s10817-017-9433-5},
)
@inproceedings(Lauren18,
 author       = {Lauren Pick and Grigory Fedyukovich and Aartic Gupta},
 year         = {2018},
 title        = {Exploiting Synchrony and Symmetry in Relational Verification},
 booktitle    = {{CAV}},
 doi          = {10.1007/978-3-319-96145-3_9},
)
@book(pierce17,
 author       = {Benjamin C. Pierce and Arthur Azevedo de Amorim and Chris Casinghino and Marco Gaboardi and Michael Greenberg and Hri\c{t}cu, C\v{a}t\v{a}lin and Vilhelm Sj\"{o}berg and Brent Yorgey},
 year         = {2018},
 title        = {Logical Foundations},
 series       = {Software Foundations series, volume 1},
 publisher    = {Electronic textbook},
 note         = {Version 5.5. \url{http://www.cis.upenn.edu/~bcpierce/sf}},
)
@inproceedings(sousa16,
 author       = {Marcelo Sousa and Isil Dillig},
 year         = {2016},
 title        = {Cartesian {Hoare} logic for verifying k-safety properties},
 booktitle    = {{PLDI}},
 doi          = {10.1145/2980983.2908092},
)
@inproceedings(terauchi05,
 author       = {Tachio Terauchi and Alexander Aiken},
 year         = {2005},
 title        = {Secure Information Flow as a Safety Problem},
 booktitle    = {{SAS}},
 doi          = {10.1007/11547662_24},
)
@inproceedings(unno17,
 author       = {Hiroshi Unno and Sho Torii},
 year         = {2017},
 title        = {Automating Induction for Solving {Horn} Clauses},
 booktitle    = {{CAV}},
 doi          = {10.1007/978-3-319-63390-9_30},
)
@misc(z3,
 year         = {2017},
 title        = {Z3Prover/z3 - GitHub},
 howpublished = {\url{https://github.com/Z3Prover/z3}},
 note         = {Accessed: 2017 July 1},
)