@inproceedings(barnett2005weakest,
 doi          = {10.1145/1108792.1108813},
)
@inproceedings(berdine2005symbolic,
 doi          = {10.1007/11575467_5},
)
@incollection(bjorner2015horn,
 doi          = {10.1007/978-3-319-23534-9_2},
)
@techreport(bobot2011why3,
 url          = {https://hal.inria.fr/hal-00822856},
)
@inproceedings(ernst:cav2019,
 doi          = {10.1007/978-3-030-25543-5_13},
)
@article(ernst:sttt2015,
 doi          = {10.1007/s10009-014-0308-3},
)
@inproceedings(ernst2019verifythis,
 doi          = {10.1007/978-3-030-17502-3_12},
)
@inproceedings(fragoso2020gillian,
 doi          = {10.1145/3385412.3386014},
)
@inproceedings(hentschel2016interactive,
 doi          = {10.1145/2970276.2970292},
)
@article(huet1997zipper,
 doi          = {10.1017/S0956796897002864},
)
@inproceedings(jacobs2011verifast,
 doi          = {10.1007/978-3-642-20398-5_4},
)
@inproceedings(le2011boogie,
 doi          = {10.1007/978-3-642-24690-6_28},
)
@inproceedings(leino2014dafny,
 doi          = {10.4204/EPTCS.149.2},
)
@inproceedings(masci2019pvs,
 doi          = {10.4204/EPTCS.310.5},
)
@article(plotkin2004origins,
 doi          = {10.1016/j.jlap.2004.03.009},
)
@article(ramsey2006applicative,
 doi          = {10.1016/j.entcs.2005.11.042},
)
@inproceedings(rask2021visual,
 url          = {https://arxiv.org/abs/2101.07261},
)
@inproceedings(voisin2014rodin,
 doi          = {10.1007/978-3-662-43652-3_1},
)
@inproceedings(wenzel2018isabelle,
 doi          = {10.1007/978-3-642-31374-5_38},
)