More Like this

1. Liquid proof macros

   https://doi.org/10.1145/3546189.3549921  

   Blanchette, Henry; Vazou, Niki; Lampropoulos, Leonidas (September 2022, International Symposium on Haskell)
2. Machine-Assisted Proof

   https://doi.org/10.1090/noti3041  

   Tao, Terence Chi-Shen (January 2025, Notices of the American Mathematical Society)
3. Propositional Proof Skeletons

   https://doi.org/10.1007/978-3-031-30823-9_17  

   Reeves, Joseph E.; Kiesl-Reiter, Benjamin; Heule, Marijn J. (April 2023, Springer)

   Sankaranarayanan, S.; Sharygina, N. (Ed.)

   Modern SAT solvers produce proofs of unsatisfiability to justify the correctness of their results. These proofs, which are usually represented in the well-known DRAT format, can often become huge, requiring multiple gigabytes of disk storage. We present a technique for semantic proof compression that selects a subset of important clauses from a proof and stores them as a so-called proof skeleton. This proof skeleton can later be used to efficiently reconstruct a full proof by exploiting parallelism. We implemented our approach on top of the award-winning SAT solver CaDiCaL and the proof checker DRAT-trim. In an experimental evaluation, we demonstrate that we can compress proofs into skeletons that are 100 to 5,000 times smaller than the original proofs. For almost all problems, proof reconstruction using a skeleton improves the solving time on a single core, and is around five times faster when using 24 cores. 

   more » « less
4. 2-hop Blockchain: Combining Proof-of-Work and Proof-of-Stake Securely

   https://doi.org/https://doi.org/10.1007/978-3-030-59013-0_34  

   Duong, T; Fan, L; Katz, J; Thai, P; Zhou, H-S. (September 2020, Lecture notes in computer science)

   null (Ed.)
5. Proof-Carrying Network Code

   https://doi.org/10.1145/3319535.3363214  

   Skalka, C; Ring, J; Darais, D; Kwon, M; Gupta, S; Diller, K; Smolka, S; and Foster, N (November 2019, Proceedings of the ACM Conference on Computer and Communications Security)

   Computer networks often serve as the first line of defense against malicious attacks. Although there are a growing number of software defined networking (SDN) tools for defining and enforcing security policies, most assume a single administrative domain and are unable to handle the challenges that arise in networks that could beneficially be programmed by multiple administrative domains. For example, consumers may want want to allow their home IoT networks to be configured by device vendors, which raises security and privacy concerns. In this paper we propose a framework called Proof Carrying Network Code (PCNC) for specifying and enforcing security in SDNs with interacting administrative domains. Like Proof Carrying Authorization (PCA), PCNC provides methods for authorization domains for network reprogramming, and like Proof Carrying Code (PCC), PCNC provides methods for enforcing desired behavior of network programs. We develop theoretical foundations for PCNC and evaluate it in simulated and real network settings, in a case study that considers security in IoT networks for at-home health monitoring. 

   more » « less