arXiv subjects

Qinshi Wang

Publications and source records attributed to Qinshi Wang.

4 recordsLinked to original sources

arXiv2024

Foundational Verification of Smart Contracts through Verified Compilation

Programs executed on a blockchain - smart contracts - have high financial stakes; their correctness is crucial. We argue, that this correctness needs to be foundational: correctness needs to be based on the operational semantics of their execution environment. In this work we present a foundational system - the DeepSEA system - targeting the Ethereum blockchain as the largest smart contract platform. The DeepSEA system has a small but sufficiently rich programming language amenable for verification, the DeepSEA language, and a verified DeepSEA compiler. Together they enable true end-to-end verification for smart contracts. We demonstrate usability through two case studies: a realistic contract for Decentralized Finance and contract for crowdfunding.

cs.PL↗

arXiv2023

VST-A: A Foundationally Sound Annotation Verifier

Program verifiers for imperative languages such as C may be annotation-based, in which assertions and invariants are put into source files and then checked, or tactic-based, where proof scripts separate from programs are interactively developed in a proof assistant such as Coq. Annotation verifiers have been more automated and convenient, but some interactive verifiers have richer assertion languages and formal proofs of soundness. We present VST-A, an annotation verifier that uses the rich assertion language of VST, leverages the formal soundness proof of VST, but allows users to describe functional correctness proofs intuitively by inserting assertions. VST-A analyzes control flow graphs, decomposes every C function into control flow paths between assertions, and reduces program verification problems into corresponding straightline Hoare triples. Compared to existing foundational program verification tools like VST and Iris, in VST-A, such decompositions and reductions are allowed to be nonstructural, which makes VST-A more flexible to use. VST-A's decomposition and reduction is defined in Coq, proved sound in Coq, and computed in a call-by-value way in Coq. The soundness proof for reduction is totally logical, independent of the complicated semantic model (and soundness proof) of VST's Hoare triple. Because of the rich assertion language, not all reduced proof goals can be automatically checked, but the system allows users to prove residual proof goals using the full power of the Coq proof assistant.

cs.PL↗

arXiv2021

Improving Regret Bounds for Combinatorial Semi-Bandits with Probabilistically Triggered Arms and Its Applications

We study combinatorial multi-armed bandit with probabilistically triggered arms (CMAB-T) and semi-bandit feedback. We resolve a serious issue in the prior CMAB-T studies where the regret bounds contain a possibly exponentially large factor of $1/p^*$, where $p^*$ is the minimum positive probability that an arm is triggered by any action. We address this issue by introducing a triggering probability modulated (TPM) bounded smoothness condition into the general CMAB-T framework, and show that many applications such as influence maximization bandit and combinatorial cascading bandit satisfy this TPM condition. As a result, we completely remove the factor of $1/p^*$ from the regret bounds, achieving significantly better regret bounds for influence maximization and cascading bandits than before. Finally, we provide lower bound results showing that the factor $1/p^*$ is unavoidable for general CMAB-T problems, suggesting that the TPM condition is crucial in removing this factor.

cs.LG↗

arXiv2016

Combinatorial Multi-Armed Bandit and Its Extension to Probabilistically Triggered Arms

We define a general framework for a large class of combinatorial multi-armed bandit (CMAB) problems, where subsets of base arms with unknown distributions form super arms. In each round, a super arm is played and the base arms contained in the super arm are played and their outcomes are observed. We further consider the extension in which more based arms could be probabilistically triggered based on the outcomes of already triggered arms. The reward of the super arm depends on the outcomes of all played arms, and it only needs to satisfy two mild assumptions, which allow a large class of nonlinear reward instances. We assume the availability of an offline (α,β)-approximation oracle that takes the means of the outcome distributions of arms and outputs a super arm that with probability β generates an α fraction of the optimal expected reward. The objective of an online learning algorithm for CMAB is to minimize (α,β)-approximation regret, which is the difference between the αβ fraction of the expected reward when always playing the optimal super arm, and the expected reward of playing super arms according to the algorithm. We provide CUCB algorithm that achieves O(log n) distribution-dependent regret, where n is the number of rounds played, and we further provide distribution-independent bounds for a large class of reward functions. Our regret analysis is tight in that it matches the bound of UCB1 algorithm (up to a constant factor) for the classical MAB problem, and it significantly improves the regret bound in a earlier paper on combinatorial bandits with linear rewards. We apply our CMAB framework to two new applications, probabilistic maximum coverage and social influence maximization, both having nonlinear reward structures. In particular, application to social influence maximization requires our extension on probabilistically triggered arms.

cs.LG↗