Sciweavers

MEMOCODE
2010
IEEE
13 years 9 months ago
LTSs for translation validation of (multi-clocked) SIGNAL specifications
Design of critical embedded systems demands for guarantees on the reliability of the implementation/compilation of a specification. In general, this guarantee takes either the form...
Julio C. Peralta, Thierry Gautier, Loïc Besna...
MEMOCODE
2010
IEEE
13 years 9 months ago
A formal executable semantics of Verilog
This paper describes a formal executable semantics for the Verilog hardware description language. The goal of our formalization is to provide a concise and mathematically rigorous...
Patrick O'Neil Meredith, Michael Katelman, Jos&eac...
MEMOCODE
2010
IEEE
13 years 9 months ago
A flexible schema for generating explanations in lazy theory propagation
Abstract--Theory propagation in Satisfiability Modulo Theories is crucial for the solver's performance. It is important, however, to pay particular care to the amount of deduc...
Roberto Bruttomesso, Edgar Pek, Natasha Sharygina