Conference Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols 2025 • Proceedings of the 19th Usenix Symposium on Operating Systems Design and Implementation Osdi 2025 • 1-17 Zhang TN, Singh K, Chajed T, Kapritsos M, Parno B
Chapter Cazamariposas: Automated Instability Debugging in SMT-Based Program Verification 2025 • Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) • 15943:75-94 Zhou Y, Shah A, Lin Z, Heule M, Parno B
Conference Instability Track for SMT-COMP 2025 • CEUR Workshop Proceedings • 4008:148-152 Shah A, Zhou Y, Heule M, Parno B
Chapter A Framework for Debugging Automated Program Verification Proofs via Proof Actions 2024 • Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) • 14681:348-361 Cho C, Zhou Y, Bosamiya J, Parno B
Conference Context Pruning for More Robust SMT-based Program Verification 2024 Zhou Y, Bosamiya J, Li J, Heule M, Parno B
Journal Article FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional Permissions 2024 • Proceedings of the ACM on Programming Languages • 8(OOPSLA): Lin Z, Gancher J, Parno B
Conference Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs 2024 • PROCEEDINGS OF THE 18TH USENIX SYMPOSIUM ON OPERATING SYSTEMS DESIGN AND IMPLEMENTATION, OSDI 2024 • 837-853 Zhang TN, Hance T, Kapritsos M, Chajed T, Parno B
Conference Verus: A Practical Foundation for Systems Verification 2024 • PROCEEDINGS OF THE 2024 ACM SIGOPS 30TH SYMPOSIUM ON OPERATING SYSTEMS PRINCIPLES, SOSP 2024 • 438-454 Lattuada A, Hance T, Bosamiya J, Brun M, Cho C, LeBlanc H, Srinivasan P, Achermann R, Chajed T, Hawblitzel C, Howell J, Lorch JR, Padon O, Parno B
Conference Algebraic Reductions of Knowledge 2023 • Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) • 14084:669-701 Kothapalli A, Parno B
Conference FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores 2023 30-46 Arasu A, Ramananandro T, Rastogi A, Swamy N, Fromherz A, Hietala K, Parno B, Ramamurthy R
Conference Galapagos: Developing Verified Low-Level Cryptography on Heterogeneous Hardware 2023 • PROCEEDINGS OF THE 2023 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY, CCS 2023 • 2113-2127 Zhou Y, Gibson S, Cai S, Winchell M, Parno B
Journal Article Leaf: Modularity for Temporary Sharing in Separation Logic 2023 • Proceedings of the ACM on Programming Languages • 7(OOPSLA): Hance T, Howell J, Padon O, Parno B
Preprint Leaf: Modularity for Temporary Sharing in Separation Logic (Extended Version) 2023 Hance T, Howell J, Padon O, Parno B
Conference Mariposa: Measuring SMT Instability in Automated Program Verification 2023 • 2023 FORMAL METHODS IN COMPUTER-AIDED DESIGN, FMCAD • 178-188 Zhou Y, Bosamiya J, Takashima Y, Li J, Heule M, Parno B
Journal Article MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code 2023 • Proceedings of the ACM on Programming Languages • 7(POPL): Michael AE, Gollamudi A, Bosamiya J, Johnson E, Denlinger A, Disselkoen C, Watt C, Parno B, Patrignani M, Vassena M, Stefan D
Conference No Root Store Left Behind 2023 • PROCEEDINGS OF THE 22ND ACM WORKSHOP ON HOT TOPICS IN NETWORKS, HOTNETS 2023 • 295-301 Larisch J, Aqeel W, Chung T, Kohler E, Levin D, Maggs BM, Parno B, Wilson C
Conference Owl: Compositional Verification of Security Protocols via an Information-Flow Type System 2023 • IEEE Symposium on Security and Privacy: Proceedings • 00:1130-1147 Gancher J, Gibson S, Singh P, Dharanikota S, Parno B
Conference Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems 2023 • PROCEEDINGS OF THE 17TH USENIX SYMPOSIUM ON OPERATING SYSTEMS DESIGN AND IMPLEMENTATION, OSDI 2023 • 911-929 Hance T, Zhou Y, Lattuada A, Achermann R, Conway A, Stutsman R, Zellweger G, Hawblitzel C, Howell J, Parno B
Journal Article Verus: Verifying Rust Programs using Linear Ghost Types 2023 • Proceedings of the ACM on Programming Languages • 7(OOPSLA): Lattuada A, Hance T, Cho C, Brun M, Subasinghe I, Zhou Y, Howell J, Parno B, Hawblitzel C
Preprint Verus: Verifying Rust Programs using Linear Ghost Types (extended version) 2023 Lattuada A, Hance T, Cho C, Brun M, Subasinghe I, Zhou Y, Howell J, Parno B, Hawblitzel C
Preprint WaveCert: Translation Validation for Asynchronous Dataflow Programs via Dynamic Fractional Permissions 2023 Lin Z, Gancher J, Parno B
Journal Article Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility 2022 • ACM Transactions on Programming Languages and Systems • 44(2): Lorch JR, Chen Y, Kapritsos M, Ma H, Parno B, Qadeer S, Sharma U, Wilcox JR, Zhao X
Journal Article Degradation Attacks on Certifiably Robust Neural Networks 2022 • Transactions on Machine Learning Research • 1(1): Leino K, Zhang C, Mangal R, Fredrikson M, Parno B, Pasareanu C
Conference Hammurabi 2022 • Proceedings of the ACM Conference on Computer and Communications Security • 1857-1870 Larisch J, Aqeel W, Lum M, Goldschlag Y, Kannan L, Torshizi K, Wang Y, Chung T, Levin D, Maggs BM, Mislove A, Parno B, Wilson C
Journal Article Linear Types for Large-Scale Systems Verification 2022 • Proceedings of the ACM on Programming Languages • 6(OOPSLA): Li J, Lattuada A, Zhou Y, Cameron J, Howell J, Parno B, Hawblitzel C
