LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
Last revision Both sides next revision
start [2018/10/21 16:23]
vkuncak
start [2022/08/31 09:34]
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 to help 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 ===== ===== Scientific Staff =====
  
Line 12: Line 34:
 <tr> <tr>
 <td align="​center"​ valign="​bottom">​ <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' ​ width='​160' ​
-alt="​Viktor ​Kuncak">+alt="​Viktor ​Kunčak">
 </a> </a>
 <br> <br>
-<a href="http://icwww.epfl.ch/​~kuncak">​Viktor ​Kuncak</a>+<a href="https://lara.epfl.ch/​~kuncak">​Viktor ​Kunčak</a>
 </td> </td>
 +
 +<td align="​center"​ valign="​bottom">​
 +<a href="​https://​people.epfl.ch/​mario.bucev/">​
 +<img src="​https://​people.epfl.ch/​private/​common/​photos/​links/​247537.jpg"​ width='​160' ​
 +alt="​Mario Bucev">​
 +</a>
 +<br>
 +<a href="​https://​people.epfl.ch/​mario.bucev/">​Mario Bucev</​a>​
 +</td>
 +
 +<td align="​center"​ valign="​bottom">​
 +<a href="​https://​people.epfl.ch/​sankalp.gambhir">​
 +<img src="​https://​lara.epfl.ch/​~kuncak/​staff/​somebody.png"​ width='​160' ​
 +alt="​Sankalp Gambhir">​
 +</a>
 +<br>
 +<a href="​https://​people.epfl.ch/​sankalp.gambhir">​Sankalp Gambhir</​a>​
 +</td>
 +
 +
 </tr> </tr>
  
 <tr> <tr>
 <td align="​center"​ valign="​bottom">​ <td align="​center"​ valign="​bottom">​
-<a href="http://lara.epfl.ch/~pavlogia/">​ +<a href="https://people.epfl.ch/dragana.milovancevic">​ 
-<img src="http://lara.epfl.ch/~pavlogia/profile.jpg" ​ +<img src="https://people.epfl.ch/private/common/​photos/​links/​289485.jpg?​ts=1612961306" width='​160'​ 
-width='​160'​  +alt="Dragana Milovancevic">
-alt="Andreas Pavlogiannis">+
 </a> </a>
 <br> <br>
