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/14 17:56]
vkuncak
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 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://​dblp.org/pid/198/4641.html">
-<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">​ +
-<a href="​https://​people.epfl.ch/georg.schmid">+
 <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 53: 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 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>
  
 +</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 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 245: 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 341: 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 403: Line 447:
 ===== 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]] 
 +---