Publications This page contains a chronological list of my peer-revied publications, as well as technical reports and theses. Papers are color-coded into several broad themes: * safe reinforcement learning via neuro-symbolic AI (see press coverage) * theorem proving for hybrid dynamical systems / cyber-physical systems (see press coverage) * modeling and verifying cyber-physical systems * programming languages for security * large language models Ben Athiwaratkun, Sanjay Krishna Gouda, Zijian Wang, Xiaopeng Li, Yuchen Tian, Ming Tan, Wasi Uddin Ahmad, Shiqi Wang, Qing Sun, Mingyue Shang, Sujan Kumar Gonugondla, Hantian Ding, Varun Kumar, Nathan Fulton, Arash Farahani, Siddhartha Jain, Robert Giaquinto, Haifeng Qian, Murali Krishna Ramanathan, Ramesh Nallapati, Baishakhi Ray, Parminder Bhatia, Sudipta Sengupta, Dan Roth, Bing Xiang. Multi-lingual evaluation of code generation models. In the 2023 Conference on Learning Representations (ICLR 2023), 2023.
[PDF](https://arxiv.org/pdf/2210.14868.pdf) | [HuggingFace](https://huggingface.co/datasets/mxeval/mbxp) [Jian Xiang](https://jianxiang.info/), Nathan Fulton, [Stephen Chong](https://people.seas.harvard.edu/~chong). Relational Analysis of Sensor Attacks on Cyber-Physical Systems. In Proceedings of the 34th IEEE Computer Security Foundations Symposium (CSF), June 2021.
[PDF](https://arxiv.org/pdf/2106.01850.pdf) | [bib](https://people.seas.harvard.edu/~chong/bib/XiangFC2021.bib) [Nathan Hunt](https://www.linkedin.com/in/neighthan), Nathan Fulton, [Sara Magliacane](https://mitibmwatsonailab.mit.edu/people/sara-magliacane/), [Nghia Hoang](https://sites.google.com/site/idmhtn/home), [Subhro Das](https://researcher.watson.ibm.com/researcher/view.php?person=ibm-Subhro.Das), [Armando Solar-Lezama](https://people.csail.mit.edu/asolar/). Verifiably Safe Exploration for End-to-End Reinforcement Learning. Proceedings of the 24th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2021). Online. May 19-21, 2021. (**Best Paper Award**)
[arxiv preprint](https://arxiv.org/pdf/2007.01223.pdf) | [VSRL framework](https://github.com/IBM/vsrl-framework) | [bib](/bib/vrsrl.bib) [Koundinya Vajjha](https://kodyvajjha.github.io/), [Avraham Shinnar](https://researcher.watson.ibm.com/researcher/view.php?person=us-shinnar), [Vasily Pestun](https://pestun.ihes.fr/), Barry Trager, Nathan Fulton. CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq. To be presented at The 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021). Online. January 18-19, 2021.
[PDF](https://arxiv.org/pdf/2009.11403.pdf) | [Coq Library](https://github.com/IBM/formalML/tree/converge) | [bib](/bib/certrl.bib) [presentation](https://youtu.be/VuWGyBmek70) May Wu, Nathan Fulton, Jessie Rosenberg. A Formally Verified Plasma Vertical Position Control Algorithm. In the 25th International Conference on Formal Methods for Industrial Critical Systems. Vienna, Austria, September 2-3, 2020.
[PDF](/papers/fmics.pdf) Viren Bajaj, Karim Elmaaroufi, Nathan Fulton, [André Platzer](http://symbolaris.com). Verifiably Safe SCUBA Diving with Commodity Sensors. WiP track at the ACM SIGBED International Conference on Embedded Software (EMSOFT'19), New York, NY, USA.
[PDF](https://dl.acm.org/doi/pdf/10.1145/3349568.3351554?download=true) | [github](https://github.com/nrfulton/scuba-release) Nathan Fulton, [Nathan Hunt](https://www.linkedin.com/in/neighthan), [Subhro Das](https://researcher.watson.ibm.com/researcher/view.php?person=ibm-Subhro.Das), [Nghia Hoang](https://sites.google.com/site/idmhtn/home). Formal Verification of End-to-End Learning in Cyber-Physical Systems: Progress and Challenges. NeurIPS-2019 Workshop on Safety and Robustness in Decision Making, Vancouver, BC, CA.
[PDF](https://arxiv.org/abs/2006.09181) | [canonical citation](/bib/vsrl.bib) Nathan Fulton and [André Platzer](http://symbolaris.com). Verifiably Safe Off-Model Reinforcement Learning. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19), Held as part of the European Joint Conferences on Theory and Practice of Software (ETAPS'19).
[PDF](/papers/vpmu.pdf) | [bib](/bib/vpmu.bib) Nathan Fulton and [André Platzer](http://symbolaris.com). Safe AI for CPS. International Test Conference, ITC'18. (**Invited paper**)
[PDF](http://symbolaris.com/pub/itc18.pdf) | [bib](/bib/itc.bib) Nathan Fulton and [André Platzer](http://symbolaris.com). Safe Reinforcement Learning via Formal Methods: Toward Safe Control Through Proof and Learning. Proceedings of the 32nd AAAI International Conference on Artificial Intelligence, AAAI'18, New Orleans, LA, USA. (**oral presentation**)
[PDF](/papers/aaai18.pdf) | [slides](/slides/AAAI.pdf) | [bib](/bib/aaai18.bib) Nathan Fulton, [Stefan Mitsch](http://www.cs.cmu.edu/~smitsch), Brandon Bohrer, [André Platzer](http://symbolaris.com). Bellerophon: Tactical Theorem Proving for Hybrid Systems. In Proceedings of the 8th International Conference on Interactive Theorem Proving, ITP'17, Brasília, Brazil.
[PDF](/papers/bellerophon.pdf) | [Slides](/slides/Bellerophon.pdf) | [Language Implementation](https://github.com/LS-Lab/KeYmaeraX-release/tree/master/keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/bellerophon) | [Standard Library Implementation](https://github.com/LS-Lab/KeYmaeraX-release/tree/master/keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/btactics) | [bib](https://dblp.org/rec/bibtex/conf/itp/FultonMBP17) Nathan Fulton, [André Platzer](http://symbolaris.com). **A Logic of Proofs for Differential Dynamic Logic: Toward Independently Checkable Proof Certificates for Dynamic Logics**. In Proceedings of The 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP'16, St. Petersburg, FL, USA.
[PDF](/papers/lpdl.pdf) | [Slides](http://nfulton.org/slides/cpp16.pdf) | [bib](https://dblp.org/rec/bibtex/conf/cpp/FultonP16) Nathan Fulton, [Stefan Mitsch](http://www.cs.cmu.edu/~smitsch/), [Jan-David Quesel](https://www.cs.cmu.edu/~jquesel/), [Marcus Völp](http://os.inf.tu-dresden.de/~voelp/), [André Platzer](http://symbolaris.com). **KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems**. In the International Conference on Automated Deduction, CADE'15, Berlin, DE.
[PDF](/papers/KeYmaeraX.pdf) | [Slides](/slides/keymaerax_slides.pdf) | [Poster](/posters/keymaerax_poster.pdf) | [Implementation](https://github.com/LS-Lab/KeYmaeraX-release) | [bib](https://dblp.org/rec/bibtex/conf/cade/FultonMQVP15) Nathan Fulton, [Cyrus Omar](http://www.cs.cmu.edu/~comar/), [Jonathan Aldrich](https://www.cs.cmu.edu/~./aldrich/). **Statically Typed String Sanitation Inside a Python**. PSP'14 Workshop, 2014, Portland, OR. [PDF](/papers/python.pdf) | [Poster](https://github.com/cyrus-/papers/blob/master/sanitation-psp14/poster/poster.pdf) | [Slides](/slides/strings.pdf) | [bib](https://dblp.org/rec/bibtex/conf/oopsla/FultonOA14) Nathan Fulton, [Cyrus Omar](http://www.cs.cmu.edu/~comar/), [Jonathan Aldrich](https://www.cs.cmu.edu/~./aldrich/). **Statically Typed String Sanitation Inside a Python**. CMU-ISR-14-112. In ISR Technical Reports 2014. Carnegie Mellon University (Technical Report).
[PDF](http://nfulton.org/papers/CMU-ISR-14-112.pdf) | [canonical citation](https://dblp.org/rec/bibtex/conf/oopsla/FultonOA14) Nathan Fulton. **Security Through Extensible Type Systems**. SPLASH'12 Student Research Competition (**Second Place**).
[PDF](/papers/src.pdf) | [canonical citation](https://dblp.org/rec/bibtex/conf/oopsla/FultonOA14) ## Theses Nathan Fulton. **Verifiably Safe Autonomy for Cyber-Physical Systems**. Computer Science Department, Carnegie Mellon University.
[PDF](http://reports-archive.adm.cs.cmu.edu/anon/2018/CMU-CS-18-125.pdf) Nathan Fulton. **A Typed Lambda Calculus for Input Sanitation**. In Selected Mathematics Senior Theses for the 2012-2013 Academic Year. Carthage College.
[PDF](https://dspace.carthage.edu/bitstream/handle/123456789/432/main.pdf?sequence=1&isAllowed=y) | [canonical citation](https://dblp.org/rec/bibtex/conf/oopsla/FultonOA14) ## Other Talks and Presentations I have given several talks and presentations that were not associated with a paper published in a formal proceedings. **Verifiably Safe Reinforcement Learning**. NASA JPL Autonomy Seminar Series. August 5, 2020. **A Formal Methods Perspective on Safe Reinforcement Learning** (Invited Talk). [Formal Methods for the Informal Engineer](https://fmie.github.io/). The Broad Institute of Harvard and MIT. Postponed due to COVID-19. **End-to-End Verification of Intelligent Cyber-Physical Systems: Progress and Challenges** (Invited Talk). Interactive Workshop on the Industrial Application of Verification and Testing. Prague, Czech Republic. 2019. Slides available on request. **Safe Reinforcement Learning**. Presented at SUNY-Stony Brook. 2018. **Safe Reinforcement Learning**. Presented at the Security seminar at Columbia University. New York City, New York, USA. 2018. **Safe Reinforcement Learning**. Presented at the 3rd Conference on Artificial Intelligence and Theorem Proving. Aussois, France. March 2018.
[Slides](https://nfulton.org/slides/AITP.pdf) | [canonical citation](/bib/aaai18.bib) **Marktoberdorf Tutorial on KeYmaera X**. Presented at Summer School Marktoberdorf 2017: Logical Methods for Safety and Security of Software Systems. Marktoberdorf, Garmany. August 2017.
[Slides](https://nfulton.org/slides/marktoberdorf.pdf) | [Other Resources](http://nfulton.org/2017/08/11/Marktoberdorf/) **Reachability Analysis in the KeYmaera X Theorem Prover**. Presented at the Third International Workshop on Symbolic and Numerical Methods. Uppsala, Sweden. April 2017.
[Slides](https://nfulton.org/slides/snr17.pdf) **Automatic Incremental Robustification for Hybrid Systems**. Presented at the Dagstuhl Seminar on Robustness for Cyber-Phyiscal Systems. Dagstuhl, Germany. September 2016.
[Slides](https://nfulton.org/slides/dagstuhl.pdf) ## Other In 2019 I helped organize the [Foundations of Safe Learning](https://workshop.safelearning.ai/) workshop @ IBM Research Week.