Update README.md

Author: rodrigo7491

README.md

@@ -40,6 +40,10 @@ The framework is currently capable of validating models produced for LIA instanc
 
 A large part of the [SMT instance generator] was implemented by Fedor Gromov.
 
+## Publication
+
+To know more about the theory behind ATHENA, as well as its applications, have a look at our [iFM23 paper].
+
 [Eldarica]: https://github.com/uuverifiers/eldarica
 [Golem]: https://github.com/usi-verification-and-security/golem
 [Spacer]: https://github.com/Z3Prover/z3
@@ -66,4 +70,5 @@ A large part of the [SMT instance generator] was implemented by Fedor Gromov.
 [LFSC checker 9aab068]: https://github.com/cvc5/LFSC/commit/9aab068dec2c5a9f5f2bf465590005c638078e95
 [latest version of TSWC]: https://verify.inf.usi.ch/certificate-producing-opensmt2
 [SMT instance generator]: https://github.com/usi-verification-and-security/chc-model-validator/blob/master/scripts/generate_chc_witness_checks.py
-[CHC-COMP formatter]: https://github.com/chc-comp/scripts/tree/master/format
+[CHC-COMP formatter]: https://github.com/chc-comp/scripts/tree/master/format
+[iFM23 paper]: https://doi.org/10.1007/978-3-031-47705-8_4