Zobrazeno 1 - 10
of 548
pro vyhledávání: '"PIERCE, BENJAMIN C."'
Suppose we are given two OCaml modules implementing the same signature. How do we check that they are observationally equivalent -- that is, that they behave the same on all inputs? One established technique is to use a property-based testing (PBT) t
Externí odkaz:
http://arxiv.org/abs/2408.14561
Autor:
Cutler, Joseph W., Watson, Christopher, Nkurumeh, Emeka, Hilliard, Phillip, Goldstein, Harrison, Stanford, Caleb, Pierce, Benjamin C.
We propose a rich foundational theory of typed data streams and stream transformers, motivated by two high-level goals: (1) The type of a stream should be able to express complex sequential patterns of events over time. And (2) it should describe the
Externí odkaz:
http://arxiv.org/abs/2307.09553
"A generator is a parser of randomness." This perspective on generators for random data structures is well established as folklore in the programming languages community, but it has apparently never been formalized, nor have its consequences been dee
Externí odkaz:
http://arxiv.org/abs/2203.00652
Autor:
Anderson, Sean Noble, Blanco, Roberto, Lampropoulos, Leonidas, Pierce, Benjamin C., Tolmach, Andrew
Publikováno v:
Proceedings of the 2023 IEEE 36th Computer Security Foundations Symposium (CSF)
The term stack safety is used to describe a variety of compiler, run-time, and hardware mechanisms for protecting stack memory. Unlike "the heap," the ISA-level stack does not correspond to a single high-level language concept: different compilers us
Externí odkaz:
http://arxiv.org/abs/2105.00417
Publikováno v:
Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2021). Association for Computing Machinery, New York, NY, USA, 529--539
We present a principled automatic testing framework for application-layer protocols. The key innovation is a domain-specific embedded language for writing nondeterministic models of the behavior of networked servers. These models are defined within t
Externí odkaz:
http://arxiv.org/abs/2102.00378
Applying differential privacy at scale requires convenient ways to check that programs computing with sensitive data appropriately preserve privacy. We propose here a fully automated framework for {\em testing} differential privacy, adapting a well-k
Externí odkaz:
http://arxiv.org/abs/2010.04126
Autor:
Xia, Li-yao, Zakowski, Yannick, He, Paul, Hur, Chung-Kil, Malecha, Gregory, Pierce, Benjamin C., Zdancewic, Steve
"Interaction trees" (ITrees) are a general-purpose data structure for representing the behaviors of recursive programs that interact with their environments. A coinductive variant of "free monads," ITrees are built out of uninterpreted events and the
Externí odkaz:
http://arxiv.org/abs/1906.00046
Curators of sensitive datasets sometimes need to know whether queries against the data are differentially private [Dwork et al. 2006]. Two sorts of logics have been proposed for checking this property: (1) type systems and other static analyses, whic
Externí odkaz:
http://arxiv.org/abs/1905.12594
Autor:
Koh, Nicolas, Li, Yao, Li, Yishuai, Xia, Li-yao, Beringer, Lennart, Honoré, Wolf, Mansky, William, Pierce, Benjamin C., Zdancewic, Steve
Publikováno v:
Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '19), January 14--15, 2019, Cascais, Portugal
We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChic
Externí odkaz:
http://arxiv.org/abs/1811.11911