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
Next revision Both sides next revision
start [2019/08/09 10:26]
fabien [Scientific Staff]
start [2022/08/31 09:26]
vkuncak [Scientific Staff]
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 15: Line 37:
 <img src="​https://​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="​https://​icwww.epfl.ch/​~kuncak">​Viktor ​Kuncak</a>+<a href="​https://​lara.epfl.ch/​~kuncak">​Viktor ​Kunčak</a>
 </td> </td>
-</tr> 
- 
-<tr> 
-<td align="​center"​ valign="​bottom">​ 
-<a href="​https://​lara.epfl.ch/​~pavlogia/">​ 
-<img src="​https://​lara.epfl.ch/​~pavlogia/​profile.jpg" ​ 
-width='​160' ​ 
-alt="​Andreas Pavlogiannis">​ 
-</a> 
-<br> 
-<a href="​http://​lara.epfl.ch/​~pavlogia/">​Andreas Pavlogiannis</​a>​ 
-</td> 
- 
- 
-<td align="​center"​ valign="​top">​ 
-<a href="​https://​people.epfl.ch/​jad.hamza">​ 
-<img src="​https://​lara.epfl.ch/​~kuncak/​staff/​jad.jpg" ​ 
-width='​160'​ alt="​Jad Hamza"/>​ 
-</a> 
-<br> 
-<a href="​https://​people.epfl.ch/​jad.hamza">​Jad Hamza</​a>​ 
-<br> 
-</td> 
- 
 <td align="​center"​ valign="​bottom">​ <td align="​center"​ valign="​bottom">​
-<a href="​https://​people.epfl.ch/georg.schmid">+<a href="​https://​dblp.org/pid/198/4641.html">
 <img src="​https://​lara.epfl.ch/​~kuncak/​staff/​georg.jpg"​ width='​160'​ <img src="​https://​lara.epfl.ch/​~kuncak/​staff/​georg.jpg"​ width='​160'​
 alt="​Georg S. Schmid">​ alt="​Georg S. Schmid">​
Line 52: Line 50:
 <a href="​https://​people.epfl.ch/​georg.schmid">​Georg S. Schmid</​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="https://people.epfl.ch/​​romain.edelmann"> +<a href="​https://​people.epfl.ch/​mario.bucev/">​ 
-<img src="​https://​lara.epfl.ch/~kuncak/staff/romain.jpg" +<img src="​https://​people.epfl.ch/private/common/photos/​links/​247537.jpg" width='​160' ​ 
-width='​160'​ alt="Romain Edelmann"/>+alt="Mario Bucev">
 </a> </a>
 <br> <br>
-<a href="https://people.epfl.ch/​​romain.edelmann">Romain Edelmann</a>+<a href="​https://​people.epfl.ch/​mario.bucev/">Mario Bucev</a>
 </td> </td>
  
  
 +
 +</tr>
 +
 +<tr>
 <td align="​center"​ valign="​bottom">​ <td align="​center"​ valign="​bottom">​
-<a href="​https://​romac.me/">​ +<a href="​https://​people.epfl.ch/dragana.milovancevic">​ 
-<img src="​https://​lara.epfl.ch/~kuncak/staff/romac.jpg" width='​160'​ +<img src="​https://​people.epfl.ch/private/common/photos/​links/​289485.jpg?​ts=1612961306" width='​160'​ 
-alt="Romain Ruetschi">+alt="Dragana Milovancevic">
 </a> </a>
 <br> <br>
-<a href="​https://​romac.me/">Romain Ruetschi</a>+<a href="​https://​people.epfl.ch/dragana.milovancevic">Dragana Milovancevic</a>
 </td> </td>
- 
 <td align="​center"​ valign="​bottom">​ <td align="​center"​ valign="​bottom">​
