Quelle  root.bib

% Encoding: UTF-8
@InProceedings{   Hodovan2018,
  author = {Hodov\'{a}n, Ren\'{a}ta and Kiss, \'{A}kos and Gyim\'{o}thy, Tibor},
  booktitle = {Proceedings of the 9th ACM SIGSOFT International Workshop on Automating TEST Case Design, Selection,
    and Evaluation},
  title  = {{Grammarinator: A Grammar-Based Open Source Fuzzer}},
  year  = 2018,
  address = {New York, NY, USA},
  pages  = {45{\^a}€“48},
  publisher = {Association for Computing Machinery},
  series = {A-TEST 2018},
  abstract = {Fuzzing, or random testing, is an increasingly popular testing technique. The power of the approach
    lies in its ability to generate a large number of useful test cases without consuming expensive
    manpower. Furthermore, because of the randomness, it can often produce unusual cases that would be
    beyond the awareness of a human tester. In this paper, we present Grammarinator, a general purpose
    test generator tool that is able to utilize existing parser grammars as models. Since the model can
    act both as a parser and as a generator, the tool can provide the capabilities of both generation and
    mutation-based fuzzers. The presented tool is actively used to test various JavaScript engines and has
    found more than 100 unique issues.},
  doi  = {10.1145/3278186.3278193},
  isbn  = 9781450360531,
  keywords = {grammars, security, random testing, fuzzing},
  location = {Lake Buena Vista, FL, USA},
  numpages = 4,
  url  = {https://doi.org/10.1145/3278186.3278193}
}

@Misc{    Parr,
  author = {Terence Parr},
  howpublished = {\url{https://www.antlr.org/index.html}},
  note  = {{Accessed: 2021-05-01}},
  title  = {ANTLR (ANother Tool for Language Recognition)}
}

@Misc{    truffle,
  author = {{ConsenSys Software Inc.}},
  howpublished = {\url{https://www.trufflesuite.com/truffle}},
  note  = {{Accessed: 2021-05-01}},
  title  = {Truffle}
}

@Misc{    ganache,
  author = {{ConsenSys Software Inc.}},
  howpublished = {\url{https://www.trufflesuite.com/docs/ganache/}},
  note  = {{Accessed: 2021-05-01}},
  title  = {Ganache}
}

@Book{    Scott1971,
  author = {Scott, Dana and Strachey, Christopher},
  publisher = {Oxford University Computing Laboratory, Programming Research Group Oxford},
  title  = {Toward a mathematical semantics for computer languages},
  year  = 1971,
  volume = 1
}

@Book{    Scott1970,
  author = {Scott, Dana},
  publisher = {Oxford University Computing Laboratory, Programming Research Group Oxford},
  title  = {Outline of a mathematical theory of computation},
  year  = 1970
}

@InProceedings{   Bertoni2013,
  author = {Bertoni, Guido and Daemen, Joan and Peeters, Micha{\"e}l and Van Assche, Gilles},
  booktitle = {Advances in Cryptology -- EUROCRYPT 2013},
  title  = {Keccak},
  year  = 2013,
  address = {Berlin, Heidelberg},
  editor = {Johansson, Thomas and Nguyen, Phong Q.},
  pages  = {313--314},
  publisher = {Springer Berlin Heidelberg},
  abstract = {In October 2012, the American National Institute of Standards and Technology (NIST) announced the
    selection of Keccak as the winner of the SHA-3 Cryptographic Hash Algorithm Competition [10,11]. This
    concluded an open competition that was remarkable both for its magnitude and the involvement of the
    cryptographic community. Public review is of paramount importance to increase the confidence in the
    new standard and to favor its quick adoption. The SHA-3 competition explicitly took this into account
    by giving open access to the candidate algorithms and everyone in the cryptographic community could
    try to break them, compare their performance, or simply give comments.},
  isbn  = {978-3-642-38348-9}
}

@InProceedings{   Hildenbrandt2018,
  author = {Hildenbrandt, Everett and Saxena, Manasvi and Rodrigues, Nishant and Zhu, Xiaoran and Daian, Philip
    and Guth, Dwight and Moore, Brandon and Park, Daejun and Zhang, Yi and Stefanescu, Andrei and Rosu,
    Grigore},
  booktitle = {2018 IEEE 31st Computer Security Foundations Symposium (CSF)},
  title  = {KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine},
  year  = 2018,
  pages  = {204--217},
  doi  = {10.1109/CSF.2018.00022}
}

@Article{   Rosu2010,
  author = {Grigore Ro{\`E}™u and Traian Florin {\`E}˜erb{\"A}ƒnut{\"A}ƒ},
  journal = {The Journal of Logic and Algebraic Programming},
  title  = {An overview of the K semantic framework},
  year  = 2010,
  issn  = {1567-8326},
  note  = {Membrane computing and programming},
  number = 6,
  pages  = {397--434},
  volume = 79,
  abstract = {K is an executable semantic framework in which programming languages, calculi, as well as type
    systems or formal analysis tools can be defined, making use of configurations, computations and rules.
    Configurations organize the system/program state in units called cells, which are labeled and can be
    nested. Computations carry {\^a}€œcomputational meaning{\^a}€ as special nested list structures
    sequentializing computational tasks, such as fragments of program; in particular, computations extend
    the original language or calculus syntax. K (rewrite) rules generalize conventional rewrite rules by
    making explicit which parts of the term they read, write, or do not care about. This distinction makes
    K a suitable framework for defining truly concurrent languages or calculi, even in the presence of
    sharing. Since computations can be handled like any other terms in a rewriting environment, that is,
    they can be matched, moved from one place to another in the original term, modified, or even deleted,
    K is particularly suitable for defining control-intensive language features such as abrupt
    termination, exceptions, or call/cc. This paper gives an overview of the K framework: what it is, how
    it can be used, and where it has been used so far. It also proposes and discusses the K definition of
    Challenge, a programming language that aims to challenge and expose the limitations of existing
    semantic frameworks.},
  doi  = {https://doi.org/10.1016/j.jlap.2010.03.012},
  url  = {https://www.sciencedirect.com/science/article/pii/S1567832610000160}
}

@InProceedings{   Hirai2017,
  author = {Hirai, Yoichi},
  booktitle = {Financial Cryptography and Data Security},
  title  = {Defining the Ethereum Virtual Machine for Interactive Theorem Provers},
  year  = 2017,
  address = {Cham},
  editor = {Brenner, Michael and Rohloff, Kurt and Bonneau, Joseph and Miller, Andrew and Ryan, Peter Y.A. and
    Teague, Vanessa and Bracciali, Andrea and Sala, Massimiliano and Pintore, Federico and Jakobsson,
    Markus},
  pages  = {520--535},
  publisher = {Springer International Publishing},
  abstract = {Smart contracts in Ethereum are executed by the Ethereum Virtual Machine (EVM). We defined EVM in
    Lem, a language that can be compiled for a few interactive theorem provers. We tested our definition
    against a standard test suite for Ethereum implementations. Using our definition, we proved some
    safety properties of Ethereum smart contracts in an interactive theorem prover Isabelle/HOL. To our
    knowledge, ours is the first formal EVM definition for smart contract verification that implements all
    instructions. Our definition can serve as a basis for further analysis and generation of Ethereum
    smart contracts.},
  isbn  = {978-3-319-70278-0}
}

@Book{    Nipkow2002,
  author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  publisher = {Springer},
  title  = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  year  = 2002,
  series = {LNCS},
  volume = 2283
}

@InProceedings{   perez.ea:smart:2021,
  author = {Daniel Perez and Ben Livshits},
  title  = {Smart Contract Vulnerabilities: Vulnerable Does Not Imply Exploited},
  booktitle = {30th {USENIX} Security Symposium ({USENIX} Security 21)},
  year  = 2021,
  url  = {https://www.usenix.org/conference/usenixsecurity21/presentation/perez},
  publisher = {{USENIX} Association},
  month  = aug
}

@Article{   Yang2020,
  author = {Yang, Zheng and Lei, Hang},
  journal = {Mathematical Problems in Engineering},
  title  = {Lolisa: Formal Syntax and Semantics for a Subset of the Solidity Programming Language in Mathematical
    Tool Coq},
  year  = 2020,
  issn  = {1024-123X},
  pages  = 6191537,
  volume = 2020,
  abstract = {The security of blockchain smart contracts is one of the most emerging issues of the greatest
    interest for researchers. This article presents an intermediate specification language for the formal
    verification of Ethereum-based smart contract in Coq, denoted as Lolisa. The formal syntax and
    semantics of Lolisa contain a large subset of the Solidity programming language developed for the
    Ethereum blockchain platform. To enhance type safety, the formal syntax of Lolisa adopts a stronger
    static type system than Solidity. In addition, Lolisa includes a large subset of Solidity syntax
    components as well as general-purpose programming language features. Therefore, Solidity programs can
    be directly translated into Lolisa with line-by-line correspondence. Lolisa is inherently
    generalizable and can be extended to express other programming languages. Finally, the syntax and
    semantics of Lolisa have been encapsulated as an interpreter in mathematical tool Coq. Hence, smart
    contracts written in Lolisa can be symbolically executed and verified in Coq.},
  publisher = {Hindawi},
  url  = {https://doi.org/10.1155/2020/6191537}
}

@Manual{   Coq,
  title  = {The Coq proof assistant reference manual},
  author = {The Coq development team},
  note  = {Version 8.0},
  organization = {LogiCal Project},
  year  = 2004,
  url  = {http://coq.inria.fr}
}

@InProceedings{   Crosara2019,
  author = {Marco Crosara and Gabriele Centurino and Vincenzo Arceri},
  booktitle = {Proceedings of The Eleventh International Conference on Advances in System Testing and Validation
    Lifecycle (VALID)},
  title  = {{Towards an Operational Semantics for Solidity}},
  year  = 2019,
  editor = {Jos van Rooyen and Samuele Buro and Marco Campion and Michele Pasqua},
  month  = nov,
  pages  = {1--6},
  publisher = {IARIA}
}

@InProceedings{   Jiao2020,
  author = {Jiao, Jiao and Kan, Shuanglong and Lin, Shang-Wei and Sanan, David and Liu, Yang and Sun, Jun},
  booktitle = {2020 IEEE Symposium on Security and Privacy (SP)},
  title  = {Semantic understanding of smart contracts: executable operational semantics of Solidity},
  year  = 2020,
  organization = {IEEE},
  pages  = {1695--1712}
}

@InProceedings{   Jiao2020a,
  author = {Jiao, Jiao and Lin, Shang-Wei and Sun, Jun},
  booktitle = {Fundamental Approaches to Software Engineering},
  title  = {A Generalized Formal Semantic Framework for Smart Contracts},
  year  = 2020,
  address = {Cham},
  editor = {Wehrheim, Heike and Cabot, Jordi},
  pages  = {75--96},
  publisher = {Springer International Publishing},
  abstract = {Smart contracts can be regarded as one of the most popular blockchain-based applications. The
    decentralized nature of the blockchain introduces vulnerabilities absent in other programs.
    Furthermore, it is very difficult, if not impossible, to patch a smart contract after it has been
    deployed. Therefore, smart contracts must be formally verified before they are deployed on the
    blockchain to avoid attacks exploiting these vulnerabilities. There is a recent surge of interest in
    analyzing and verifying smart contracts. While most of the existing works either focus on EVM bytecode
    or translate Solidity contracts into programs in intermediate languages for analysis and verification,
    we believe that a direct executable formal semantics of the high-level programming language of smart
    contracts is necessary to guarantee the validity of the verification. In this work, we propose a
    generalized formal semantic framework based on a general semantic model of smart contracts.
    Furthermore, this framework can directly handle smart contracts written in different high-level
    programming languages through semantic extensions and facilitates the formal verification of security
    properties with the generated semantics.},
  isbn  = {978-3-030-45234-6}
}

@InProceedings{   Mavridou2019,
  author = {Mavridou, Anastasia and Laszka, Aron and Stachtiari, Emmanouela and Dubey, Abhishek},
  booktitle = {Financial Cryptography and Data Security},
  title  = {VeriSolid: Correct-by-Design Smart Contracts for Ethereum},
  year  = 2019,
  address = {Cham},
  editor = {Goldberg, Ian and Moore, Tyler},
  pages  = {446--465},
  publisher = {Springer International Publishing},
  abstract = {The adoption of blockchain based distributed ledgers is growing fast due to their ability to provide
    reliability, integrity, and auditability without trusted entities. One of the key capabilities of
    these emerging platforms is the ability to create self-enforcing smart contracts. However, the
    development of smart contracts has proven to be error-prone in practice, and as a result, contracts
    deployed on public platforms are often riddled with security vulnerabilities. This issue is
    exacerbated by the design of these platforms, which forbids updating contract code and rolling back
    malicious transactions. In light of this, it is crucial to ensure that a smart contract is secure
    before deploying it and trusting it with significant amounts of cryptocurrency. To this end, we
    introduce the VeriSolid framework for the formal verification of contracts that are specified using a
    transition-system based model with rigorous operational semantics. Our model-based approach allows
    developers to reason about and verify contract behavior at a high level of abstraction. VeriSolid
    allows the generation of Solidity code from the verified models, which enables the correct-by-design
    development of smart{\^A} contracts.},
  isbn  = {978-3-030-32101-7}
}

@InProceedings{   Mavridou2018,
  author = {Mavridou, Anastasia and Laszka, Aron},
  booktitle = {Principles of Security and Trust},
  title  = {Tool Demonstration: FSolidM for Designing Secure Ethereum Smart Contracts},
  year  = 2018,
  address = {Cham},
  editor = {Bauer, Lujo and K{\"u}sters, Ralf},
  pages  = {270--277},
  publisher = {Springer International Publishing},
  abstract = {Blockchain-based distributed computing platforms enable the trusted execution of
    computation---defined in the form of smart contracts---without trusted agents. Smart contracts are
    envisioned to have a variety of applications, ranging from financial to IoT asset tracking.
    Unfortunately, the development of smart contracts has proven to be extremely error prone. In practice,
    contracts are riddled with security vulnerabilities comprising a critical issue since bugs are by
    design non-fixable and contracts may handle financial assets of significant value. To facilitate the
    development of secure smart contracts, we have created the FSolidM framework, which allows developers
    to define contracts as finite state machines (FSMs) with rigorous and clear semantics. FSolidM
    provides an easy-to-use graphical editor for specifying FSMs, a code generator for creating Ethereum
    smart contracts, and a set of plugins that developers may add to their FSMs to enhance security and
    functionality.},
  isbn  = {978-3-319-89722-6}
}

@InProceedings{   Ahrendt2020,
  author = {Ahrendt, Wolfgang and Bubel, Richard},
  booktitle = {Leveraging Applications of Formal Methods, Verification and Validation: Applications},
  title  = {Functional Verification of Smart Contracts via Strong Data Integrity},
  year  = 2020,
  address = {Cham},
  editor = {Margaria, Tiziana and Steffen, Bernhard},
  pages  = {9--24},
  publisher = {Springer International Publishing},
  abstract = {We present an invariant-based specification and verification methodology that allows us to
    conveniently specify and verify strong data integrity properties for Solidity smart contracts. Our
    approach is able to reason precisely about arbitrary usage of the contracts, which may include
    re-entrance, a common security pitfall in smart contracts. We implemented the approach in a prototype
    verification tool, called SolidiKeY, and applied it successfully to a number of smart contracts.},
  isbn  = {978-3-030-61467-6}
}

@Article{   Ahrendt2016,
  author = {Ahrendt, Wolfgang and Beckert, Bernhard and Bubel, Richard and H{\"a}hnle, Reiner and Schmitt, Peter
    H and Ulbrich, Mattias},
  journal = {Lecture Notes in Computer Science},
  title  = {Deductive software verification--the key book},
  year  = 2016,
  volume = 10001,
  publisher = {Springer}
}

@InProceedings{   Crafa2020,
  author = {Crafa, Silvia and Di Pirro, Matteo and Zucca, Elena},
  booktitle = {Financial Cryptography and Data Security},
  title  = {Is Solidity Solid Enough?},
  year  = 2020,
  address = {Cham},
  editor = {Bracciali, Andrea and Clark, Jeremy and Pintore, Federico and R{\o}nne, Peter B. and Sala,
    Massimiliano},
  pages  = {138--153},
  publisher = {Springer International Publishing},
  abstract = {We introduce Featherweight Solidity, a calculus formalizing the core features of the Solidity
    language, thus providing a fundamental step to reason about safety properties of smart contracts'
    source code. The formalization includes a static type system that represents the foundation of the
    Solidity compiler. We show that it prevents some errors whereas many others, such as accesses to a non
    existing function or state variable, are only detected at runtime and cause interruption and
    rolling-back of transactions. We then propose a refinement of the type system that is retro-compatible
    with original Solidity code, and statically captures more errors, such as unsafe casts and unsafe
    call-back expressions.},
  isbn  = {978-3-030-43725-1}
}

@Misc{    Remix,
  author = {Online},
  howpublished = {\url{https://remix-ide.readthedocs.io/en/latest}},
  title  = {Remix - Solidity IDE}
}

@InProceedings{   Bartoletti2019,
  author = {Bartoletti, Massimo and Galletta, Letterio and Murgia, Maurizio},
  booktitle = {Data Privacy Management, Cryptocurrencies and Blockchain Technology},
  title  = {A Minimal Core Calculus for Solidity Contracts},
  year  = 2019,
  address = {Cham},
  editor = {P{\'e}rez-Sol{\`a}, Cristina and Navarro-Arribas, Guillermo and Biryukov, Alex and Garcia-Alfaro,
    Joaquin},
  pages  = {233--243},
  publisher = {Springer International Publishing},
  abstract = {The Ethereum platform supports the decentralized execution of smart contracts, i.e. computer programs
    that transfer digital assets between users. The most common language used to develop these contracts
    is Solidity, a Javascript-like language which compiles into EVM bytecode, the language actually
    executed by Ethereum nodes. While much research has addressed the formalisation of the semantics of
    EVM bytecode, relatively little attention has been devoted to that of Solidity. In this paper we
    propose a minimal calculus for Solidity contracts, which extends an imperative core with a single
    primitive to transfer currency and invoke contract procedures. We build upon this formalisation to
    give semantics to the Ethereum blockchain. We show our calculus expressive enough to reason about some
    typical quirks of Solidity, like e.g. re-entrancy.},
  isbn  = {978-3-030-31500-9}
}

@InProceedings{   Zakrzewski2018,
  author = {Jakub Zakrzewski},
  booktitle = {Verified Software. Theories, Tools, and Experiments - 10th International Conference, {VSTTE} 2018,
    Oxford, UK, July 18-19, 2018, Revised Selected Papers},
  title  = {Towards Verification of Ethereum Smart Contracts: {A} Formalization of Core of Solidity},
  year  = 2018,
  editor = {Ruzica Piskac and Philipp R{\"{u}}mmer},
  pages  = {229--247},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 11294,
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl = {https://dblp.org/rec/conf/vstte/Zakrzewski18.bib},
  doi  = {10.1007/978-3-030-03592-1\_13},
  timestamp = {Tue, 14 May 2019 10:00:49 +0200},
  url  = {https://doi.org/10.1007/978-3-030-03592-1\_13}
}

@InProceedings{   Hajdu2020,
  author = {Hajdu, {\'A}kos and Jovanovi{\'{c}}, Dejan},
  booktitle = {Verified Software. Theories, Tools, and Experiments},
  title  = {solc-verify: A Modular Verifier for Solidity Smart Contracts},
  year  = 2020,
  address = {Cham},
  editor = {Chakraborty, Supratik and Navas, Jorge A.},
  pages  = {161--179},
  publisher = {Springer International Publishing},
  abstract = {We present solc-verify, a source-level verification tool for Ethereum smart contracts. solc-verify
    takes smart contracts written in Solidity and discharges verification conditions using modular program
    analysis and SMT solvers. Built on top of the Solidity compiler, solc-verify reasons at the level of
    the contract source code, as opposed to the more common approaches that operate at the level of
    Ethereum bytecode. This enables solc-verify to effectively reason about high-level contract properties
    while modeling low-level language semantics precisely. The properties, such as contract invariants,
    loop invariants, and function pre- and post-conditions, can be provided as annotations in the code by
    the developer. This enables automated, yet user-friendly formal verification for smart contracts. We
    demonstrate solc-verify by examining real-world examples where our tool can effectively find bugs and
    prove correctness of non-trivial properties with minimal user effort.},
  isbn  = {978-3-030-41600-3}
}

@InProceedings{   Amani2018,
  author = {Amani, Sidney and B\'{e}gel, Myriam and Bortin, Maksym and Staples, Mark},
  booktitle = {Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  title  = {Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL},
  year  = 2018,
  address = {New York, NY, USA},
  pages  = {66{\^a}€“77},
  publisher = {Association for Computing Machinery},
  series = {CPP 2018},
  abstract = {Blockchain technology has increasing attention in research and across many industries. The Ethereum
    blockchain offers smart contracts, which are small programs defined, executed, and recorded as
    transactions in the blockchain transaction history. These smart contracts run on the Ethereum Virtual
    Machine (EVM) and can be used to encode agreements, transfer assets, and enforce integrity conditions
    in relationships between parties. Smart contracts can carry financial value, and are increasingly used
    for safety-, security-, or mission-critical purposes. Errors in smart contracts have led and will lead
    to loss or harm. Formal verification can provide the highest level of confidence about the correct
    behaviour of smart contracts. In this paper we extend an existing EVM formalisation in Isabelle/HOL by
    a sound program logic at the level of bytecode. We structure bytecode sequences into blocks of
    straight-line code and create a program logic to reason about these. This abstraction is a step
    towards control of the cost and complexity of formal verification of EVM smart contracts.},
  doi  = {10.1145/3167084},
  isbn  = 9781450355865,
  keywords = {blockchain, formal verification, smart contracts, Ethereum, Isabelle/HOL},
  location = {Los Angeles, CA, USA},
  numpages = 12,
  url  = {https://doi.org/10.1145/3167084}
}

@Misc{   Wood2014,
  author = {Wood, Gavin and others},
  journal = {Ethereum project yellow paper},
  title  = {Ethereum: A secure decentralised generalised transaction ledger},
  year  = 2022,
  note = {Berlin Version 3078285 -- 2022-07-13. \url{https://ethereum.github.io/yellowpaper/paper.pdf}},
  pages  = {1--32},
}

@Misc{    Solidity,
  author = {Online},
  howpublished = {\url{https://solidity.readthedocs.io/en/latest}},
  title  = {Solidity documentation}
}

@InProceedings{   Grishchenko2018,
  author = {Grishchenko, Ilya and Maffei, Matteo and Schneidewind, Clara},
  booktitle = {Principles of Security and Trust},
  title  = {A Semantic Framework for the Security Analysis of Ethereum Smart Contracts},
  year  = 2018,
  address = {Cham},
  editor = {Bauer, Lujo and K{\"u}sters, Ralf},
  pages  = {243--269},
  publisher = {Springer International Publishing},
  abstract = {Smart contracts are programs running on cryptocurrency (e.g., Ethereum) blockchains, whose popularity
    stem from the possibility to perform financial transactions, such as payments and auctions, in a
    distributed environment without need for any trusted third party. Given their financial nature, bugs
    or vulnerabilities in these programs may lead to catastrophic consequences, as witnessed by recent
    attacks. Unfortunately, programming smart contracts is a delicate task that requires strong expertise:
    Ethereum smart contracts are written in Solidity, a dedicated language resembling JavaScript, and
    shipped over the blockchain in the EVM bytecode format. In order to rigorously verify the security of
    smart contracts, it is of paramount importance to formalize their semantics as well as the security
    properties of interest, in particular at the level of the bytecode being executed.},
  isbn  = {978-3-319-89722-6}
}

@Article{   Wood2014a,
  author = {Wood, Gavin and others},
  journal = {Ethereum project yellow paper},
  title  = {Ethereum: A secure decentralised generalised transaction ledger},
  year  = 2014,
  number = 2014,
  pages  = {1--32},
  volume = 151
}

@InProceedings{   Swamy2016,
  author = {Swamy, Nikhil and Hri\c{t}cu, C\u{a}t\u{a}lin and Keller, Chantal and Rastogi, Aseem and
    Delignat-Lavaud, Antoine and Forest, Simon and Bhargavan, Karthikeyan and Fournet, C\'{e}dric and
    Strub, Pierre-Yves and Kohlweiss, Markulf and Zinzindohoue, Jean-Karim and Zanella-B\'{e}guelin, Santiago},
  booktitle = {Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  title  = {Dependent Types and Multi-Monadic Effects in F*},
  year  = 2016,
  address = {New York, NY, USA},
  pages  = {256{\^a}€“270},
  publisher = {Association for Computing Machinery},
  series = {POPL '16},
  abstract = {We present a new, completely redesigned, version of F*, a language that works both as a proof
    assistant as well as a general-purpose, verification-oriented, effectful programming language. In
    support of these complementary roles, F* is a dependently typed, higher-order, call-by-value language
    with _primitive_ effects including state, exceptions, divergence and IO. Although primitive,
    programmers choose the granularity at which to specify effects by equipping each effect with a
    monadic, predicate transformer semantics. F* uses this to efficiently compute weakest preconditions
    and discharges the resulting proof obligations using a combination of SMT solving and manual proofs.
    Isolated from the effects, the core of F* is a language of pure functions used to write specifications
    and proof terms---its consistency is maintained by a semantic termination check based on a
    well-founded order. We evaluate our design on more than 55,000 lines of F* we have authored in the
    last year, focusing on three main case studies. Showcasing its use as a general-purpose programming
    language, F* is programmed (but not verified) in F*, and bootstraps in both OCaml and F#. Our
    experience confirms F*'s pay-as-you-go cost model: writing idiomatic ML-like code with no finer
    specifications imposes no user burden. As a verification-oriented language, our most significant
    evaluation of F* is in verifying several key modules in an implementation of the TLS-1.2 protocol
    standard. For the modules we considered, we are able to prove more properties, with fewer annotations
    using F* than in a prior verified implementation of TLS-1.2. Finally, as a proof assistant, we discuss
    our use of F* in mechanizing the metatheory of a range of lambda calculi, starting from the simply
    typed lambda calculus to System F-omega and even micro-F*, a sizeable fragment of F* itself---these
    proofs make essential use of F*'s flexible combination of SMT automation and constructive proofs,
    enabling a tactic-free style of programming and proving at a relatively large scale.},
  doi  = {10.1145/2837614.2837655},
  isbn  = 9781450335492,
  keywords = {effectful programming, verification, proof assistants},
  location = {St. Petersburg, FL, USA},
  numpages = 15,
  url  = {https://doi.org/10.1145/2837614.2837655}
}

@Article{   10.1145/2914770.2837655,
  author = {Swamy, Nikhil and Hri\c{t}cu, C\u{a}t\u{a}lin and Keller, Chantal and Rastogi, Aseem and
    Delignat-Lavaud, Antoine and Forest, Simon and Bhargavan, Karthikeyan and Fournet, C\'{e}dric and
    Strub, Pierre-Yves and Kohlweiss, Markulf and Zinzindohoue, Jean-Karim and Zanella-B\'{e}guelin, Santiago},
  journal = {SIGPLAN Not.},
  title  = {Dependent Types and Multi-Monadic Effects in F*},
  year  = 2016,
  issn  = {0362-1340},
  month  = jan,
  number = 1,
  pages  = {256{\^a}€“270},
  volume = 51,
  abstract = {We present a new, completely redesigned, version of F*, a language that works both as a proof
    assistant as well as a general-purpose, verification-oriented, effectful programming language. In
    support of these complementary roles, F* is a dependently typed, higher-order, call-by-value language
    with _primitive_ effects including state, exceptions, divergence and IO. Although primitive,
    programmers choose the granularity at which to specify effects by equipping each effect with a
    monadic, predicate transformer semantics. F* uses this to efficiently compute weakest preconditions
    and discharges the resulting proof obligations using a combination of SMT solving and manual proofs.
    Isolated from the effects, the core of F* is a language of pure functions used to write specifications
    and proof terms---its consistency is maintained by a semantic termination check based on a
    well-founded order. We evaluate our design on more than 55,000 lines of F* we have authored in the
    last year, focusing on three main case studies. Showcasing its use as a general-purpose programming
    language, F* is programmed (but not verified) in F*, and bootstraps in both OCaml and F#. Our
    experience confirms F*'s pay-as-you-go cost model: writing idiomatic ML-like code with no finer
    specifications imposes no user burden. As a verification-oriented language, our most significant
    evaluation of F* is in verifying several key modules in an implementation of the TLS-1.2 protocol
    standard. For the modules we considered, we are able to prove more properties, with fewer annotations
    using F* than in a prior verified implementation of TLS-1.2. Finally, as a proof assistant, we discuss
    our use of F* in mechanizing the metatheory of a range of lambda calculi, starting from the simply
    typed lambda calculus to System F-omega and even micro-F*, a sizeable fragment of F* itself---these
    proofs make essential use of F*'s flexible combination of SMT automation and constructive proofs,
    enabling a tactic-free style of programming and proving at a relatively large scale.},
  address = {New York, NY, USA},
  doi  = {10.1145/2914770.2837655},
  issue_date = {January 2016},
  keywords = {proof assistants, verification, effectful programming},
  numpages = 15,
  publisher = {Association for Computing Machinery},
  url  = {https://doi.org/10.1145/2914770.2837655}
}

@Article{   Mulligan2014,
  author = {Mulligan, Dominic P. and Owens, Scott and Gray, Kathryn E. and Ridge, Tom and Sewell, Peter},
  journal = {SIGPLAN Not.},
  title  = {Lem: Reusable Engineering of Real-World Semantics},
  year  = 2014,
  issn  = {0362-1340},
  month  = aug,
  number = 9,
  pages  = {175{\^a}€“188},
  volume = 49,
  abstract = {Recent years have seen remarkable successes in rigorous engineering: using mathematically rigorous
    semantic models (not just idealised calculi) of real-world processors, programming languages,
    protocols, and security mechanisms, for testing, proof, analysis, and design. Building these models is
    challenging, requiring experimentation, dialogue with vendors or standards bodies, and validation;
    their scale adds engineering issues akin to those of programming to the task of writing clear and
    usable mathematics. But language and tool support for specification is lacking. Proof assistants can
    be used but bring their own difficulties, and a model produced in one, perhaps requiring many
    person-years effort and maintained over an extended period, cannot be used by those familiar with
    another.We introduce Lem, a language for engineering reusable large-scale semantic models. The Lem
    design takes inspiration both from functional programming languages and from proof assistants, and Lem
    definitions are translatable into OCaml for testing, Coq, HOL4, and Isabelle/HOL for proof, and LaTeX
    and HTML for presentation. This requires a delicate balance of expressiveness, careful library design,
    and implementation of transformations - akin to compilation, but subject to the constraint of
    producing usable and human-readable code for each target. Lem's effectiveness is demonstrated by its
    use in practice.},
  address = {New York, NY, USA},
  doi  = {10.1145/2692915.2628143},
  issue_date = {September 2014},
  keywords = {proof assistants, real-world semantics, lem, specification languages},
  numpages = 14,
  publisher = {Association for Computing Machinery},
  url  = {https://doi.org/10.1145/2692915.2628143}
}

@InProceedings{   10.1145/2628136.2628143,
  author = {Mulligan, Dominic P. and Owens, Scott and Gray, Kathryn E. and Ridge, Tom and Sewell, Peter},
  booktitle = {Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming},
  title  = {Lem: Reusable Engineering of Real-World Semantics},
  year  = 2014,
  address = {New York, NY, USA},
  pages  = {175{\^a}€“188},
  publisher = {Association for Computing Machinery},
  series = {ICFP '14},
  abstract = {Recent years have seen remarkable successes in rigorous engineering: using mathematically rigorous
    semantic models (not just idealised calculi) of real-world processors, programming languages,
    protocols, and security mechanisms, for testing, proof, analysis, and design. Building these models is
    challenging, requiring experimentation, dialogue with vendors or standards bodies, and validation;
    their scale adds engineering issues akin to those of programming to the task of writing clear and
    usable mathematics. But language and tool support for specification is lacking. Proof assistants can
    be used but bring their own difficulties, and a model produced in one, perhaps requiring many
    person-years effort and maintained over an extended period, cannot be used by those familiar with
    another.We introduce Lem, a language for engineering reusable large-scale semantic models. The Lem
    design takes inspiration both from functional programming languages and from proof assistants, and Lem
    definitions are translatable into OCaml for testing, Coq, HOL4, and Isabelle/HOL for proof, and LaTeX
    and HTML for presentation. This requires a delicate balance of expressiveness, careful library design,
    and implementation of transformations - akin to compilation, but subject to the constraint of
    producing usable and human-readable code for each target. Lem's effectiveness is demonstrated by its
    use in practice.},
  doi  = {10.1145/2628136.2628143},
  isbn  = 9781450328739,
  keywords = {real-world semantics, lem, specification languages, proof assistants},
  location = {Gothenburg, Sweden},
  numpages = 14,
  url  = {https://doi.org/10.1145/2628136.2628143}
}

@Manual{   solidity-0.8.4,
  title  = {Solidity (Version 0.8.4)},
  howpublished = {\url{https://docs.soliditylang.org/en/v0.8.4/}}
}

@TechReport{   wood:ethereum:2021,
  author = {Gavin Wood},
  title  = {Ethereum: A Secure Decentralised Generalised Transation Ledger (Version 2021-04-21)},
  optnote = {\url{https://ethereum.github.io/yellowpaper/paper.pdf}}
}

@Misc{    coinmarket,
  title  = {The {Bitcon} Market Capitalisation.},
  url  = {https://coinmarketcap.com/currencies/bitcoin/},
  note  = {Last checked on 2021-05-04.}
}

@InCollection{   marmsoler.ea:conformance:2022,
  abstract = {A common problem in verification is to ensure that the formal specification models the real-world
    system, i.e., the implementation, faithfully. Testing is a technique that can help to bridge the gap
    between a formal specification and its implementation.\\\\Fuzzing in general and grammar-based fuzzing
    in particular are successfully used for finding bugs in implementations. Traditional fuzzing
    applications rely on an implicit test specification that informally can be described as ``the program
    under test does not crash''.\\\\In this paper, we present an approach using grammar-based fuzzing to
    ensure the conformance of a formal specification, namely the formal semantics of the Solidity
    Programming language, to a real-world implementation. For this, we derive an executable test-oracle
    from the formal semantics of Solidity in Isabelle/HOL. The derived test oracle is used during the
    fuzzing of the implementation to validate that the formal semantics and the implementation are in
    conformance.},
  address = {Heidelberg},
  author = {Diego Marmsoler and Achim D. Brucker},
  booktitle = {{TAP} 2022: Tests And Proofs},
  editor = {Laura Kovacs and Karl Meinke},
  isbn  = {978-3-642-38915-3},
  keywords = {Conformance Testing, Fuzzing, Verification, Solidity},
  language = {USenglish},
  location = {Nantes, France},
  pdf  = {https://www.brucker.ch/bibliography/download/2022/marmsoler.ea-conformance-2022.pdf},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  title  = {Conformance Testing of Formal Semantics using Grammar-based Fuzzing},
  url  = {https://www.brucker.ch/bibliography/abstract/marmsoler.ea-conformance-2022},
  year  = 2022
}

@InCollection{   marmsoler.ea:solidity-semantics:2021,
  abstract = {Smart contracts are programs, usually automating legal agreements such as financial transactions.
    Thus, bugs in smart contracts can lead to large financial losses. For example, an incorrectly
    initialized contract was the root cause of the Parity Wallet bug that made USD 280mil worth of Ether
    inaccessible. Ether is the cryptocurrency of the Ethereum blockchain that uses Solidity for expressing
    smart contracts.\\\\In this paper, we address this problem by presenting an executable denotational
    semantics for Solidity in the interactive theorem prover Isabelle/HOL. This formal semantics builds
    the foundation of an interactive program verification environment for Solidity programs and allows for
    inspecting Solidity programs by (symbolic) execution. We combine the latter with grammar-based fuzzing
    to ensure that our formal semantics complies to the Solidity implementation on the Ethereum
    Blockchain. Finally, we demonstrate the formal verification of Solidity programs by two examples:
    constant folding and memory optimization.},
  address = {Heidelberg},
  author = {Diego Marmsoler and Achim D. Brucker},
  booktitle = {Software Engineering and Formal Methods (SEFM)},
  editor = {Radu Calinescu and Corina Pasareanu},
  isbn  = {3-540-25109-X},
  keywords = {Solidity, Denotational Semantics, Isabelle/HOL, Gas Optimization},
  language = {USenglish},
  pdf  = {https://www.brucker.ch/bibliography/download/2021/marmsoler.ea-solidity-semantics-2021.pdf},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  title  = {A Denotational Semantics of {Solidity} in {Isabelle/HOL}},
  url  = {https://www.brucker.ch/bibliography/abstract/marmsoler.ea-solidity-semantics-2021},
  year  = 2021
}
@COMMENT{jabref-meta: databaseType:bibtex;}