Next paper 08 September

data/desc.txt

@@ -1,3 +1,3 @@
-Mostly Automated Proof Repair for Verified Libraries
-Gopinathan, Kiran, et al. “Mostly Automated Proof Repair for Verified Libraries.” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, June 2023, pp. 25–49. Crossref, https://doi.org/10.1145/3591221.
-The cost of maintaining formally specified and verified software is widely considered prohibitively high due to the need to constantly keep code and the proofs of its correctness in sync—the problem known as proof repair . One of the main challenges in automated proof repair for evolving code is to infer invariants for a new version of a once verified program that are strong enough to establish its full functional correctness. In this work, we present the first proof repair methodology for higher-order imperative functions, whose initial versions were verified in the Coq proof assistant and whose specifications remained unchanged. Our proof repair procedure is based on the combination of dynamic program alignment, enumerative invariant synthesis, and a novel technique for efficiently pruning the space of invariant candidates, dubbed proof-driven testing , enabled by the constructive nature of Coq’s proof certificates. We have implemented our approach in a mostly-automated proof repair tool called Sisyphus. Given an OCaml function verified in Coq and its unverified new version, Sisyphus produces a Coq proof for the new version, discharging most of the new proof goals automatically and suggesting high-confidence obligations for the programmer to prove for the cases when automation fails. We have evaluated Sisyphus on 10 OCaml programs taken from popular libraries, that manipulate arrays and mutable data structures, considering their verified original and unverified evolved versions. Sisyphus has managed to repair proofs for all those functions, suggesting correct invariants and generating a small number of easy-to-prove residual obligations.
+Comparative Synthesis: Learning Near-Optimal Network Designs by Query
+Wang, Yanjun, et al. “Comparative Synthesis: Learning Near-Optimal Network Designs by Query.” Proceedings of the ACM on Programming Languages, vol. 7, no. POPL, Jan. 2023, pp. 91–120. Crossref, https://doi.org/10.1145/3571197.
+When managing wide-area networks, network architects must decide how to balance multiple conflicting metrics, and ensure fair allocations to competing traffic while prioritizing critical traffic. The state of practice poses challenges since architects must precisely encode their intent into formal optimization models using abstract notions such as utility functions, and ad-hoc manually tuned knobs. In this paper, we present the first effort to synthesize optimal network designs with indeterminate objectives using an interactive program-synthesis-based approach. We make three contributions. First, we present comparative synthesis, an interactive synthesis framework which produces near-optimal programs (network designs) through two kinds of queries (Validate and Compare), without an objective explicitly given. Second, we develop the first learning algorithm for comparative synthesis in which a voting-guided learner picks the most informative query in each iteration. We present theoretical analysis of the convergence rate of the algorithm. Third, we implemented Net10Q, a system based on our approach, and demonstrate its effectiveness on four real-world network case studies using black-box oracles and simulation experiments, as well as a pilot user study comprising network researchers and practitioners. Both theoretical and experimental results show the promise of our approach.

data/history.txt

@@ -10,4 +10,5 @@ https://doi.org/10.1145/3547652
 https://doi.org/10.1145/3314221.3314607
 https://doi.org/10.1145/3591264
 https://doi.org/10.1145/3563333
-https://doi.org/10.1145/3591221
+https://doi.org/10.1145/3591221
+https://doi.org/10.1145/3571197

data/next.txt

@@ -1 +1 @@
-https://doi.org/10.1145/3591221
+https://doi.org/10.1145/3571197

data/past.txt

@@ -2,4 +2,5 @@
 https://doi.org/10.1145/3314221.3314607
 https://doi.org/10.1145/3591264
 https://doi.org/10.1145/3563333
-https://doi.org/10.1145/3591221
+https://doi.org/10.1145/3591221
+https://doi.org/10.1145/3571197

docs/next.md

@@ -1 +1 @@
-Gopinathan, Kiran, et al. “Mostly Automated Proof Repair for Verified Libraries.” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, June 2023, pp. 25–49. Crossref, <a href='https://doi.org/10.1145/3591221' target='_blank'>https://doi.org/10.1145/3591221</a>.
+Wang, Yanjun, et al. “Comparative Synthesis: Learning Near-Optimal Network Designs by Query.” Proceedings of the ACM on Programming Languages, vol. 7, no. POPL, Jan. 2023, pp. 91–120. Crossref, <a href='https://doi.org/10.1145/3571197' target='_blank'>https://doi.org/10.1145/3571197</a>.

docs/papers.md

@@ -1,4 +1,5 @@
-1. Gopinathan, Kiran, et al. “Mostly Automated Proof Repair for Verified Libraries.” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, June 2023, pp. 25–49. Crossref, <a href='https://doi.org/10.1145/3591221' target='_blank'>https://doi.org/10.1145/3591221</a>.
-2. Sundararajah, Kirshanthan, et al. “UniRec: A Unimodular-like Framework for Nested Recursions and Loops.” Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA2, Oct. 2022, pp. 1264–90. Crossref, <a href='https://doi.org/10.1145/3563333' target='_blank'>https://doi.org/10.1145/3563333</a>.
-3. Zhang, Jialun, et al. “Interval Parsing Grammars for File Format Parsing.” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, June 2023, pp. 1073–95. Crossref, <a href='https://doi.org/10.1145/3591264' target='_blank'>https://doi.org/10.1145/3591264</a>.
-4. Liao, Kevin, et al. “ILC: A Calculus for Composable, Computational Cryptography.” Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2019. Crossref, <a href='https://doi.org/10.1145/3314221.3314607' target='_blank'>https://doi.org/10.1145/3314221.3314607</a>.
+1. Wang, Yanjun, et al. “Comparative Synthesis: Learning Near-Optimal Network Designs by Query.” Proceedings of the ACM on Programming Languages, vol. 7, no. POPL, Jan. 2023, pp. 91–120. Crossref, <a href='https://doi.org/10.1145/3571197' target='_blank'>https://doi.org/10.1145/3571197</a>.
+2. Gopinathan, Kiran, et al. “Mostly Automated Proof Repair for Verified Libraries.” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, June 2023, pp. 25–49. Crossref, <a href='https://doi.org/10.1145/3591221' target='_blank'>https://doi.org/10.1145/3591221</a>.
+3. Sundararajah, Kirshanthan, et al. “UniRec: A Unimodular-like Framework for Nested Recursions and Loops.” Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA2, Oct. 2022, pp. 1264–90. Crossref, <a href='https://doi.org/10.1145/3563333' target='_blank'>https://doi.org/10.1145/3563333</a>.
+4. Zhang, Jialun, et al. “Interval Parsing Grammars for File Format Parsing.” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, June 2023, pp. 1073–95. Crossref, <a href='https://doi.org/10.1145/3591264' target='_blank'>https://doi.org/10.1145/3591264</a>.
+5. Liao, Kevin, et al. “ILC: A Calculus for Composable, Computational Cryptography.” Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2019. Crossref, <a href='https://doi.org/10.1145/3314221.3314607' target='_blank'>https://doi.org/10.1145/3314221.3314607</a>.