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
start [2019/08/14 17:56]
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 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 ​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>​
  
 ===== 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]] 
 +---