Search results

  • 2023

    Baldur: Whole-Proof Generation and Repair with Large Language Models

    First, E., Rabe, M., Ringer, T. & Brun, Y., Nov 30 2023, ESEC/FSE 2023 - Proceedings of the 31st ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering. Chandra, S., Blincoe, K. & Tonella, P. (eds.). Association for Computing Machinery, p. 1229-1241 13 p. (ESEC/FSE 2023 - Proceedings of the 31st ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
  • Long-Term Mentoring for Computer Science Researchers

    Ringer, T., Ruppel, E., Liu, S., Garza, E., Ryu, S. & Silva, A., Apr 21 2023, In: Communications of the ACM. 66, 5, p. 33-35 3 p.

    Research output: Contribution to journalArticlepeer-review

    Open Access
  • Passport: Improving Automated Formal Verification Using Identifiers

    Sanchez-Stern, A., First, E., Zhou, T., Kaufman, Z., Brun, Y. & Ringer, T., Jun 26 2023, In: ACM Transactions on Programming Languages and Systems. 45, 2, 12.

    Research output: Contribution to journalArticlepeer-review

    Open Access
  • Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset

    Reichel, T., Wesley Henderson, R., Touchet, A., Gardner, A. & Ringer, T., Jul 2023, 14th International Conference on Interactive Theorem Proving, ITP 2023. Naumowicz, A. & Thiemann, R. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 26. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 268).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • PRoofster: Automated Formal Verification

    Agrawal, A., First, E., Kaufman, Z., Reichel, T., Zhang, S., Zhou, T., Sanchez-Stern, A., Ringer, T. & Brun, Y., 2023, Proceedings - 2023 IEEE/ACM 45th International Conference on Software Engineering: Companion, ICSE-Companion 2023. IEEE Computer Society, p. 26-30 5 p. (Proceedings - International Conference on Software Engineering).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2021

    Proof repair across type equivalences

    Ringer, T., Porter, R. D., Yazdani, N., Leo, J. & Grossman, D., Jun 18 2021, PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Freund, S. N. & Yahav, E. (eds.). Association for Computing Machinery, p. 112-127 16 p. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2020

    REPLica: REPL instrumentation for Coq analysis

    Ringer, T., Sanchez-Stern, A., Grossman, D. & Lerner, S., Jan 20 2020, CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020. Blanchette, J. & Hritcu, C. (eds.). Association for Computing Machinery, p. 99-113 15 p. (CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
  • 2019

    Ornaments for proof reuse in Coq

    Ringer, T., Yazdani, N., Leo, J. & Grossman, D., Sep 2019, 10th International Conference on Interactive Theorem Proving, ITP 2019. Harrison, J., O'Leary, J. & Tolmach, A. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 26. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 141).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • QED at large: A survey of engineering of formally verified software

    Ringer, T., Palmskog, K., Sergey, I., Gligoric, M. & Tatlock, Z., Sep 3 2019, In: Foundations and Trends in Programming Languages. 5, 2-3, p. 102-281 180 p.

    Research output: Contribution to journalArticlepeer-review

    Open Access
  • 2018

    Adapting proof automation to adapt proofs

    Ringer, T., Leo, J., Yazdani, N. & Grossman, D., Jan 8 2018, CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018. Felty, A. & Andronick, J. (eds.). Association for Computing Machinery, p. 115-129 15 p. (CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018; vol. 2018-January).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2017

    A Solver-Aided Language for Test Input Generation

    Ringer, T., Grossman, D., Schwartz-Narbonne, D. & Tasiran, S., Oct 1 2017, In: Proceedings of the ACM on Programming Languages. 1, OOPSLA, p. 1-24 91.

    Research output: Contribution to journalConference articlepeer-review

    Open Access
  • 2016

    AUDACIOUS: User-driven access control with unmodified operating systems

    Ringer, T., Grossman, D. & Roesner, F., Oct 24 2016, CCS 2016 - Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, p. 204-216 13 p. (Proceedings of the ACM Conference on Computer and Communications Security; vol. 24-28-October-2016).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution