Campus Event Calendar
Event Entry
What and Who
Avacs Virtuel Seminar"Computation of Minimal Counterexamples by Using Black BoxTechniques and Symbolic Methods"
Tobias Nopper
Miscellaneous
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 11 May 2007
13:30
-- Not specified --
E1 4
007
Saarbrücken
Abstract
Computing counterexamples is a crucial task for error diagnosis and
debugging of sequential systems. If an implementation does not fulfill
its specification, counterexamples are used to explain the error effect
to the designer. In order to be understood by the designer,
counterexamples should be simple, i.e. they should be as general as
possible and assign values to a minimal number of input signals.
Here we use the concept of `Black Boxes' -- parts of the design with
unknown behavior -- to mask out components for counterexample
computation. By doing so, the resulting counterexample will argue about
a reduced number of components in the system to facilitate the task of
understanding and correcting the error. We introduce the notion of
`uniform counterexamples' to provide an exact formalization of
simplified counterexamples arguing only about components which were not
masked out. Our computation of counterexamples is based on symbolic
methods using AIGs (And-Inverter-Graphs). Experimental results using a
VLIW processor as a case study clearly demonstrate our capability of
providing simplified counterexamples.
debugging of sequential systems. If an implementation does not fulfill
its specification, counterexamples are used to explain the error effect
to the designer. In order to be understood by the designer,
counterexamples should be simple, i.e. they should be as general as
possible and assign values to a minimal number of input signals.
Here we use the concept of `Black Boxes' -- parts of the design with
unknown behavior -- to mask out components for counterexample
computation. By doing so, the resulting counterexample will argue about
a reduced number of components in the system to facilitate the task of
understanding and correcting the error. We introduce the notion of
`uniform counterexamples' to provide an exact formalization of
simplified counterexamples arguing only about components which were not
masked out. Our computation of counterexamples is based on symbolic
methods using AIGs (And-Inverter-Graphs). Experimental results using a
VLIW processor as a case study clearly demonstrate our capability of
providing simplified counterexamples.
Contact
Roxane Wetzel
-900
--email hidden
passcode not visible
logged in users only
Roxane Wetzel, 05/10/2007 11:11
Roxane Wetzel, 05/10/2007 11:08 -- Created document.
Roxane Wetzel, 05/10/2007 11:08 -- Created document.