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/09 10:26]
fabien [Scientific Staff]
start [2022/08/31 09:34]
vkuncak
Line 1: Line 1:
 +<​html>​
 +<​style>​
 +p {
 +   ​font-size:​ 24px !important;
 +}
 +</​style>​
 +
 +<p>
 +<​strong>​
 +Helping construct software that does what we expect
 +</​strong>​
 +</p>
  
-===== MissionHelp people construct software that does what they expect =====+<​p>​(<​a href="https://​epfl-lara.github.io/">​Click here for simpler version of this page on GitHub</​a>​)</​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 ​+<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">​ <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 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>
  
 <td align="​center"​ valign="​bottom">​ <td align="​center"​ valign="​bottom">​
-<a href="​https://​people.epfl.ch/​georg.schmid">​ +<a href="​https://​people.epfl.ch/​sankalp.gambhir">​ 
-<img src="​https://​lara.epfl.ch/​~kuncak/​staff/​georg.jpg" width='​160'​ +<img src="​https://​lara.epfl.ch/​~kuncak/​staff/​somebody.png" width='​160'​  
-alt="Georg S. Schmid">+alt="Sankalp Gambhir">
 </a> </a>
 <br> <br>
-<a href="​https://​people.epfl.ch/​georg.schmid">Georg S. Schmid</a>+<a href="​https://​people.epfl.ch/​sankalp.gambhir">Sankalp Gambhir</a>
 </td> </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 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>
  
 +<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 156: 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 244: 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 340: 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 400: 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]] 
 +---