• Åbogade 34, 5341, 119

    8200 Aarhus N

    Denmark

20062024

Research activity per year

Filter
Article in proceedings

Search results

  • 2024

    The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography

    Haselwarter, P. G., Hvass, B. S., Hansen, L. L., Winterhalter, T., Hriţcu, C. & Spitters, B., Jan 2024, CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs. Timany, A., Traytel, D., Pientka, B. & Blazy, S. (eds.). Association for Computing Machinery, p. 30-44 15 p.

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

    Open Access
  • 2023

    Faster constant-time evaluation of the Kronecker symbol with application to elliptic curve hashing

    Aranha, D. F., Hvass, B. S., Spitters, B. & Tibouchi, M., 15 Nov 2023, CCS'23: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security. New York: Association for Computing Machinery, p. 3228-3238 11 p.

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

    3 Citations (Scopus)
  • Formalising Decentralised Exchanges in Coq

    Nielsen, E. H., Annenkov, D. & Spitters, B., Jan 2023, CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. Krebbers, R., Traytel, D., Pientka, B. & Zdancewic, S. (eds.). New York: Association for Computing Machinery, p. 290-302 13 p.

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

    Open Access
    6 Citations (Scopus)
  • High-assurance field inversion for curve-based cryptography

    Hvass, B. S., Aranha, D. F. & Spitters, B., 2023, 2023 IEEE 36th Computer Security Foundations Symposium (CSF) . IEEE, p. 552-567 16 p. (Proceedings of the IEEE Computer Security Foundations Symposium).

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

    2 Citations (Scopus)
  • 2022

    Finding Smart Contract Vulnerabilities with ConCert's Property-Based Testing Framework

    Milo, M., Nielsen, E. H., Annenkov, D. & Spitters, B., Oct 2022, 4th International Workshop on Formal Methods for Blockchains (FMBC 2022). Dargaye, Z. & Schneidewind, C. (eds.). Dagstuhl Publishing, 13 p. (OpenAccess Series in Informatics, Vol. 105).

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

    Open Access
    1 Citation (Scopus)
  • 2021

    Extracting smart contracts tested and verified in Coq

    Annenkov, D., Milo, M., Nielsen, J. B. & Spitters, B., Jan 2021, CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021. Hritcu, C. & Popescu, A. (eds.). Association for Computing Machinery, p. 105-121 17 p.

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

    Open Access
    11 Citations (Scopus)
  • Formalizing Nakamoto-Style Proof of Stake

    Thomsen, S. E. & Spitters, B., 2021, Proceedings - 2021 IEEE 34th Computer Security Foundations Symposium, CSF 2021. IEEE, 15 p.

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

    15 Citations (Scopus)
  • Formal security analysis of MPC-in-the-head zero-knowledge protocols

    Sidorenco, N., Oechsner, S. & Spitters, B., 2021, Proceedings - 2021 IEEE 34th Computer Security Foundations Symposium, CSF 2021. IEEE, p. 607-620 14 p.

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

    11 Citations (Scopus)
  • SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

    Abate, C., Haselwarter, P. G., Rivas, E., Muylder, A. V., Winterhalter, T., Hriţcu, C., Maillard, K. & Spitters, B., 2021, Proceedings - 2021 IEEE 34th Computer Security Foundations Symposium, CSF 2021. IEEE, 15 p.

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

    17 Citations (Scopus)
  • 2020

    ConCert: A smart contract certification framework in Coq

    Annenkov, D., Botsch Nielsen, J. & Spitters, B., 2020, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’20), January 20-21, 2020, New Orleans, LA, USA. New York: Association for Computing Machinery, p. 215-228 14 p.

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

    Open Access
    31 Citations (Scopus)
  • Smart contract interactions in coq

    Nielsen, J. B. & Spitters, B., Jan 2020, Formal Methods- FM 2019 International Workshops - Revised Selected Papers. Sekerinski, E., Moreira, N., Oliveira, J. N., Ratiu, D., Guidotti, R., Farrell, M., Luckcuck, M., Marmsoler, D., Campos, J., Astarte, T., Gonnord, L., Cerone, A., Couto, L., Dongol, B., Kutrib, M., Monteiro, P. & Delmas, D. (eds.). Cham: Springer, p. 380-391 12 p. (Lecture Notes in Computer Science, Vol. 12232).

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

    Open Access
    7 Citations (Scopus)
  • 2018

    Computer-Aided Proofs for Multiparty Computation with Active Security

    Haagh, H., Karbyshev, A., Oechsner, S., Spitters, B. & Strub, P., 7 Aug 2018, Proceedings - IEEE 31st Computer Security Foundations Symposium, CSF 2018. Oxford: IEEE, Vol. 2018. p. 119-131 13 p. 8429300. (Proceedings of the IEEE Computer Security Foundations Symposium; No. 31).

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

    22 Citations (Scopus)
  • Preuves constructives de programmes probabilistes

    Translated title of the contribution: Constructive proofs of probabilistic programsFaissole, F. & Spitters, B., Jan 2018, Journées Francophones des Langages Applicatifs. (Journées Francophones des Langages Applicatifs (JFLA); No. 2018).

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  • 2017

    The HoTT Library: A Formalization of Homotopy Type Theory in Coq

    Bauer, A., Gross, J., Lumsdaine, P. L., Shulman, M., Sozeau, M. & Spitters, B., 16 Jan 2017, CPP 2017 - Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, co-located with POPL 2017: CPP 2017. Bertot, Y. & Vafeiadis, V. (eds.). New York, NY, USA: Association for Computing Machinery, p. 164-172 9 p.

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

    38 Citations (Scopus)
  • 2016

    Guarded Cubical Type Theory: Path Equality for Guarded Recursion

    Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H. B., Spitters, B. & Vezzosi, A., 2016, CSL 2016: 25th EACSL Annual Conference on Computer Science Logic. Talbot, J.-M. & Regnier, L. (eds.). p. 1 - 17 17 p. (Leibniz International Proceedings in Informatics, Vol. 62).

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

    Open Access
    File
    168 Downloads (Pure)
  • 2013

    The Picard algorithm for ordinary differential equations in Coq

    Makarov, E. & Spitters, B., 28 Aug 2013, Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings. p. 463-468 6 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 7998 LNCS).

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

    25 Citations (Scopus)
  • 2011

    Computer certified efficient exact reals in Coq

    Krebbers, R. & Spitters, B., 11 Aug 2011, Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011 and 10th International Conference, MKM 2011, Proceedings. p. 90-106 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 6824 LNAI).

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

    10 Citations (Scopus)