Jan-Paul 😎

CORNELL

Evaluating Soundness of a Gradual Verifier with Property Based Testing

Jan-Paul Ramos-Dávila

In Cornell Undergraduate Research Journal, 2(1), 17–27, https://doi.org/10.37513/curj.v2i1.696.

TOPLAS

Gradual C0: Symbolic Execution for Gradual Verification

Jenna DiVincenzo, Ian McCormack, Hemant Gouni, Jacob Gorenburg, Jan-Paul Ramos-Dávila, Mona Zhang, Conrad Zimmerman, Joshua Sunshine, Éric Tanter, Jonathan Aldrich

In ACM Transactions on Programming Languages and Systems, 2024.

POPL

Gradual C0: Symbolic Execution for Gradual Verification

Jenna DiVincenzo, Ian McCormack, Hemant Gouni, Jacob Gorenburg, Jan-Paul Ramos-Dávila, Mona Zhang, Conrad Zimmerman, Joshua Sunshine, Éric Tanter, Jonathan Aldrich

In 52nd ACM SIGPLAN Symposium on Principles of Programming Languages, 2025.

CoqPL

Formal Verification of a Software Defined Delay-Tolerant Network

Jan-Paul Ramos-Dávila, Alwyn E. Goodloe

In The Eleventh International Workshop on Coq for Programming Languages, co-located with POPL, 2025, In Submission.

NASA / IEEE

Formal Verification of a Software Defined Delay-Tolerant Network

Jan-Paul Ramos-Dávila

In IEEE Workshop on Optimizing Interplanetary Communication Through Network Autonomy, 2024.

PriSC

Gradual Verification of Smart Contracts

Haojia Sun, Kunal Singh, Jan-Paul Ramos-Dávila, Jonathan Aldrich, Jenna Wise (DiVincenzo)

In Workshop on Principles of Secure Compilation, co-located with POPL, 2024.

POPL SRC

Optimization of a Gradual Verifier: Lazy evaluation of Iso-recursive Predicates as Equi-recursive at Runtime

Jan-Paul Ramos-Dávila

In ACM SIGPLAN Symposium on Principles of Programming Languages, 2024.

POPL SRC

Evaluating Soundness of a Gradual Verifier with Property Based Testing

Jan-Paul Ramos-Dávila

In ACM SIGPLAN Symposium on Principles of Programming Languages, 2023.

MWPLS

Optimization of a Gradual Verifier: Lazy evaluation of Iso-recursive Predicates as Equi-recursive at Runtime

Jan-Paul Ramos-Dávila

In Midwest Programming Languages Summit, 2023.

Jan-Paul Vincent Ramos-Dávila

Publications

Journals

Evaluating Soundness of a Gradual Verifier with Property Based Testing

Gradual C0: Symbolic Execution for Gradual Verification

Conferences

Gradual C0: Symbolic Execution for Gradual Verification

Workshops

Formal Verification of a Software Defined Delay-Tolerant Network

Formal Verification of a Software Defined Delay-Tolerant Network

Gradual Verification of Smart Contracts

Research Competitions

Optimization of a Gradual Verifier: Lazy evaluation of Iso-recursive Predicates as Equi-recursive at Runtime

Evaluating Soundness of a Gradual Verifier with Property Based Testing

Presentations

Optimization of a Gradual Verifier: Lazy evaluation of Iso-recursive Predicates as Equi-recursive at Runtime