Zobrazeno 1 - 10
of 144
pro vyhledávání: '"SPITTERS, BAS"'
Publikováno v:
FMBC: Formal Methods for Blockchains, 2022
We provide three detailed case studies of vulnerabilities in smart contracts, and show how property-based testing would have found them: 1. the Dexter1 token exchange; 2. the iToken; 3. the ICO of Brave's BAT token. The last example is, in fact, new,
Externí odkaz:
http://arxiv.org/abs/2208.00758
The number of attacks and accidents leading to significant losses of crypto-assets is growing. According to Chainalysis, in 2021, approx. $14 billion has been lost due to various incidents, and this number is dominated by Decentralized Finance (DeFi)
Externí odkaz:
http://arxiv.org/abs/2203.08016
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. We extend the MetaCoq erasure output language with typing information and use it as an intermediate representation, which we call $\lambda^T_\square
Externí odkaz:
http://arxiv.org/abs/2108.02995
Publikováno v:
CPP'2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, January 18--19, 2021, Virtual, Denmark
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operationa
Externí odkaz:
http://arxiv.org/abs/2012.09138
Autor:
Thomsen, Søren Eller, Spitters, Bas
Publikováno v:
2021 IEEE 34th Computer Security Foundations Symposium (CSF), Pages: 1-15
Fault-tolerant distributed systems move the trust in a single party to a majority of parties participating in the protocol. This makes blockchain based crypto-currencies possible: they allow parties to agree on a total order of transactions without a
Externí odkaz:
http://arxiv.org/abs/2007.12105
Publikováno v:
Mathematical Structures in Computer Science, 1-29, 2021
The ALEA Coq library formalizes measure theory based on a variant of the Giry monad on the category of sets. This enables the interpretation of a probabilistic programming language with primitives for sampling from discrete distributions. However, co
Externí odkaz:
http://arxiv.org/abs/1912.07339
Autor:
Nielsen, Jakob Botsch, Spitters, Bas
Publikováno v:
1st Workshop on Formal Methods for Blockchains, 3rd Formal Methods World Congress on October 11, 2019 in Porto, Portugal
We present a model/executable specification of smart contract execution in Coq. Our formalization allows for inter-contract communication and generalizes existing work by allowing modelling of both depth-first execution blockchains (like Ethereum) an
Externí odkaz:
http://arxiv.org/abs/1911.04732
Publikováno v:
CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, January 2020, Pages 215-228
We present a new way of embedding functional languages into the Coq proof assistant by using meta-programming. This allows us to develop the meta-theory of the language using the deep embedding and provides a convenient way for reasoning about concre
Externí odkaz:
http://arxiv.org/abs/1907.10674
Autor:
Sterling, Jonathan, Spitters, Bas
The connection between normalization by evaluation, logical predicates and semantic gluing constructions is a matter of folklore, worked out in varying degrees within the literature. In this note, we present an elementary version of the gluing techni
Externí odkaz:
http://arxiv.org/abs/1809.08646
Publikováno v:
Foundations of Probabilistic Programming, ed. Gilles Barthe, Joost-Pieter Katoen & Alexandra Silva, Cambridge University Press, 2020
In this chapter, we explore how (Type-2) computable distributions can be used to give both (algorithmic) sampling and distributional semantics to probabilistic programs with continuous distributions. Towards this end, we sketch an encoding of computa
Externí odkaz:
http://arxiv.org/abs/1806.07966