Publications


2017

Format unraveled. Journées Francophones des Langages Applicatifs (JFLA) 2017.

2015

A syntactic soundness proof for free-variable tableaux with on-the-fly Skolemization. CoRR.
SMTpp: preprocessors and analyzers for SMT-LIB. SMT 2015, San Francisco, California, July 18-19, 2015..

2014

LLVM-Based Code Generation for B. SBMF 2014, Maceió, AL, Brazil, September 29-October 1, 2014.
Extending SMT-LIB v2 with \(\lambda\)-Terms and Polymorphism. SMT 2014, Vienna, Austria, July 17-18, 2014.

2011

A Mergeable Interval Map. Stud. Inform. Univ..
Rigorous Evidence of Freedom from Concurrency Faults in Industrial Control Software. SAFECOMP 2011, Naples, Italy, September 19-22, 2011.

2007

Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs. LPAR 2007, Yerevan, Armenia, October 15-19, 2007.

2006

A Semantic Completeness Proof for TaMeD. LPAR 2006, Phnom Penh, Cambodia, November 13-17..
On Constructive Cut Admissibility in Deduction Modulo. TYPES 2006, Nottingham, UK, April 18-21, 2006 --- Revised selected papers.

2004

TaMeD: A Tableau Method for Deduction Modulo. IJCAR 2004, Cork, Ireland, July 4-8, 2004..