CADE
2007
Springer
14 years 4 months ago
2007
Springer
Abstract. Heterogeneous specification becomes more and more important because complex systems are often specified using multiple viewpoints, involving multiple formalisms. Moreover...
CADE
2007
Springer
14 years 7 months ago
2007
Springer
Abstract. Most methods for termination analysis of term rewrite systems (TRSs) essentially try to find arguments of functions that decrease in recursive calls. However, they fail ...
CADE
2007
Springer
14 years 7 months ago
2007
Springer
We develop and implement a novel algorithm for discovering the optimal sets of premisses for proving and disproving conjectures in first-order logic. The algorithm uses interpret...
CADE
2007
Springer
15 years 1 months ago
2007
Springer
CADE
2007
Springer
15 years 1 months ago
2007
Springer
We introduce a calculus for handling integer arithmetic in first-order logic. The method is tailored to Java program verification and meant to be used both as a supporting procedur...
CADE
2007
Springer
15 years 1 months ago
2007
Springer
Fault tolerance mechanisms are a key ingredient of dependable systems. In particular, software-implemented hardware fault tolerance (SIHFT) is gaining in popularity, because of its...
CADE
2007
Springer
15 years 1 months ago
2007
Springer
In this paper we propose a method for inferring invariants for loops in Java programs. An example of a simple while loop is used throughout the paper to explain our approach. The m...
CADE
2007
Springer
15 years 1 months ago
2007
Springer
We show how theorem proving and methods for handling real algebraic constraints can be combined for hybrid system verification. In particular, we highlight the interaction of deduc...
CADE
2007
Springer
15 years 1 months ago
2007
Springer
This paper presents an overview of the verication framework ALICE in its current version 0.7. It is based on the generic theorem prover Isabelle [Pau03a]. Within ALICE a software o...
CADE
2007
Springer
15 years 1 months ago
2007
Springer
Safety and security guarantees for individual applications in general depend on assumptions on the given context provided by distributed instances of operating systems, hardware pl...