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 09:58] – 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 | 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.++
  
Line 50: Line 50:
 ==== Participants ==== ==== Participants ====
  
-**The talks are open to whoever wants to attend, just show up!** 
- 
-Participants so far: 
   * Martin Bodin (U Chile)   * Martin Bodin (U Chile)
   * Raimil Cruz (U Chile)   * Raimil Cruz (U Chile)
Line 69: Line 66:
   * Matías Toro (U Chile)   * Matías Toro (U Chile)
   * Beta Ziliani (U Córdoba)   * Beta Ziliani (U Córdoba)
- 
-==== Other practical info ==== 
- 
-     * lunches will be at restaurant [[https://www.facebook.com/Picadelly-145207942209018/|Picadelly]], on club hipico street, 5 min walk from the DCC. It's both a pizza place and a restaurant with 4-5 "menu of the day" options. Aprox 4.000 CLP. 
-     * **Thursday afternoon 6pm**: we are invited by Claude Puech to visit [[http://inria.cl/|Inria Chile]] 
-     * We will coordinate dinners every evening 
-