Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
Next revisionBoth sides next revision
research:csec [2018/03/21 10:02] – etanterresearch:csec [2018/03/21 10:03] – etanter
Line 20: Line 20:
  
 **Federico Olmedo**: **Federico Olmedo**:
-     * ++ Language-based Cryptographic Proofs in Coq, or Coq for Probabilistic Programs {{research:csec:olmedo-crypto.pdf|slides}} | Between many others, cryptography is a field where formal, machine-aided, verification has been applied with great success. In this talk I will present CertiCrypt, a framework for building certified cryptographic proofs on top of the Coq proof assistant. The key insight behind this framework is understanding cryptographic proofs as a problem of relational, probabilistic, program verification. Throughout the talk, I will overview the different features that the framework offers for reasoning about probabilistic programs, including a complete formalization of the semantics of an imperative probabilistic language, a set of certified program transformations and a full-fledged relational Hoare logic. +++     * ++ Language-based Cryptographic Proofs in Coq, or Coq for Probabilistic Programs | Between many others, cryptography is a field where formal, machine-aided, verification has been applied with great success. In this talk I will present CertiCrypt, a framework for building certified cryptographic proofs on top of the Coq proof assistant. The key insight behind this framework is understanding cryptographic proofs as a problem of relational, probabilistic, program verification. Throughout the talk, I will overview the different features that the framework offers for reasoning about probabilistic programs, including a complete formalization of the semantics of an imperative probabilistic language, a set of certified program transformations and a full-fledged relational Hoare logic. {{research:csec:olmedo-crypto.pdf|slides}} ++
      * ++ Improving the Proof Experience in Coq | As Coq users for the development of mid and large scale projects, over the years we have encountered some hurdles that usually impacted negatively in our proof development process. In these talk we will informally identify some of these obstacles and discuss related solutions that could overall improve both the user proof experience and the quality attributes of the developed proofs.++      * ++ Improving the Proof Experience in Coq | As Coq users for the development of mid and large scale projects, over the years we have encountered some hurdles that usually impacted negatively in our proof development process. In these talk we will informally identify some of these obstacles and discuss related solutions that could overall improve both the user proof experience and the quality attributes of the developed proofs.++