Sciweavers

ENTCS
2007
130views more  ENTCS 2007»
14 years 12 days ago
Specify, Compile, Run: Hardware from PSL
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, ...
ENTCS
2007
85views more  ENTCS 2007»
14 years 12 days ago
On-the-Fly Data Flow Analysis Based on Verification Technology
María-del-Mar Gallardo, Christophe Joubert,...
ENTCS
2007
85views more  ENTCS 2007»
14 years 12 days ago
Towards Software Component Procurement Automation with Latent Semantic Analysis
Hans-Gerhard Groß, Marco Lormans, Jun Zhou
ENTCS
2007
107views more  ENTCS 2007»
14 years 12 days ago
Formal Translation of Bytecode into BoogiePL
Many modern program verifiers translate the program to be verified and its specification into a simple intermediate representation and then compute verification conditions on ...
Hermann Lehner, Peter Müller
ENTCS
2007
168views more  ENTCS 2007»
14 years 12 days ago
Bytecode Rewriting in Tom
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...
ENTCS
2007
98views more  ENTCS 2007»
14 years 12 days ago
Type Systems for Optimizing Stack-based Code
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...
Ando Saabas, Tarmo Uustalu
ENTCS
2007
88views more  ENTCS 2007»
14 years 12 days ago
Keeping Secrets in Resource Aware Components
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 ...
Tom Chothia, Jun Pang, Muhammad Torabi Dashti
ENTCS
2007
116views more  ENTCS 2007»
14 years 12 days ago
Handling Model Changes: Regression Testing and Test-Suite Update with Model-Checkers
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
ENTCS
2007
75views more  ENTCS 2007»
14 years 12 days ago
Testing Planning Domains (without Model Checkers)
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...
Franco Raimondi, Charles Pecheur, Guillaume Brat