ENTCS
2007
13 years 4 months ago
2007
We propose to use a formal specification language as a high-level hardware description language. Formal languages allow for compact, unambiguous representations and yield designs...
ENTCS
2007
13 years 4 months ago
2007
ENTCS
2007
13 years 4 months ago
2007
ENTCS
2007
13 years 4 months ago
2007
Many modern program verifiers translate the program to be verified and its specification into a simple intermediate representation and then compute verification conditions on ...
ENTCS
2007
13 years 4 months ago
2007
In this paper, we present a term rewriting based library for manipulating Java bytecode. We define a mapping from bytecode programs to algebraic terms, and we use Tom, an extensi...
ENTCS
2007
13 years 4 months ago
2007
We give a uniform type-systematic account of a number of optimizations and the underlying analyses for a bytecode-like stack-based low-level language, including analysis soundness...
ENTCS
2007
13 years 4 months ago
2007
We present a powerful and flexible method for automatically checking the secrecy of values inside components. In our framework an attacker may monitor the external communication ...
ENTCS
2007
13 years 4 months ago
2007
ENTCS
2007
13 years 4 months ago
2007
Several model-checker based methods to automated test-case generation have been proposed recently. The performance and applicability largely depends on the complexity of the model...
ENTCS
2007
13 years 4 months ago
2007
We address the problem of verifying planning domains as used in model-based planning, for example in space missions. We propose a methodology for testing flight rules of planning...