| Publication | Date of Publication | Type |
|---|
On ground AC-completion
Rewriting Techniques and Applications | 2022-12-09 | Paper |
AC-complete unification and its application to theorem proving
Rewriting Techniques and Applications | 2022-12-09 | Paper |
A formally proved, complete algorithm for path resolution with symbolic links
| 2019-09-18 | Paper |
Automating the verification of floating-point programs
| 2018-12-07 | Paper |
A formally verified interpreter for a shell-like programming language
| 2018-12-07 | Paper |
How to get an efficient yet verified arbitrary-precision integer library
| 2018-12-07 | Paper |
Instrumenting a weakest precondition calculus for counterexample generation
Journal of Logical and Algebraic Methods in Programming | 2018-06-27 | Paper |
Rewrite systems for natural, integral, and rational arithmetic
Rewriting Techniques and Applications | 2017-11-17 | Paper |
Formal verification of numerical programs: from C annotated programs to mechanical proofs
Mathematics in Computer Science | 2013-05-16 | Paper |
Hardware-Dependent Proofs of Numerical Programs
Certified Programs and Proofs | 2011-11-22 | Paper |
A refinement methodology for object-oriented programs
Formal Verification of Object-Oriented Software | 2011-01-21 | Paper |
Modular inference of subprogram contracts for safety checking
Journal of Symbolic Computation | 2010-11-10 | Paper |
Multi-prover verification of floating-point programs
Automated Reasoning | 2010-09-14 | Paper |
Operational termination of conditional term rewriting systems
Information Processing Letters | 2009-12-04 | Paper |
Proving operational termination of membership equational programs
Higher-Order and Symbolic Computation | 2009-08-04 | Paper |
Towards Modular Algebraic Specifications for Pointer Programs: A Case Study
Rewriting, Computation and Proof | 2009-03-06 | Paper |
Modular and incremental proofs of AC-termination
Journal of Symbolic Computation | 2007-08-24 | Paper |
Mechanically proving termination using polynomial interpretations
Journal of Automated Reasoning | 2006-11-17 | Paper |
Theorem Proving in Higher Order Logics
| 2006-07-06 | Paper |
Algebraic Methodology and Software Technology
Lecture Notes in Computer Science | 2005-08-25 | Paper |
The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
The Journal of Logic and Algebraic Programming | 2004-10-14 | Paper |
scientific article; zbMATH DE number 1615245 (Why is no real title available?)
| 2001-07-08 | Paper |
scientific article; zbMATH DE number 1241628 (Why is no real title available?)
| 1999-06-22 | Paper |
scientific article; zbMATH DE number 1023522 (Why is no real title available?)
| 1997-11-09 | Paper |
Normalized rewriting: An alternative to rewriting modulo a set of equations
Journal of Symbolic Computation | 1997-01-21 | Paper |
Termination and completion modulo associativity, commutativity and identity
Theoretical Computer Science | 1993-01-17 | Paper |
THE WORD PROBLEM OF ACD-GROUND THEORIES IS UNDECIDABLE
International Journal of Foundations of Computer Science | 1993-01-16 | Paper |
An efficient finite element incompressible Navier-Stokes solver that approximates nonlinear terms with finite differences
Finite Elements in Analysis and Design | 1993-01-16 | Paper |