-<a href="​https://​people.epfl.ch/​nataliia.stulova?​lang=en">​ +<a href="​https://​people.epfl.ch/​simon.guilloud">​ 
-<img src="​https://​lara.epfl.ch/w/_media/stulova.jpg" width='​160'​ +<img src="​https://​people.epfl.ch/private/common/photos/​links/​250109.jpg?​ts=1612961599" width='​160'​ 
-alt="Nataliia Stulova">+alt="Simon Guilloud">
 </a> </a>
 <br> <br>
-<a href="​https://​people.epfl.ch/​nataliia.stulova?​lang=en">Nataliia Stulova</a>+<a href="​https://​people.epfl.ch/​simon.guilloud">Simon Guilloud</a>
 </td> </td>
- 
- 
- 
-</tr> 
- 
-<tr> 
- 
  
 <td align="​center"​ valign="​bottom">​ <td align="​center"​ valign="​bottom">​
-<a href="​https://​people.epfl.ch/sarah.sallinger">​ +<a href="​https://​dblp.org/pid/257/8380.html">​ 
-<img src="https://​lara.epfl.ch/​~kuncak/​staff/​sarah.jpg" width='​160'​ +<img src="http://​lara.epfl.ch/​~kuncak/​staff/​rodrigo.jpg" width='​160'​  
-alt="Sarah Sallinger"> +alt="Rodrigo Raya"></​a>​
-</a>+
 <br> <br>
-<a href="​https://​people.epfl.ch/​sarah.sallinger">Sarah Sallinger</a>+<a href="​https://​people.epfl.ch/​rodrigo.raya">Rodrigo Raya</a>
 </td> </td>
- 
- 
 </tr> </tr>
  
Line 127: Line 114:
  
 <td align="​center"​ valign="​top">​ <td align="​center"​ valign="​top">​
-<a href="​https://​people.epfl.ch/​sylvie.jankow"​">​ +<a href="​https://​people.epfl.ch/​sylvie.buchard">​ 
-<img src="​https://​lara.epfl.ch/~kuncak/staff/sylvie.jpg"  +<img src="​https://​people.epfl.ch/private/common/photos/​links/​266882.jpg?​ts=1639433244"  
-width='​160'​ alt="​Sylvie ​Jankow"/>+width='​160'​ alt="​Sylvie ​Buchard"/>
 </a> </a>
 <br> <br>
 Secretary <br> Secretary <br>
-<a href="​https://​people.epfl.ch/​sylvie.jankow">​Sylvie ​Jankow</a>+<a href="​https://​people.epfl.ch/​sylvie.buchard">​Sylvie ​Buchard</a>
 <br> <br>
 </td> </td>
Line 146: Line 133:
 <​html>​ <​html>​
 <table width="​50%"​ align="​top">​ <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>
  
 +</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> <tr>
Line 156: Line 192:
 <br> <br>
 <a href="​https://​people.epfl.ch/​nicolas.voirol">​Nicolas Voirol</​a>​ <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>
  
Line 244: Line 289:
  
 <td align="​center"​ valign="​bottom">​ <td align="​center"​ valign="​bottom">​
-<a href="​https://​people.epfl.ch/eva.darulova">+<a href="​https://​malyzajko.github.io/">
 <img src="​https://​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="​https://​lara.epfl.ch/~darulova">​Eva Darulova</​a>​+<a href="​https://​malyzajko.github.io/">​Eva Darulova</​a>​
 </td> </td>
  
Line 340: Line 385:
 <tr> <tr>
 <td align="​center"​ valign="​top">​ <td align="​center"​ valign="​top">​
-<a href="https://www.mpi-sws.org/~piskac/">​+<a href="http://www.cs.yale.edu/​homes/​piskac/">​
 <img src="​https://​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="https://www.mpi-sws.org/~piskac/">​Ruzica Piskac</​a>​ <br>+<a href="http://www.cs.yale.edu/​homes/​piskac/">​Ruzica Piskac</​a>​ <br>
 (<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>​) (<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>
Line 400: Line 445:
 {{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]] 
 +---