-<a href="http://lara.epfl.ch/~pavlogia/">Andreas Pavlogiannis</a>+<a href="https://people.epfl.ch/dragana.milovancevic">​Dragana Milovancevic<​/a> 
 +</​td>​ 
 +<td align="​center"​ valign="​bottom">​ 
 +<a href="​https://​people.epfl.ch/​simon.guilloud">​ 
 +<img src="​https://​people.epfl.ch/​private/​common/​photos/​links/​250109.jpg?​ts=1612961599"​ width='​160'​ 
 +alt="​Simon Guilloud">​ 
 +</​a>​ 
 +<​br>​ 
 +<a href="​https://​people.epfl.ch/​simon.guilloud">Simon Guilloud</a>
 </td> </td>
  
 +<td align="​center"​ valign="​bottom">​
 +<a href="​https://​dblp.org/​pid/​257/​8380.html">​
 +<img src="​http://​lara.epfl.ch/​~kuncak/​staff/​rodrigo.jpg"​ width='​160' ​
 +alt="​Rodrigo Raya"></​a>​
 +<br>
 +<a href="​https://​people.epfl.ch/​rodrigo.raya">​Rodrigo Raya</​a>​
 +</td>
 +</tr>
 +
 +</​table>​
 +</​html>​
 +
 +See also [[http://​people.epfl.ch/​cgi-bin/​people?​id=177241&​op=teaching_phd&​lang=en&​cvlang=en|the official list of past and current PhD students]] and [[http://​search.epfl.ch/​ubrowse.action?​acro=LARA|automatically generated administrative page of the group]].
 +
 +===== Support =====
 +
 +<​html>​
 +<table width="​50%"​ align="​top">​
 +<tr>
  
 <td align="​center"​ valign="​top">​ <td align="​center"​ valign="​top">​
-<a href="http://​people.epfl.ch/​jad.hamza">​ +<a href="https://​people.epfl.ch/​fabien.salvi">​ 
-<img src="http://​lara.epfl.ch/​~kuncak/​staff/​jad.jpg"  +<img src="https://​lara.epfl.ch/​~kuncak/​staff/​fabien.jpg"  
-width='​160'​ alt="Jad Hamza"/>+width='​160'​ alt="Fabien Salvi"/>
 </a> </a>
 <br> <br>
-<a href="http://​people.epfl.ch/​jad.hamza">Jad Hamza</a>+System Manager <​br>​ 
 +<a href="https://​people.epfl.ch/​fabien.salvi">Fabien Salvi</a>
 <br> <br>
 </td> </td>
  
-<td align="​center"​ valign="​bottom">​ +<td align="​center"​ valign="​top">​ 
-<a href="​https://​people.epfl.ch/​georg.schmid">​ +<a href="​https://​people.epfl.ch/​sylvie.buchard">​ 
-<img src="http://lara.epfl.ch/~kuncak/staff/georg.jpg" width='​160'​ +<img src="https://people.epfl.ch/private/common/photos/​links/​266882.jpg?​ts=1639433244" ​ 
-alt="Georg S. Schmid">+width='​160'​ alt="Sylvie Buchard"/>
 </a> </a>
 <br> <br>
-<a href="​https://​people.epfl.ch/​georg.schmid">Georg S. Schmid</a>+Secretary <​br>​ 
 +<a href="​https://​people.epfl.ch/​sylvie.buchard">Sylvie Buchard</a
 +<br>
 </td> </td>
  
 </tr> </tr>
 +</​table>​
  
 +</​html>​
 +
 +===== Academic Alumni =====
 +
 +<​html>​
 +<table width="​50%"​ align="​top">​
 <tr> <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">​ <td align="​center"​ valign="​bottom">​
-<a href="https://​people.epfl.ch/​romain.edelmann"> +<a href="​https://​dblp.org/pid/198/4641.html">​ 
-<img src="http://​lara.epfl.ch/​~kuncak/​staff/​romain.jpg" +<img src="https://​lara.epfl.ch/​~kuncak/​staff/​georg.jpg" width='​160'​ 
-width='​160'​ alt="Romain Edelmann"/>+alt="Georg S. Schmid">
 </a> </a>
 <br> <br>
-<a href="https://people.epfl.ch/​​romain.edelmann">Romain Edelmann</a>+<a href="​https://​people.epfl.ch/​georg.schmid">Georg S. Schmid</a>
 </td> </td>
  
 +
 +</tr>
 +
 +<tr>
 <td align="​center"​ valign="​bottom">​ <td align="​center"​ valign="​bottom">​
-<a href="http://people.epfl.ch/nicolas.voirol">​ +<a href="https://cs.au.dk/​~pavlogiannis/">​ 
-<img src="http://​lara.epfl.ch/​~kuncak/​staff/​nicolas.jpg"  +<img src="https://​lara.epfl.ch/​~kuncak/​staff/​AndreasPavlogiannis.jpg"  
-width='​160'​ alt="Nicolas Voirol"/>+width='​160' ​ 
 +alt="Andreas Pavlogiannis">
 </a> </a>
 <br> <br>
-<a href="​http://​people.epfl.ch/nicolas.voirol">Nicolas Voirol</a>+<a href="​http://​lara.epfl.ch/~pavlogia/">Andreas Pavlogiannis</a>
 </td> </td>
  
 <td align="​center"​ valign="​bottom">​ <td align="​center"​ valign="​bottom">​
 <a href="​https://​romac.me/">​ <a href="​https://​romac.me/">​
-<img src="http://​lara.epfl.ch/​~kuncak/​staff/​romac.jpg"​ width='​160'​+<img src="https://​lara.epfl.ch/​~kuncak/​staff/​romac.jpg"​ width='​160'​
 alt="​Romain Ruetschi">​ alt="​Romain Ruetschi">​
 </a> </a>
Line 84: Line 183:
 </td> </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>
  
 <tr> <tr>
- +<td align="​center"​ valign="​bottom">​ 
-<td align="​center"​ valign="​top">​ +<a href="https://​people.epfl.ch/​nicolas.voirol">​ 
-<a href="http://​people.epfl.ch/​emmanouil.koukoutos">​ +<img src="https://​lara.epfl.ch/​~kuncak/​staff/​nicolas.jpg"  
-<img src="http://​lara.epfl.ch/​~kuncak/​staff/​manos.jpg"​ +width='​160'​ alt="Nicolas Voirol"/>
-width='​160' height='​200' alt="Emmanouil Koukoutos"/>+
 </a> </a>
 <br> <br>
-<a href="http://​people.epfl.ch/​emmanouil.koukoutos">Manos Koukoutos</a+<a href="https://​people.epfl.ch/​nicolas.voirol">Nicolas Voirol</a>
-<br>+
 </td> </td>
  
 <td align="​center"​ valign="​bottom">​ <td align="​center"​ valign="​bottom">​
 <a href="​https://​people.epfl.ch/​sarah.sallinger">​ <a href="​https://​people.epfl.ch/​sarah.sallinger">​
-<img src="http://​lara.epfl.ch/​~kuncak/​staff/​sarah.jpg"​ width='​160'​+<img src="https://​lara.epfl.ch/​~kuncak/​staff/​sarah.jpg"​ width='​160'​
 alt="​Sarah Sallinger">​ alt="​Sarah Sallinger">​
 </a> </a>
Line 107: Line 212:
 <a href="​https://​people.epfl.ch/​sarah.sallinger">​Sarah Sallinger</​a>​ <a href="​https://​people.epfl.ch/​sarah.sallinger">​Sarah Sallinger</​a>​
 </td> </td>
- 
- 
-</tr> 
- 
-</​table>​ 
-</​html>​ 
- 
-See also [[http://​people.epfl.ch/​cgi-bin/​people?​id=177241&​op=teaching_phd&​lang=en&​cvlang=en|the official list of past and current PhD students]] and [[http://​search.epfl.ch/​ubrowse.action?​acro=LARA|automatically generated administrative page of the group]]. 
- 
-===== Support ===== 
- 
-<​html>​ 
-<table width="​50%"​ align="​top">​ 
-<tr> 
  
 <td align="​center"​ valign="​top">​ <td align="​center"​ valign="​top">​
-<a href="http://​people.epfl.ch/​fabien.salvi">​ +<a href="https://​people.epfl.ch/​emmanouil.koukoutos">​ 
-<img src="http://​lara.epfl.ch/​~kuncak/​staff/​fabien.jpg"  +<img src="https://​lara.epfl.ch/​~kuncak/​staff/​manos.jpg"​ 
-width='​160'​ alt="Fabien Salvi"/>+width='​160' height='​200' alt="Emmanouil Koukoutos"/>
 </a> </a>
 <br> <br>
-System Manager <​br>​ +<a href="https://​people.epfl.ch/​emmanouil.koukoutos">Manos Koukoutos</a>
-<a href="http://​people.epfl.ch/​fabien.salvi">Fabien Salvi</a>+
 <br> <br>
 </td> </td>
  
-<td align="​center"​ valign="​top">​ 
-<a href="​https://​people.epfl.ch/​sylvie.jankow"">​ 
-<img src="​http://​lara.epfl.ch/​~kuncak/​staff/​sylvie.jpg" ​ 
-width='​160'​ alt="​Yvette Gallay"/>​ 
-</a> 
-<br> 
-Secretary <br> 
-<a href="​http://​people.epfl.ch/​sylvie.jankow">​Sylvie Jankow</​a>​ 
-<br> 
-</td> 
  
 </tr> </tr>
-</​table>​ 
- 
-</​html>​ 
- 
-===== Academic Alumni ===== 
- 
-<​html>​ 
-<table width="​50%"​ align="​top">​ 
  
 <tr> <tr>
  
 <td align="​center"​ valign="​top">​ <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=""/>​ width='​160'​ alt=""/>​
 </a> </a>
 <br> <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> <br>
 </td> </td>
  
 <td align="​center"​ valign="​top">​ <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"​ <img src="/​w/​_media/​marco_thumb.jpg"​
 width='​160'​ alt="​Marco Antognini"/>​ width='​160'​ alt="​Marco Antognini"/>​
 </a> </a>
 <br> <br>
-<a href="http://​people.epfl.ch/​Marco Antognini">​Marco Antognini</​a>​+<a href="https://​people.epfl.ch/​Marco Antognini">​Marco Antognini</​a>​
 <br> <br>
 </td> </td>
Line 178: Line 250:
  
 <td align="​center"​ valign="​top">​ <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=""/>​ width='​160'​ alt=""/>​
 </a> </a>
 <br> <br>
-<a href="http://​people.epfl.ch/​mikael.mayer">​Mikael Mayer</​a>​+<a href="https://​people.epfl.ch/​mikael.mayer">​Mikael Mayer</​a>​
 <br> <br>
 </td> </td>
Line 193: Line 265:
  
 <td align="​center"​ valign="​bottom">​ <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=""/>​ width='​160'​ alt=""/>​
 </a> </a>
 <br> <br>
-<a href="http://​people.epfl.ch/​regis.blanc">​Regis Blanc</​a>​+<a href="https://​people.epfl.ch/​regis.blanc">​Regis Blanc</​a>​
 <br> <br>
 </td> </td>
  
 <td align="​center"​ valign="​bottom">​ <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"/>​ width='​160'​ alt="​Etienne Kneuss"/>​
 </a> </a>
 <br> <br>
-<a href="http://​lara.epfl.ch/​~ekneuss/">​Etienne Kneuss</​a>​+<a href="https://​lara.epfl.ch/​~ekneuss/">​Etienne Kneuss</​a>​
 </td> </td>
  
  
 <td align="​center"​ valign="​top">​ <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"/>​ width='​160'​ alt="​Andrew J. Reynolds"/>​
 </a> </a>
 <br> <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> <br>
 </td> </td>
Line 227: Line 299:
  
 <td align="​center"​ valign="​bottom">​ <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"/>​ width='​160'​ alt="​Eva Darulova"/>​
 </a> </a>
 <br> <br>
-<a href="http://lara.epfl.ch/~darulova">​Eva Darulova</​a>​+<a href="https://malyzajko.github.io/">​Eva Darulova</​a>​
 </td> </td>
  
 <td align="​center"​ valign="​bottom">​ <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"/>​ width='​160'​ alt="​Tihomir Gvero"/>​
 </a> </a>
 <br> <br>
-<a href="http://​tihomirg.github.io/">​Tihomir Gvero</​a>​+<a href="https://​tihomirg.github.io/">​Tihomir Gvero</​a>​
 </td> </td>
  
 <td align="​center"​ valign="​top">​ <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"/>​ width='​160'​ alt="​Ivan Kuraj"/>​
 </a> </a>
 <br> <br>
-<a href="http://​people.epfl.ch/​ivan.kuraj">​Ivan Kuraj</​a>​+<a href="https://​people.epfl.ch/​ivan.kuraj">​Ivan Kuraj</​a>​
 <br> <br>
 </td> </td>
Line 259: Line 331:
  
 <td align="​center"​ valign="​top">​ <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"/>​ width='​160'​ alt="​Giuliano Losa"/>​
 </a> </a>
 <br> <br>
-<a href="http://​www.losa.fr/">​Giuliano Losa</​a>​+<a href="https://​www.losa.fr/">​Giuliano Losa</​a>​
 </td> </td>
  
 <td align="​center"​ valign="​top">​ <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"/>​ width='​160'​ alt="​Hossein Hojjat"/>​
 </a> </a>
 <br> <br>
-<a href="http://​www.cs.cornell.edu/​~hojjat/">​Hossein Hojjat</​a>​+<a href="https://​www.cs.cornell.edu/​~hojjat/">​Hossein Hojjat</​a>​
 <br> <br>
 </td> </td>
  
 <td align="​center"​ valign="​top">​ <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">​ width='​160'​ alt="​Philippe Suter">​
 </a> </a>
 <br> <br>
-<a href="http://​lara.epfl.ch/​~psuter/">​Philippe Suter</​a>​+<a href="https://​lara.epfl.ch/​~psuter/">​Philippe Suter</​a>​
 </td> </td>
  
Line 291: Line 363:
  
 <td align="​center"​ valign="​top">​ <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=""/>​ width='​160'​ alt=""/>​
 </a> </a>
 <br> <br>
-<a href="http://​people.epfl.ch/​filip.konecny">​Filip Konecny</​a>​+<a href="https://​people.epfl.ch/​filip.konecny">​Filip Konecny</​a>​
 <br> <br>
 </td> </td>
  
 <td align="​center"​ valign="​top">​ <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"/>​ width='​160'​ alt="​Pierre-Emmanuel Cornilleau"/>​
 </a> </a>
 <br> <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>
  
 <td align="​center"​ valign="​top">​ <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"/>​ width='​160'​ alt="​Andrej Spielmann"/>​
 </a> </a>
Line 323: Line 395:
 <tr> <tr>
 <td align="​center"​ valign="​top">​ <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"/>​ width='​160'​ alt="​Ruzica Piskac"/>​
 </a> </a>
 <br> <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>
  
 <td align="​center"​ valign="​top">​ <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"/>​ width='​160'​ alt="​Swen Jacobs"/>​
 </a> </a>
 <br> <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>
  
 <td align="​center"​ valign="​top">​ <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"/>​ width='​160'​ alt="​Ali Sinan Köksal"/>​
 </a> </a>
Line 361: Line 433:
 Information on joining and collaborating with LARA: Information on joining and collaborating with LARA:
   * [[https://​issuu.com/​iccommunication/​docs/​ic-at-a-glance-d__pliant-prod-18-07|About IC]]   * [[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   * [[PhD Positions]] and information about EPFL
     * {{phdseminar09.pdf|Slides from a Seminar for Starting PhD Students}} (September 2009, somewhat context-specific)     * {{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]]   * [[EPFL internships]]
   * [[Exchanges for EPFL students]]   * [[Exchanges for EPFL students]]
Line 383: Line 455:
 {{lara.jpg|LARA Research Staff, 2009}} {{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]] 
 +---