Papers
-
Rocket-fast proof checking for SMT solvers,
Proceedings of TACAS 2008. On
using term rewriting as an eficient proof engine.
- Fx7 or In Software, It Is All About Quantifiers,
Satisfiability Modulo Theories Competition 2007, Berlin. Fx7 system description, the solver was
second in the AUFLIA division.
-
Edit
& Verify, with Radu Grigore, First-order Theorem Proving workshop 2007,
Liverpool, UK. During incremental program verification we get many similar
formulas, that need to be proven. We show how to simplify the new ones with
respect to the old ones, that are already proven.
- Reachability
Analysis for Annotated Code, with Mikolas Janota and Radu Grigore,
Specification and Verification of Component-Based Systems, 2007, Cavtat, Croatia.
On smoke-testing soundness of assumptions in program annotations.
-
E-Matching for Fun and Profit,
with Jakub Łopuszański and Joseph R. Kiniry,
Satisfiability Modulo Theories workshop 2007, Berlin.
Special SMT 2007 ENTCS issue. E-matching is used in
quantifier instantiation in SMT solvers.
-
Fx7 Technical report (kind of outdated).
- Type Inference with Deferral -- MSc thesis, about type inference for nominal
type systems with subtyping, parametric polymorphism and overloading. Submitted on June 27th, 2005.
