ENTCS
2007
13 years 4 months ago
2007
We present a method for pipeline verification using SMT solvers. It is based on a non-deterministic “mother pipeline” machine (MOP) that abstracts the instruction set archite...
ENTCS
2007
13 years 4 months ago
2007
ENTCS
2007
13 years 4 months ago
2007
Automated deduction methods should be specified not procedurally, but declaratively, as inference systems which are proved correct regardless of implementation details. Then, di...
ENTCS
2007
13 years 4 months ago
2007
ENTCS
2007
13 years 4 months ago
2007
The use of typed intermediate languages can significantly increase the reliability of a compiler. By typechecking the code produced at each transformation stage, one can identify...
ENTCS
2007
13 years 4 months ago
2007
In the constructive setting, membership predicates over recursive types are inhabited by terms indexing the elements that satisfy the criteria for membership. In this paper, we mo...
ENTCS
2007
13 years 4 months ago
2007
Transient faults that arise in large-scale software systems can often be repaired by re-executing the code in which they occur. Ascribing a meaningful semantics for safe re-execut...
ENTCS
2007
13 years 4 months ago
2007
The rewrite-based approach to satisfiability modulo theories consists of using generic theorem-proving strategies for first-order logic with equality. If one can prove that an i...
ENTCS
2007
13 years 4 months ago
2007
In this paper we introduce the notion of approximate implementations for Probabilistic I/O Automata (PIOA) and develop methods for proving such relationships. We employ a task str...