Sciweavers

Share
CADE
2007
Springer
9 years 10 months ago
The Heterogeneous Tool Set (Hets)
Abstract. Heterogeneous specification becomes more and more important because complex systems are often specified using multiple viewpoints, involving multiple formalisms. Moreover...
Till Mossakowski, Christian Maeder, Klaus Lüt...
CADE
2007
Springer
10 years 1 months ago
Proving Termination by Bounded Increase
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 ...
Jürgen Giesl, René Thiemann, Stephan S...
CADE
2007
Springer
10 years 1 months ago
Semantic Selection of Premisses for Automated Theorem Proving
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...
Petr Pudlak
CADE
2007
Springer
10 years 7 months ago
A Sequent Calculus for Integer Arithmetic with Counterexample Generation
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...
Philipp Rümmer
CADE
2007
Springer
10 years 7 months ago
Symbolic Fault Injection
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...
Daniel Larsson, Reiner Hähnle
CADE
2007
Springer
10 years 7 months ago
Inferring Invariants by Symbolic Execution
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...
Benjamin Weiß, Peter H. Schmitt
CADE
2007
Springer
10 years 7 months ago
Combining Deduction and Algebraic Constraints for Hybrid System Analysis
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...
André Platzer
CADE
2007
Springer
10 years 7 months ago
ALICE: An Advanced Logic for Interactive Component Engineering
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...
Borislav Gajanovic, Bernhard Rumpe
CADE
2007
Springer
10 years 7 months ago
A History-based Verification of Distributed Applications
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...
Bruno Langenstein, Andreas Nonnengart, Georg Rock,...
books