[Home] [Teaching] [Research] [Contact]

Projects

• The K Framework
• Symbolic execution framework
• Program verification in K

The K Framework

• Executable semantic framework for defining programming Languages
• Webpage
• Available on Github
• Related papers: FM2012,ENTCS2014,ENTCS2014

[Go to top]

Symbolic execution framework

• A language independent framework for symbolic execution
• Theoretical framework (see my PhD thesis)
• Implementation based on the K framework - version 3.4
• Related papers: SLE2013, WRLA2014,CLSS2015, JLAMP2015

[Go to top]

Program verification in K

• Hoare Logic in K (see SYNASC2013 and my PhD thesis for details)
• Reachability Logic verification using symbolic execution
  • Language-Independent Program Verification Using Symbolic Execution INRIA-HAL RR-8369
  • Verifying Reachability-Logic Properties on Rewriting-Logic Specifications LRC2015
  • Proving Reachability-Logic Formulas Incrementally WRLA2016
  • Formal Proof of Soundness for an RL Prover INRIA-HAL RR-471

[Go to top]