CADE
2007
Springer
14 years 12 months ago
2007
Springer
CADE
2007
Springer
14 years 12 months ago
2007
Springer
Abstract. The verification of device drivers is essential for the pervasive verification of an operating system. To show the correctness of device drivers, devices have to be forma...
CADE
2007
Springer
14 years 12 months ago
2007
Springer
Abstract. Hoare logic is widely used for software specification and verification. Frequently we need to prove the total correctness of a program: to prove that the program not only...
CADE
2007
Springer
14 years 12 months ago
2007
Springer
MaLARea (a Machine Learner for Automated Reasoning) is a simple metasystem iteratively combining deductive Automated Reasoning tools (now the E and the SPASS ATP systems) with a m...
CADE
2007
Springer
14 years 12 months ago
2007
Springer
We present results of our work on using first order theorem proving to reason over a large ontology (the Suggested Upper Merged Ontology ? SUMO), and methods for making SUMO suita...
CADE
2007
Springer
14 years 12 months ago
2007
Springer
We develop a formalization of the Size-Change Principle in Isabelle/HOL and use it to construct formally certified termination proofs for recursive functions automatically.
CADE
2007
Springer
14 years 12 months ago
2007
Springer
This paper combines predictive labeling with dependency pairs and reports on its implementation. Our starting point is the method of proving termination of rewrite systems using se...
CADE
2007
Springer
14 years 12 months ago
2007
Springer
Abstract. It has often been claimed that model checking, special purpose automated deduction or interactive theorem proving are needed for formal program development. Recently, it ...
CADE
2007
Springer
14 years 12 months ago
2007
Springer
We present a multi-context focused sequent calculus whose derivations are in bijective correspondence with normal natural deductions in the propositional fragment of the intuitioni...
CADE
2007
Springer
14 years 12 months ago
2007
Springer
Continuous probability distributions are widely used to mathematically describe random phenomena in engineering and physical sciences. In this paper, we present a methodology that ...