biblio.bib

@book{programmingElixir,
  author={Dave Thomas},
  title={Programming Elixir},
  publisher={The Pragmatic Programmers},
  year=2018
}

@book{metaprogrammingElixir,
  author={Chris McCord},
  title={Metaprogramming Elixir},
  publisher={The Pragmatic Programmers},
  year=2015
}

@book{masteringElixir,
  author={Andr\'{e} Albuquerque and Daniel Caixinha},
  title={Mastering Elixir},
  publisher={Packt Publishing},
  year=2018
}

@book{smtLibStandard,
  author={Clark Barrett and Pascal Fontaine and Cesare Tinelli},
  title={The SMT-LIB Standard},
  publisher={Digital version},
  year=2017
}

@book{DafnyManual,
  author={Richard L. Ford and K. Rustan M. Leino},
  title={Dafny Reference Manual},
  publisher={Digital version},
  year=2017
}

@book{Why3Manual,
  author={Fran\c{c}ois Bobot and Jean-Christophe Filli\^{a}tre and Claude March\'{e} and Guillaume Melquiond and Andrei Paske-vich},
  title={Why3 Documentation},
  publisher={Digital version},
  year=2022
}

@book{lindholm2013java,
  title={The Java Virtual Machine Specification, Java SE 7 Edition: Java Virt Mach Spec Java\_3},
  author={Lindholm, Tim and Yellin, Frank and Bracha, Gilad and Buckley, Alex},
  year={2013},
  publisher={Addison-Wesley}
}

@book{stenman2015erlang,
  title={The Erlang Run-Time System},
  author={Stenman, E.},
  year={2015},
  publisher={Oreilly \& Associates Incorporated}
}

@misc{ElixirDocs,
  title={{Elixir} documentation in {Hex}},
  howpublished={\url{https://hexdocs.pm/elixir}},
  year=2022
}

@misc{ErlangDocs,
  title={{Erlang} documentation},
  howpublished={\url{https://www.erlang.org/doc/}},
  year=2022
}

@misc{NimbleDocs,
  title={{NimbleParsec} documentation in {Hex}},
  howpublished={\url{https://hexdocs.pm/nimble_parsec}},
  year=2022
}

@inproceedings{Why3,
  title={Why3: {S}hepherd your herd of provers},
  author={Bobot, Fran{\c{c}}ois and Filli{\^a}tre, Jean-Christophe and March{\'e}, Claude and Paskevich, Andrei},
  booktitle={Boogie 2011: First International Workshop on Intermediate Verification Languages},
  pages={53--64},
  year={2011}
}

@inproceedings{wasm,
  title={Bringing the web up to speed with {W}eb{A}ssembly},
  author={Haas, Andreas and Rossberg, Andreas and Schuff, Derek L and Titzer, Ben L and Holman, Michael and Gohman, Dan and Wagner, Luke and Zakai, Alon and Bastien, JF},
  booktitle={Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation},
  pages={185--200},
  year={2017}
}

@article{erlangveri,
  title={A verification tool for {E}rlang},
  author={Fredlund, Lars--{\AA}ke and Gurov, Dilian and Noll, Thomas and Dam, Mads and Arts, Thomas and Chugunov, Gennady},
  journal={International Journal on Software Tools for Technology Transfer},
  volume={4},
  number={4},
  pages={405--420},
  year={2003},
  publisher={Springer}
}

@inproceedings{viper,
  title={Viper: {A} verification infrastructure for permission-based reasoning},
  author={M{\"u}ller, Peter and Schwerhoff, Malte and Summers, Alexander J},
  booktitle={International conference on verification, model checking, and abstract interpretation},
  pages={41--62},
  year={2016},
  organization={Springer}
}

@article{Boogie2,
  title={This is {B}oogie 2},
  author={Leino, K Rustan M},
  journal={manuscript KRML},
  volume={178},
  number={131},
  pages={9},
  year={2008},
  publisher={Citeseer}
}

@inproceedings{caviart,
  title={A generic intermediate representation for verification condition generation},
  author={Montenegro, Manuel and Pe{\~n}a, Ricardo and S{\'a}nchez-Hern{\'a}ndez, Jaime},
  booktitle={International Symposium on Logic-Based Program Synthesis and Transformation},
  pages={227--243},
  year={2015},
  organization={Springer}
}

@article{horn,
  title={Horn clauses as an intermediate representation for program analysis and transformation},
  author={Gange, Graeme and Navas, Jorge A and Schachte, Peter and S{\o}ndergaard, Harald and Stuckey, Peter J},
  journal={Theory and Practice of Logic Programming},
  volume={15},
  number={4-5},
  pages={526--542},
  year={2015},
  publisher={Cambridge University Press}
}

@article{LLVM,
  title={The {LLVM} instruction set and compilation strategy},
  author={Lattner, Chris and Adve, Vikram},
  journal={CS Dept., Univ. of Illinois at Urbana-Champaign, Tech. Report UIUCDCS},
  year={2002},
  publisher={Citeseer}
}

@article{Dialyzer,
  title={The {DIALYZER}: a {DI}screpancy {A}na{LYZ}er for {ER}lang programs},
  author={Lindahl, Tobias},
  year={2012},
  publisher={Uppsala University, Sweden}
}

@article{cavilisp,
  title={Processing an Intermediate Representation Written in Lisp},
  author={Pe{\~n}a, Ricardo and Saavedra, Santiago and S{\'a}nchez-Hern{\'a}ndez, Jaime},
  year={2016}
}

@inproceedings{FormalizingLLVMIR,
  title={Formalizing the {LLVM} intermediate representation for verified program transformations},
  author={Zhao, Jianzhou and Nagarakatte, Santosh and Martin, Milo MK and Zdancewic, Steve},
  booktitle={Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
  pages={427--440},
  year={2012}
}

@inproceedings{DPLL,
  title={{DPLL(T)}: {F}ast decision procedures},
  author={Ganzinger, Harald and Hagen, George and Nieuwenhuis, Robert and Oliveras, Albert and Tinelli, Cesare},
  booktitle={International Conference on Computer Aided Verification},
  pages={175--188},
  year={2004},
  organization={Springer}
}

@inproceedings{cadar2008klee,
  title={Unassisted and {A}utomatic {G}eneration of {H}igh-{C}overage {T}ests for {C}omplex {S}ystems {P}rograms},
  author={Cadar, Cristian and Dunbar, Daniel and Engler, Dawson R and others},
  booktitle={OSDI},
  volume={8},
  pages={209--224},
  year={2008}
}

@inproceedings{lindner2018no,
  title={No panic! {V}erification of {R}ust programs by symbolic execution},
  author={Lindner, Marcus and Aparicius, Jorge and Lindgren, Per},
  booktitle={2018 IEEE 16th International Conference on Industrial Informatics (INDIN)},
  pages={108--114},
  year={2018},
  organization={IEEE}
}

@inproceedings{astrauskas2022prusti,
  title={The {P}rusti {P}roject: {F}ormal {V}erification for {R}ust},
  author={Astrauskas, Vytautas and B{\'\i}l{\`y}, Aurel and Fiala, Jon{\'a}{\v{s}} and Grannan, Zachary and Matheja, Christoph and M{\"u}ller, Peter and Poli, Federico and Summers, Alexander J},
  booktitle={NASA Formal Methods Symposium},
  pages={88--108},
  year={2022},
  organization={Springer}
}

@inproceedings{barrett2011cvc4,
  title={Cvc4},
  author={Barrett, Clark and Conway, Christopher L and Deters, Morgan and Hadarean, Liana and Jovanovi{\'c}, Dejan and King, Tim and Reynolds, Andrew and Tinelli, Cesare},
  booktitle={International Conference on Computer Aided Verification},
  pages={171--177},
  year={2011},
  organization={Springer}
}

@article{dutertre2006yices,
  title={The {Y}ices {SMT} solver},
  author={Dutertre, Bruno and De Moura, Leonardo},
  journal={Tool paper at http://yices. csl. sri. com/tool-paper. pdf},
  volume={2},
  number={2},
  pages={1--2},
  year={2006}
}

@inproceedings{bozzano2005mathsat,
  title={The {MATHSAT} 3 system},
  author={Bozzano, Marco and Bruttomesso, Roberto and Cimatti, Alessandro and Junttila, Tommi and Rossum, Peter van and Schulz, Stephan and Sebastiani, Roberto},
  booktitle={International Conference on Automated Deduction},
  pages={315--321},
  year={2005},
  organization={Springer}
}

@inproceedings{moura2008z3,
  title={Z3: {A}n efficient {SMT} solver},
  author={Moura, Leonardo de and Bj{\o}rner, Nikolaj},
  booktitle={International conference on Tools and Algorithms for the Construction and Analysis of Systems},
  pages={337--340},
  year={2008},
  organization={Springer}
}

@inproceedings{proper,
  title={A {PropEr} {I}ntegration of {T}ypes and {F}unction Specifications with {P}roperty-{B}ased {T}esting},
  author={Papadakis, Manolis and Sagonas, Konstantinos},
  booktitle={Proceedings of the 10th ACM SIGPLAN workshop on Erlang},
  pages={39--50},
  year={2011}
}

@inproceedings{quickcheck,
  title={Quick{C}heck testing for fun and profit},
  author={Hughes, John},
  booktitle={International Symposium on Practical Aspects of Declarative Languages},
  pages={1--32},
  year={2007},
  organization={Springer}
}

@inproceedings{rosen1988global,
  title={Global value numbers and redundant computations},
  author={Rosen, Barry K and Wegman, Mark N and Zadeck, F Kenneth},
  booktitle={Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
  pages={12--27},
  year={1988}
}