Joseph Tassarotti

Proc. ACM Program. Lang., January, 2024

Tachis: Higher-Order Separation Logic with Credits for Expected Costs.

[BibT_eX]

[DOI]

Kwing Hei Li

Markus de Medeiros

Proc. ACM Program. Lang., 2024

Almost-Sure Termination by Guarded Refinement.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2024

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs.

[BibT_eX]

[DOI]

Markus de Medeiros

Kwing Hei Li

Proc. ACM Program. Lang., 2024

A Demonic Outcome Logic for Randomized Nondeterminism.

[BibT_eX]

[DOI]

CoRR, 2024

Approximate Relational Reasoning for Higher-Order Probabilistic Programs.

[BibT_eX]

[DOI]

Kwing Hei Li

CoRR, 2024

Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, 2024

2023

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic - Coq Artifact.

[BibT_eX]

[DOI]

Dataset, October, 2023

Verified Density Compilation for a Probabilistic Programming Language.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2023

Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2023

Grove: a Separation-Logic Library for Verifying Distributed Systems (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2023

Grove: a Separation-Logic Library for Verifying Distributed Systems.

[BibT_eX]

[DOI]

Proceedings of the 29th Symposium on Operating Systems Principles, 2023

Verifying vMVCC, a high-performance transaction library using multi-version concurrency control.

[BibT_eX]

[DOI]

Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation, 2023

The K2 Architecture for Trustworthy Hardware Security Modules.

[BibT_eX]

[DOI]

Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification, 2023

2022

Later credits: resourceful reasoning for the later modality.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2022

A separation logic for negative dependence.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2022

Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning.

[BibT_eX]

[DOI]

Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation, 2022

2021

Rabia: Simplifying State-Machine Replication Through Randomization.

[BibT_eX]

[DOI]

Proceedings of the SOSP '21: ACM SIGOPS 28th Symposium on Operating Systems Principles, 2021

Transfinite Iris: resolving an existential dilemma of step-indexed separation logic.

[BibT_eX]

[DOI]

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

GoJournal: a verified, concurrent, crash-safe journaling system.

[BibT_eX]

[DOI]

Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation, 2021

On Building Modular and Elastic Data Structures with Bulk Operations.

[BibT_eX]

[DOI]

Proceedings of the ICDCN '21: International Conference on Distributed Computing and Networking, 2021

A formal proof of PAC learnability for decision stumps.

[BibT_eX]

[DOI]

Koundinya Vajjha

Anindya Banerjee

Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

2020

Verification of ML Systems via Reparameterization.

[BibT_eX]

[DOI]

CoRR, 2020

2019

A separation logic for concurrent randomized programs.

[BibT_eX]

[DOI]

Robert Harper

Proc. ACM Program. Lang., 2019

A Formal Proof of PAC Learnability for Decision Stumps.

[BibT_eX]

[DOI]

Koundinya Vajjha

CoRR, 2019

Verifying concurrent, crash-safe systems with Perennial.

[BibT_eX]

[DOI]

Proceedings of the 27th ACM Symposium on Operating Systems Principles, 2019

Argosy: verifying layered storage systems with recovery refinement.

[BibT_eX]

[DOI]

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Scaling Hierarchical Coreference with Homomorphic Compression.

[BibT_eX]

[DOI]

Michael L. Wick

Swetasudha Panda

Proceedings of the 1st Conference on Automated Knowledge Base Construction, 2019

Sketching for Latent Dirichlet-Categorical Models.

[BibT_eX]

[DOI]

Michael L. Wick

Proceedings of the 22nd International Conference on Artificial Intelligence and Statistics, 2019

2018

MoSeL: a general, extensible modal framework for interactive proofs in separation logic.

[BibT_eX]

[DOI]

Robbert Krebbers

Jacques-Henri Jourdan

Proc. ACM Program. Lang., 2018

Verified Tail Bounds for Randomized Programs.

[BibT_eX]

[DOI]

Robert Harper

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

2017

Probabilistic Recurrence Relations for Work and Span of Parallel Algorithms.

[BibT_eX]

[DOI]

CoRR, 2017

A Higher-Order Logic for Concurrent Termination-Preserving Refinement.

[BibT_eX]

[DOI]

Ralf Jung

Robert Harper

Proceedings of the Programming Languages and Systems, 2017

2015

Verifying read-copy-update in a logic for weak memory.

[BibT_eX]

[DOI]

Derek Dreyer

Viktor Vafeiadis

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

Efficient Training of LDA on a GPU by Mean-for-Mode Estimation.

[BibT_eX]

[DOI]

Guy L. Steele Jr.

Proceedings of the 32nd International Conference on Machine Learning, 2015

2014

Augur: Data-Parallel Probabilistic Modeling.

[BibT_eX]

[DOI]

Proceedings of the Advances in Neural Information Processing Systems 27: Annual Conference on Neural Information Processing Systems 2014, 2014

2013

Augur: a Modeling Language for Data-Parallel Probabilistic Inference.

[BibT_eX]

[DOI]

CoRR, 2013

2012

RockSalt: better, faster, stronger SFI for the x86.

[BibT_eX]

[DOI]

Greg Morrisett

Gang Tan