| Both sides previous revisionPrevious revisionNext revision | Previous revision |
| cc7125:proyectos-2017 [2017/11/09 12:42] – etanter | cc7125:proyectos-2017 [2017/11/09 13:05] (current) – removed etanter |
|---|
| ====== Lista de Artículos/Proyectos Posibles para Presentar ====== | |
| |
| Esta lista es sólo un punto de partida, también pueden sugerir otro artículo/proyecto que le gustaría presentar. | |
| |
| - [[http://goto.ucsd.edu/quark/usenix12.pdf|Establishing Browser Security Guarantees through Formal Shim Verification]] | |
| - [[http://ynot.cs.harvard.edu/papers/jsc-wwv-10.pdf|Trace-based Verification of Imperative Programs with I/O]] | |
| - [[http://ynot.cs.harvard.edu/papers/popl10.pdf|Toward a Verified Relational Database Management System]] | |
| - [[http://www.impredicative.com/ur/|Ur/Web]] | |
| - [[http://css.csail.mit.edu/fscq/|fscq]] | |
| - [[http://fbinfer.com/docs/separation-logic-and-bi-abduction.html#technical-papers|Infer]] | |
| - [[http://www.cis.upenn.edu/~stevez/vellvm/|Vellvm]] | |
| - [[https://doi.org/10.1016/j.entcs.2008.04.064|Building Certified Static Analysers by Modular Construction of Well-founded Lattices]] | |
| - Algún tópico avanzado del libro [[http://adam.chlipala.net/cpdt/|Certified Programming with Dependent Types]] | |
| |
| **Tienen que validar su propuesta conmigo por email a más tardar el 8 de Noviembre.** | |
| |
| ===== Grupos/Presentaciones ===== | |
| |
| **Llenar [[https://doodle.com/poll/rdibih2cw9rht22c|el Doodle]] para la(s) sesion(es) de presentación a más tardar el 8 de Noviembre.** | |
| |
| La presentación puede ser uno o dos alumnos. En caso de ser dos, la presentación tiene que tener dos partes balanceadas, y ambos deben poder presentar cualquiera de las partes (se determinará al azar). Ambos deben ser capaces de responder las preguntas. Las notas serán individuales. | |
| |
| La presentación será de 15-20 minutos + preguntas (//se ajustará según planificación//) | |
| |
| * Nicolás Caracci: //CompCert// | |
| * Fabián Mosso: //Iris: Separation Logic in Coq// | |
| * Nicolás Bravo & Juan Rojas: [[http://ynot.cs.harvard.edu/papers/popl10.pdf|Toward a Verified Relational Database Management System]] | |
| * Pablo Astudillo: [[http://css.csail.mit.edu/fscq/|fscq: A Formally Certified Crash-proof File System]] | |
| * Matiás Toro: [[http://www.impredicative.com/ur/|Ur/Web]] | |
| * Matías Meneses: [[http://goto.ucsd.edu/quark/usenix12.pdf|Establishing Browser Security Guarantees through Formal Shim Verification]] | |
| * Maximiliano Kauer: [[http://ynot.cs.harvard.edu/papers/jsc-wwv-10.pdf|Trace-based Verification of Imperative Programs with I/O]] | |
| * Hans Fehrmann: [[https://doi.org/10.1016/j.entcs.2008.04.064|Building Certified Static Analysers by Modular Construction of Well-founded Lattices]] | |
| * Paula Ríos & Tomás Díaz: [[http://fbinfer.com/docs/separation-logic-and-bi-abduction.html#technical-papers|Infer]] | |
| * Sergio Peñafiel: //Red-black trees (VFA-style vs. CPDT-style)// | |
| * Elizabeth Labrada: [[http://www.staff.city.ac.uk/~ross/papers/pts.pdf|Parametricity and Dependent Types]] | |
| |
| |
| |
