Differences

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

--- start [2018/10/21 16:16]
vkuncak
+++ start [2023/08/28 21:31] (current)
vkuncak
@@ Line 1: / Line 1: @@
+<html>
+<style>
+p {
+   font-size: 24px !important;
+}
+</style>
-===== Mission: Help people construct software that does what they expect =====
+<p>
+<strong>
+Helping construct software that does what we expect
+</strong>
+</p>
-**LARA** is a research group led by [[http://lara.epfl.ch/~kuncak|Viktor Kunčak]] We develops precise automated reasoning techniques: tools, algorithms, languages and apply these techniques to **synthesis** and **verification** of computer systems. See, for example, https://stainless.epfl.ch
+<p>(<a href="https://epfl-lara.github.io/">Click here for simpler version of this page on GitHub</a>)</p>
+<table width="60%" align="bottom">
+<tr><td>
+<p>
+LARA is a research group led by
+<strong><a href="http://lara.epfl.ch/~kuncak">Viktor Kunčak</a></strong>.
+We develop precise automated reasoning techniques: tools, algorithms and languages. The goal of these techniques is to help the construction of verified computer systems. See, for example, the
+<strong><a href="https://stainless.epfl.ch">Stainless project</a></strong>.
+</p>
+</td></tr>
+</table>
+</html>
-Our goal is to enable people to easily program and construct reliable and sophisticated systems.
 ===== Scientific Staff =====
@@ Line 12: / Line 34: @@
 <tr>
 <td align="center" valign="bottom">
-<a href="http://lara.epfl.ch/~kuncak">
+<a href="https://lara.epfl.ch/~kuncak">
-<img src="http://lara.epfl.ch/~kuncak/staff/viktor.png"
+<img src="https://lara.epfl.ch/~kuncak/staff/viktor.png"
 width='160'
-alt="Viktor Kuncak">
+alt="Viktor Kunčak">
 </a>
 <br>
-<a href="http://icwww.epfl.ch/~kuncak">Viktor Kuncak</a>
+<a href="https://lara.epfl.ch/~kuncak">Viktor Kunčak</a>
 </td>
-</tr>
-<tr>
 <td align="center" valign="bottom">
-<a href="http://lara.epfl.ch/~pavlogia/">
+<a href="https://people.epfl.ch/mario.bucev/">
-<img src="http://lara.epfl.ch/~pavlogia/profile.jpg"
+<img src="https://people.epfl.ch/private/common/photos/links/247537.jpg" width='160'
-width='160'
+alt="Mario Bucev">
-alt="Andreas Pavlogiannis">
 </a>
 <br>
-<a href="http://lara.epfl.ch/~pavlogia/">Andreas Pavlogiannis</a>
+<a href="https://people.epfl.ch/mario.bucev/">Mario Bucev</a>
-</td>
-<td align="center" valign="top">
-<a href="http://people.epfl.ch/jad.hamza">
-<img src="http://lara.epfl.ch/~kuncak/staff/jad.jpg"
-width='160' alt="Jad Hamza"/>
-</a>
-<br>
-<a href="http://people.epfl.ch/jad.hamza">Jad Hamza</a>
-<br>
 </td>
 <td align="center" valign="bottom">
-<a href="https://people.epfl.ch/georg.schmid">
+<a href="https://people.epfl.ch/sankalp.gambhir">
-<img src="http://lara.epfl.ch/~kuncak/staff/georg.jpg" width='160'
+<img src="https://lara.epfl.ch/~kuncak/staff/somebody.png" width='160'
-alt="Georg S. Schmid">
+alt="Sankalp Gambhir">
 </a>
 <br>
-<a href="https://people.epfl.ch/georg.schmid">Georg S. Schmid</a>
+<a href="https://people.epfl.ch/sankalp.gambhir">Sankalp Gambhir</a>
 </td>
 </tr>
 <tr>
 <td align="center" valign="bottom">
-<a href="https://people.epfl.ch/romain.edelmann">
+<a href="https://people.epfl.ch/dragana.milovancevic">
-<img src="http://lara.epfl.ch/~kuncak/staff/romain.jpg"
+<img src="https://people.epfl.ch/private/common/photos/links/289485.jpg?ts=1612961306" width='160'
-width='160' alt="Romain Edelmann"/>
+alt="Dragana Milovancevic">
 </a>
 <br>
-<a href="https://people.epfl.ch/romain.edelmann">Romain Edelmann</a>
+<a href="https://people.epfl.ch/dragana.milovancevic">Dragana Milovancevic</a>
 </td>
 <td align="center" valign="bottom">
-<a href="http://people.epfl.ch/nicolas.voirol">
+<a href="https://people.epfl.ch/simon.guilloud">
-<img src="http://lara.epfl.ch/~kuncak/staff/nicolas.jpg"
+<img src="https://people.epfl.ch/private/common/photos/links/250109.jpg?ts=1612961599" width='160'
-width='160' alt="Nicolas Voirol"/>
+alt="Simon Guilloud">
 </a>
 <br>
-<a href="http://people.epfl.ch/nicolas.voirol">Nicolas Voirol</a>
+<a href="https://people.epfl.ch/simon.guilloud">Simon Guilloud</a>
 </td>
 <td align="center" valign="bottom">
-<a href="https://romac.me/">
+<a href="https://dblp.org/pid/257/8380.html">
-<img src="http://lara.epfl.ch/~kuncak/staff/romac.jpg" width='160'
+<img src="http://lara.epfl.ch/~kuncak/staff/rodrigo.jpg" width='160'
-alt="Romain Ruetschi">
+alt="Rodrigo Raya"></a>
-</a>
 <br>
-<a href="https://romac.me/">Romain Ruetschi</a>
+<a href="https://people.epfl.ch/rodrigo.raya">Rodrigo Raya</a>
 </td>
-</tr>
-<tr>
-<td align="center" valign="top">
-<a href="http://people.epfl.ch/emmanouil.koukoutos">
-<img src="http://lara.epfl.ch/~kuncak/staff/manos.jpg"
-width='160' height='200' alt="Emmanouil Koukoutos"/>
-</a>
-<br>
-<a href="http://people.epfl.ch/emmanouil.koukoutos">Manos Koukoutos</a>
-<br>
-</td>
 </tr>
@@ Line 113: / Line 103: @@
 <td align="center" valign="top">
-<a href="http://people.epfl.ch/fabien.salvi">
+<a href="https://people.epfl.ch/fabien.salvi">
-<img src="http://lara.epfl.ch/~kuncak/staff/fabien.jpg"
+<img src="https://lara.epfl.ch/~kuncak/staff/fabien.jpg"
 width='160' alt="Fabien Salvi"/>
 </a>
 <br>
 System Manager <br>
-<a href="http://people.epfl.ch/fabien.salvi">Fabien Salvi</a>
+<a href="https://people.epfl.ch/fabien.salvi">Fabien Salvi</a>
 <br>
 </td>
 <td align="center" valign="top">
-<a href="https://people.epfl.ch/sylvie.jankow"">
+<a href="https://people.epfl.ch/sylvie.buchard">
-<img src="http://lara.epfl.ch/~kuncak/staff/sylvie.jpg"
+<img src="https://people.epfl.ch/private/common/photos/links/266882.jpg?ts=1639433244"
-width='160' alt="Yvette Gallay"/>
+width='160' alt="Sylvie Buchard"/>
 </a>
 <br>
 Secretary <br>
-<a href="http://people.epfl.ch/sylvie.jankow">Sylvie Jankow</a>
+<a href="https://people.epfl.ch/sylvie.buchard">Sylvie Buchard</a>
 <br>
 </td>
@@ Line 143: / Line 133: @@
 <html>
 <table width="50%" align="top">
+<tr>
+<td align="center" valign="top">
+<a href="https://dblp.org/pid/99/9609.html">
+<img src="https://lara.epfl.ch/~kuncak/staff/jad.jpg"
+width='160' alt="Jad Hamza"/>
+</a>
+<br>
+<a href="https://lara.epfl.ch/~hamza/">Jad Hamza</a>
+</td>
+<td align="center" valign="bottom">
+<a href="https://dblp.org/pid/206/2097.html">
+<img src="https://lara.epfl.ch/~kuncak/staff/romain.jpg" width='160'
+alt="Romain Edelmann">
+</a>
+<br>
+<a href="https://redelmann.ch/">Romain Edelmann</a>
+</td>
+<td align="center" valign="bottom">
+<a href="https://dblp.org/pid/198/4641.html">
+<img src="https://lara.epfl.ch/~kuncak/staff/georg.jpg" width='160'
+alt="Georg S. Schmid">
+</a>
+<br>
+<a href="https://people.epfl.ch/georg.schmid">Georg S. Schmid</a>
+</td>
+</tr>
+<tr>
+<td align="center" valign="bottom">
+<a href="https://cs.au.dk/~pavlogiannis/">
+<img src="https://lara.epfl.ch/~kuncak/staff/AndreasPavlogiannis.jpg"
+width='160'
+alt="Andreas Pavlogiannis">
+</a>
+<br>
+<a href="http://lara.epfl.ch/~pavlogia/">Andreas Pavlogiannis</a>
+</td>
+<td align="center" valign="bottom">
+<a href="https://romac.me/">
+<img src="https://lara.epfl.ch/~kuncak/staff/romac.jpg" width='160'
+alt="Romain Ruetschi">
+</a>
+<br>
+<a href="https://romac.me/">Romain Ruetschi</a>
+</td>
+<td align="center" valign="bottom">
+<a href="https://people.epfl.ch/nataliia.stulova?lang=en">
+<img src="https://lara.epfl.ch/w/_media/stulova.jpg" width='160'
+alt="Nataliia Stulova">
+</a>
+<br>
+<a href="https://people.epfl.ch/nataliia.stulova?lang=en">Nataliia Stulova</a>
+</td>
+</tr>
+<tr>
+<td align="center" valign="bottom">
+<a href="https://people.epfl.ch/nicolas.voirol">
+<img src="https://lara.epfl.ch/~kuncak/staff/nicolas.jpg"
+width='160' alt="Nicolas Voirol"/>
+</a>
+<br>
+<a href="https://people.epfl.ch/nicolas.voirol">Nicolas Voirol</a>
+</td>
+<td align="center" valign="bottom">
+<a href="https://people.epfl.ch/sarah.sallinger">
+<img src="https://lara.epfl.ch/~kuncak/staff/sarah.jpg" width='160'
+alt="Sarah Sallinger">
+</a>
+<br>
+<a href="https://people.epfl.ch/sarah.sallinger">Sarah Sallinger</a>
+</td>
+<td align="center" valign="top">
+<a href="https://people.epfl.ch/emmanouil.koukoutos">
+<img src="https://lara.epfl.ch/~kuncak/staff/manos.jpg"
+width='160' height='200' alt="Emmanouil Koukoutos"/>
+</a>
+<br>
+<a href="https://people.epfl.ch/emmanouil.koukoutos">Manos Koukoutos</a>
+<br>
+</td>
+</tr>
 <tr>
 <td align="center" valign="top">
-<a href="http://lara.epfl.ch/~kandhada">
+<a href="https://lara.epfl.ch/~kandhada">
-<img src="http://lara.epfl.ch/~kuncak/staff/ravi.jpg"
+<img src="https://lara.epfl.ch/~kuncak/staff/ravi.jpg"
 width='160' alt=""/>
 </a>
 <br>
-<a href="http://people.epfl.ch/ravi.kandhadai">Ravichandhran Kandhadai Madhavan</a>
+<a href="https://people.epfl.ch/ravi.kandhadai">Ravichandhran Kandhadai Madhavan</a>
 <br>
 </td>
 <td align="center" valign="top">
-<a href="http://people.epfl.ch/marco.antognini">
+<a href="https://people.epfl.ch/marco.antognini">
 <img src="/w/_media/marco_thumb.jpg"
 width='160' alt="Marco Antognini"/>
 </a>
 <br>
-<a href="http://people.epfl.ch/Marco Antognini">Marco Antognini</a>
+<a href="https://people.epfl.ch/Marco Antognini">Marco Antognini</a>
 <br>
 </td>
@@ Line 168: / Line 250: @@
 <td align="center" valign="top">
-<a href="http://people.epfl.ch/mikael.mayer">
+<a href="https://people.epfl.ch/mikael.mayer">
-<img src="http://lara.epfl.ch/~kuncak/staff/MikaelMayer.jpg"
+<img src="https://lara.epfl.ch/~kuncak/staff/MikaelMayer.jpg"
 width='160' alt=""/>
 </a>
 <br>
-<a href="http://people.epfl.ch/mikael.mayer">Mikael Mayer</a>
+<a href="https://people.epfl.ch/mikael.mayer">Mikael Mayer</a>
 <br>
 </td>
@@ Line 183: / Line 265: @@
 <td align="center" valign="bottom">
-<a href="http://people.epfl.ch/regis.blanc">
+<a href="https://people.epfl.ch/regis.blanc">
-<img src="http://lara.epfl.ch/~kuncak/staff/RegisBlanc.jpg"
+<img src="https://lara.epfl.ch/~kuncak/staff/RegisBlanc.jpg"
 width='160' alt=""/>
 </a>
 <br>
-<a href="http://people.epfl.ch/regis.blanc">Regis Blanc</a>
+<a href="https://people.epfl.ch/regis.blanc">Regis Blanc</a>
 <br>
 </td>
 <td align="center" valign="bottom">
-<a href="http://www.croustillant.ch/">
+<a href="https://www.croustillant.ch/">
-<img src="http://lara.epfl.ch/~kuncak/staff/etienne.png"
+<img src="https://lara.epfl.ch/~kuncak/staff/etienne.png"
 width='160' alt="Etienne Kneuss"/>
 </a>
 <br>
-<a href="http://lara.epfl.ch/~ekneuss/">Etienne Kneuss</a>
+<a href="https://lara.epfl.ch/~ekneuss/">Etienne Kneuss</a>
 </td>
 <td align="center" valign="top">
-<a href="http://people.epfl.ch/andrew.reynolds">
+<a href="https://people.epfl.ch/andrew.reynolds">
-<img src="http://lara.epfl.ch/~kuncak/staff/andrew.jpg"
+<img src="https://lara.epfl.ch/~kuncak/staff/andrew.jpg"
 width='160' alt="Andrew J. Reynolds"/>
 </a>
 <br>
-<a href="http://people.epfl.ch/andrew.reynolds">Andrew J. Reynolds</a>
+<a href="https://people.epfl.ch/andrew.reynolds">Andrew J. Reynolds</a>
 <br>
 </td>
@@ Line 217: / Line 299: @@
 <td align="center" valign="bottom">
-<a href="http://people.epfl.ch/eva.darulova">
+<a href="https://malyzajko.github.io/">
-<img src="http://lara.epfl.ch/~kuncak/staff/eva.png"
+<img src="https://lara.epfl.ch/~kuncak/staff/eva.png"
 width='160' alt="Eva Darulova"/>
 </a>
 <br>
-<a href="http://lara.epfl.ch/~darulova">Eva Darulova</a>
+<a href="https://malyzajko.github.io/">Eva Darulova</a>
 </td>
 <td align="center" valign="bottom">
-<a href="http://people.epfl.ch/tihomir.gvero">
+<a href="https://people.epfl.ch/tihomir.gvero">
-<img src="http://lara.epfl.ch/~kuncak/staff/tihomir.png"
+<img src="https://lara.epfl.ch/~kuncak/staff/tihomir.png"
 width='160' alt="Tihomir Gvero"/>
 </a>
 <br>
-<a href="http://tihomirg.github.io/">Tihomir Gvero</a>
+<a href="https://tihomirg.github.io/">Tihomir Gvero</a>
 </td>
 <td align="center" valign="top">
-<a href="http://people.epfl.ch/ivan.kuraj">
+<a href="https://people.epfl.ch/ivan.kuraj">
-<img src="http://lara.epfl.ch/~kuncak/staff/ivan.png"
+<img src="https://lara.epfl.ch/~kuncak/staff/ivan.png"
 width='160' alt="Ivan Kuraj"/>
 </a>
 <br>
-<a href="http://people.epfl.ch/ivan.kuraj">Ivan Kuraj</a>
+<a href="https://people.epfl.ch/ivan.kuraj">Ivan Kuraj</a>
 <br>
 </td>
@@ Line 249: / Line 331: @@
 <td align="center" valign="top">
-<a href="http://www.losa.fr/">
+<a href="https://www.losa.fr/">
-<img src="http://lara.epfl.ch/~kuncak/staff/giuliano.png"
+<img src="https://lara.epfl.ch/~kuncak/staff/giuliano.png"
 width='160' alt="Giuliano Losa"/>
 </a>
 <br>
-<a href="http://www.losa.fr/">Giuliano Losa</a>
+<a href="https://www.losa.fr/">Giuliano Losa</a>
 </td>
 <td align="center" valign="top">
-<a href="http://www.cs.cornell.edu/~hojjat/">
+<a href="https://www.cs.cornell.edu/~hojjat/">
-<img src="http://lara.epfl.ch/~kuncak/staff/HosseinHojjat.jpg"
+<img src="https://lara.epfl.ch/~kuncak/staff/HosseinHojjat.jpg"
 width='160' alt="Hossein Hojjat"/>
 </a>
 <br>
-<a href="http://www.cs.cornell.edu/~hojjat/">Hossein Hojjat</a>
+<a href="https://www.cs.cornell.edu/~hojjat/">Hossein Hojjat</a>
 <br>
 </td>
 <td align="center" valign="top">
-<a href="http://lara.epfl.ch/~psuter/">
+<a href="https://lara.epfl.ch/~psuter/">
-<img src="http://lara.epfl.ch/~kuncak/staff/philippe.png"
+<img src="https://lara.epfl.ch/~kuncak/staff/philippe.png"
 width='160' alt="Philippe Suter">
 </a>
 <br>
-<a href="http://lara.epfl.ch/~psuter/">Philippe Suter</a>
+<a href="https://lara.epfl.ch/~psuter/">Philippe Suter</a>
 </td>
@@ Line 281: / Line 363: @@
 <td align="center" valign="top">
-<a href="http://people.epfl.ch/filip.konecny">
+<a href="https://people.epfl.ch/filip.konecny">
-<img src="http://lara.epfl.ch/~kuncak/staff/FilipKonecny.jpg"
+<img src="https://lara.epfl.ch/~kuncak/staff/FilipKonecny.jpg"
 width='160' alt=""/>
 </a>
 <br>
-<a href="http://people.epfl.ch/filip.konecny">Filip Konecny</a>
+<a href="https://people.epfl.ch/filip.konecny">Filip Konecny</a>
 <br>
 </td>
 <td align="center" valign="top">
-<a href="http://people.epfl.ch/pierre-emmanuel.cornilleau">
+<a href="https://people.epfl.ch/pierre-emmanuel.cornilleau">
-<img src="http://lara.epfl.ch/~kuncak/staff/pierre-emmanuel.jpg"
+<img src="https://lara.epfl.ch/~kuncak/staff/pierre-emmanuel.jpg"
 width='160' alt="Pierre-Emmanuel Cornilleau"/>
 </a>
 <br>
-<a href="http://people.epfl.ch/pierre-emmanuel.cornilleau">Pierre-Emmanuel Cornilleau</a>
+<a href="https://people.epfl.ch/pierre-emmanuel.cornilleau">Pierre-Emmanuel Cornilleau</a>
 </td>
 <td align="center" valign="top">
-<a href="http://people.epfl.ch/andrej.spielmann">
+<a href="https://people.epfl.ch/andrej.spielmann">
-<img src="http://lara.epfl.ch/~kuncak/staff/andrej.png"
+<img src="https://lara.epfl.ch/~kuncak/staff/andrej.png"
 width='160' alt="Andrej Spielmann"/>
 </a>
@@ Line 313: / Line 395: @@
 <tr>
 <td align="center" valign="top">
-<a href="http://www.mpi-sws.org/~piskac/">
+<a href="http://www.cs.yale.edu/homes/piskac/">
-<img src="http://lara.epfl.ch/~kuncak/staff/ruzica.png"
+<img src="https://lara.epfl.ch/~kuncak/staff/ruzica.png"
 width='160' alt="Ruzica Piskac"/>
 </a>
 <br>
-<a href="http://www.mpi-sws.org/~piskac/">Ruzica Piskac</a> <br>
+<a href="http://www.cs.yale.edu/homes/piskac/">Ruzica Piskac</a> <br>
-(<a href="http://prix-etudiants.epfl.ch/page-51602-en.html">Patrick Denantes</a> <a href="http://library.epfl.ch/en/theses/?nr=5220">Dissertation Award</a>)
+(<a href="https://prix-etudiants.epfl.ch/page-51602-en.html">Patrick Denantes</a> <a href="http://library.epfl.ch/en/theses/?nr=5220">Dissertation Award</a>)
 </td>
 <td align="center" valign="top">
-<a href="http://www.iaik.tugraz.at/content/about_iaik/people/jacobs_swen/">
+<a href="https://www.iaik.tugraz.at/content/about_iaik/people/jacobs_swen/">
-<img src="http://lara.epfl.ch/~kuncak/staff/swen.png"
+<img src="https://lara.epfl.ch/~kuncak/staff/swen.png"
 width='160' alt="Swen Jacobs"/>
 </a>
 <br>
-<a href="http://www.iaik.tugraz.at/content/about_iaik/people/jacobs_swen/">Swen Jacobs</a>
+<a href="https://www.iaik.tugraz.at/content/about_iaik/people/jacobs_swen/">Swen Jacobs</a>
 </td>
 <td align="center" valign="top">
-<a href="http://www.cs.berkeley.edu/~koksal/">
+<a href="https://www.cs.berkeley.edu/~koksal/">
-<img src="http://lara.epfl.ch/~kuncak/staff/ali.jpg"
+<img src="https://lara.epfl.ch/~kuncak/staff/ali.jpg"
 width='160' alt="Ali Sinan Köksal"/>
 </a>
@@ Line 351: / Line 433: @@
 Information on joining and collaborating with LARA:
   * [[https://issuu.com/iccommunication/docs/ic-at-a-glance-d__pliant-prod-18-07|About IC]]
-  * for postdoc positions, email [[http://lara.epfl.ch/~kuncak|Viktor Kuncak]] and check [[http://commission-recherche.epfl.ch/EPFLFellows|EPFL Fellows program]] ({{epflfellows.pdf|PDF document}})
+  * for postdoc positions, email [[https://lara.epfl.ch/~kuncak|Viktor Kuncak]] and check [[http://commission-recherche.epfl.ch/EPFLFellows|EPFL Fellows program]] ({{epflfellows.pdf|PDF document}})
   * [[PhD Positions]] and information about EPFL
     * {{phdseminar09.pdf|Slides from a Seminar for Starting PhD Students}} (September 2009, somewhat context-specific)
-  * [[Master's program]] ([[http://youtu.be/VW5GJM4XaNs|promotional video]] from [[http://ic.epfl.ch/computer-science/prospective-students|this page]])
+  * [[Master's program]] ([[https://youtu.be/VW5GJM4XaNs|promotional video]] from [[http://ic.epfl.ch/computer-science/prospective-students|this page]])
   * [[EPFL internships]]
   * [[Exchanges for EPFL students]]
@@ Line 373: / Line 455: @@
 {{lara.jpg|LARA Research Staff, 2009}}
+===== Some Videos =====
-----
+  * [[https://tube.switch.ch/videos/166c6218|Solver-Aided Programming for All]] by [[https://homes.cs.washington.edu/~emina/|Emina Torlak]]
+  * [[https://tube.switch.ch/videos/e19471be|Verified Functional Programming]] by [[https://people.epfl.ch/nicolas.voirol|Nicolas Voirol]]
+  * [[https://tube.switch.ch/videos/bde7255e|Complete Program Synthesis for Linear Arithmetics]] by [[https://people.epfl.ch/mikael.mayer|Mikael Mayer]]
+  * [[https://tube.switch.ch/videos/dd5e03cb|Induction for SMT Solvers]] by [[https://people.epfl.ch/andrew.reynolds|Andrew Reynolds]]
+  * [[https://www.youtube.com/watch?v=Av8bo64FrDE|The Huge Threat of Tiny Software Glitches]] by [[https://lara.epfl.ch/~kuncak/|Viktor Kuncak]]
+  * [[https://www.youtube.com/watch?v=20loktdryYM|Basics of Program Verification]] by [[https://lara.epfl.ch/~kuncak/|Viktor Kuncak]]
+  * [[https://www.youtube.com/watch?v=j2m5YMnHvQQ|Abstract Interpretation for Program Verification]] by [[https://lara.epfl.ch/~kuncak/|Viktor Kuncak]]
+  * [[https://www.youtube.com/watch?v=tvtAyZlhtlM|Deep Learning for Math]] by [[https://people.epfl.ch/romain.edelmann|Romain Edelmann]]
+  * [[https://www.youtube.com/watch?v=0aPZq6VC2fk|Leon Synthesis Demo]] by [[https://people.epfl.ch/etienne.kneuss|Etienne Kneuss]]
+  * [[https://www.youtube.com/watch?v=JFbx4iryNb0|Program verification with Leon]] by [[https://people.epfl.ch/regis.blanc|Regis Blanc]]
+  * [[https://www.youtube.com/watch?v=93vZAmLyOQY|anyCode - Java Assistance Tool]] by [[https://people.epfl.ch/188355|Tihomir Gvero]]
+  * Scala Days 2017 Keynote: [[https://www.youtube.com/watch?v=d4VeFa0z_Lo|Tools for Verified Scala]] by [[https://lara.epfl.ch/~kuncak/|Viktor Kuncak]]
+  * [[http://video.itu.dk/video/10044793/icalp-2014-viktor-kuncak|Verifying and Synthesizing Software with Recursive Functions]] by [[https://lara.epfl.ch/~kuncak/|Viktor Kuncak]]
+  * [[https://www.youtube.com/watch?v=oLrSRvUTJzM|Cleaner Code with less
+Coding]] by [[https://people.epfl.ch/mikael.mayer|Mikael Mayer]]
+---