DSD
2002
IEEE
14 years 5 months ago
2002
IEEE
In this paper we describe a methodology for the formal verification of a DSP chip using the HOL theorem prover. We used an iterative method to specify both the behavioral and stru...
ITS
2004
Springer
14 years 5 months ago
2004
Springer
Abstract. We describe a theorem prover that is used in the Why2Atlas tutoring system for the purposes of evaluating the correctness of a student’s essay and for guiding feedback ...
ICFEM
2005
Springer
14 years 6 months ago
2005
Springer
Abstract. Theorem provers, model checkers, static analyzers, test generators. . . all of these and many other kinds of formal methods tools can contribute to the analysis and devel...
EUC
2005
Springer
14 years 6 months ago
2005
Springer
Algorithms that process geometric objects become more and more important for many safety-critical embedded systems, e.g. for motion planning or collision detection, where correctne...
TPHOL
2005
IEEE
14 years 6 months ago
2005
IEEE
Abstract. We present a set of problems that may support the development of calculi and theorem provers for classical higher-order logic. We propose to employ these test problems as...
TPHOL
2005
IEEE
14 years 6 months ago
2005
IEEE
We show that delaying fully-expansive proof reconstruction for non-interactive decision procedures can result in a more efficient workflow. In contrast with earlier work, our appr...
SARA
2007
Springer
14 years 6 months ago
2007
Springer
Relational databases have had great industrial success in computer science, their power evidenced by theoretical analysis and widespread adoption. Often, automated theorem provers...
TPHOL
2007
IEEE
14 years 6 months ago
2007
IEEE
Abstract. We use the theorem prover Isabelle to formalise and machinecheck results of the theory of generalised substitutions given by Dunne and used in the B method. We describe t...
CADE
2001
Springer
15 years 23 days ago
2001
Springer
The STRIP system is a theorem prover for intuitionistic propositional logic with two main characteristics: it deals with the duplication of formulae during proof-search from a fine...
CC
2009
Springer
15 years 1 months ago
2009
Springer
This paper presents a compiler which produces machine code from functions defined in the logic of a theorem prover, and at the same time proves that the generated code executes the...