Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
CADE
2007
Springer
11 years 12 months ago
Efficient E-Matching for SMT Solvers
Leonardo Mendonça de Moura, Nikolaj Bj&osla...
CADE
2007
Springer
11 years 12 months ago
Conservative Extensions in the Lightweight Description Logic EL
We bring together two recent trends in description logic (DL): lightweight DLs in which the subsumption problem is tractable and conservative extensions as a central tool for forma...
Carsten Lutz, Frank Wolter
CADE
2007
Springer
11 years 12 months ago
Labelled Clauses
We add labels to first-order clauses to simultaneously apply superpositions to several proof obligations inside one clause set. From a theoretical perspective, the approach unifies...
Tal Lev-Ami, Christoph Weidenbach, Thomas W. Reps,...
CADE
2007
Springer
11 years 12 months ago
KeY-C: A Tool for Verification of C Programs
Abstract. We present KeY-C, a tool for deductive verification of C programs. KeY-C allows to prove partial correctness of C programs relative to pre- and postconditions. It is base...
Daniel Larsson, Oleg Mürk, Reiner Hähnle
books