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...
Roderick Bloem, Stefan Galler, Barbara Jobstmann, ...
Many modern program verifiers translate the program to be verified and its specification into a simple intermediate representation and then compute verification conditions on ...
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...
Emilie Balland, Pierre-Etienne Moreau, Antoine Rei...
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...
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 ...
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...
Gordon Fraser, Bernhard K. Aichernig, Franz Wotawa
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...