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 [2019/08/14 17:56]
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 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>​(<​href="​https://epfl-lara.github.io/">​Click here for simpler version ​of this page on GitHub</a>)</p>
  
-Our goal is to enable people to easily program ​and construct reliable and sophisticated ​systems. ​+<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>​
  
 ===== Scientific Staff ===== ===== Scientific Staff =====
Line 16: 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">​ <td align="​center"​ valign="​bottom">​
-<a href="​https://​lara.epfl.ch/~pavlogia/">​ +<a href="​https://​people.epfl.ch/mario.bucev/">​ 
-<img src="​https://​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> </a>
 <br> <br>
-<a href="http://lara.epfl.ch/~pavlogia/">Andreas Pavlogiannis</a>+<a href="https://people.epfl.ch/mario.bucev/">Mario Bucev</a>
 </td> </td>
  
- +<td align="​center"​ valign="​bottom">​ 
-<td align="​center"​ valign="​top">​ +<a href="​https://​people.epfl.ch/​sankalp.gambhir">​ 
-<a href="​https://​people.epfl.ch/​jad.hamza">​ +<img src="​https://​lara.epfl.ch/​~kuncak/​staff/​somebody.png" width='​160' ​ 
-<img src="​https://​lara.epfl.ch/​~kuncak/​staff/​jad.jpg" ​ +alt="Sankalp Gambhir">
-width='​160'​ alt="Jad Hamza"/>+
 </a> </a>
 <br> <br>
-<a href="​https://​people.epfl.ch/​jad.hamza">Jad Hamza</a+<a href="​https://​people.epfl.ch/​sankalp.gambhir">Sankalp Gambhir</a>
-<br>+
 </td> </td>
  
-<td align="​center"​ valign="​bottom">​ 
-<a href="​https://​people.epfl.ch/​georg.schmid">​ 
-<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>
  
 <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/​dragana.milovancevic">​ 
-<img src="​https://​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> </a>
 <br> <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>
- 
- 
 <td align="​center"​ valign="​bottom">​ <td align="​center"​ valign="​bottom">​
-<a href="​https://​romac.me/">​ +<a href="​https://​people.epfl.ch/simon.guilloud">​ 
-<img src="​https://​lara.epfl.ch/~kuncak/staff/romac.jpg" width='​160'​ +<img src="​https://​people.epfl.ch/private/common/photos/​links/​250109.jpg?​ts=1612961599" width='​160'​ 
-alt="Romain Ruetschi">+alt="Simon Guilloud">
 </a> </a>
 <br> <br>
-<a href="​https://​romac.me/">Romain Ruetschi</a>+<a href="​https://​people.epfl.ch/simon.guilloud">Simon Guilloud</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://​dblp.org/pid/​257/​8380.html">​ 
-<img src="https://​lara.epfl.ch/​w/_media/stulova.jpg" width='​160'​ +<img src="http://​lara.epfl.ch/​~kuncak/staff/rodrigo.jpg" width='​160'​  
-alt="Nataliia Stulova"> +alt="Rodrigo Raya"></​a>​
-</a>+
 <br> <br>
-<a href="​https://​people.epfl.ch/​nataliia.stulova?​lang=en">Nataliia Stulova</a>+<a href="​https://​people.epfl.ch/​rodrigo.raya">Rodrigo Raya</a>
 </td> </td>
- 
- 
- 
-</tr> 
- 
-<tr> 
- 
- 
-<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> 
- 
- 
 </tr> </tr>
  
Line 128: 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 147: 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>
  
 +<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> <tr>
Line 157: Line 202:
 <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 245: Line 299:
  
 <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 341: Line 395:
 <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 403: Line 457:
 ===== Some Videos ===== ===== Some Videos =====
  
-  * https://​tube.switch.ch/​videos/​bde7255e +  * [[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/​dd5e03cb +  * [[https://​tube.switch.ch/​videos/​e19471be|Verified Functional Programming]] by [[https://​people.epfl.ch/​nicolas.voirol|Nicolas Voirol]] 
-  * https://​www.youtube.com/​watch?​v=Av8bo64FrDE +  * [[https://​tube.switch.ch/​videos/​bde7255e|Complete Program Synthesis for Linear Arithmetics]] by [[https://​people.epfl.ch/​mikael.mayer|Mikael Mayer]] 
-  * https://​www.youtube.com/​watch?​v=20loktdryYM +  * [[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=j2m5YMnHvQQ +  * [[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=tvtAyZlhtlM +  * [[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=0aPZq6VC2fk +  * [[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=JFbx4iryNb0 +  * [[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=93vZAmLyOQY +  * [[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=d4VeFa0z_Lo +  * [[https://​www.youtube.com/​watch?​v=JFbx4iryNb0|Program verification with Leon]] by [[https://​people.epfl.ch/​regis.blanc|Regis Blanc]] 
-  * http://​video.itu.dk/​video/​10044793/​icalp-2014-viktor-kuncak +  * [[https://​www.youtube.com/​watch?​v=93vZAmLyOQY|anyCode - Java Assistance Tool]] by [[https://​people.epfl.ch/​188355|Tihomir Gvero]] 
-  * https://​www.youtube.com/​watch?​v=oLrSRvUTJzM +  * Scala Days 2017 Keynote: [[https://​www.youtube.com/​watch?​v=d4VeFa0z_Lo|Tools for Verified Scala]] by [[https://​lara.epfl.ch/​~kuncak/​|Viktor Kuncak]] 
-  ​* ​https://www.youtube.com/watch?​v=oLrSRvUTJzM +  * [[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]] 
 +---