Campus Event Calendar
Event Entry
What and Who
Bitvector Reasoning with SPASS
Rostislav Rusev
Max-Planck-Institut für Informatik - RG1
Talk
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, 13 June 2008
11:00
30 Minutes
E1 4
Rotunda 6th floor
Saarbrücken
Abstract
Formal verification of hardware is a crucial step when verifying
entire computing systems. In order to prove that a piece of hardware is
doing exactly what it is intended to do, verification on the more abstract
level of bitvector arithmetics is essential. Here we will present a
technique for automated reasoning on problems derived from the domain of
fixed-sized bitvector arithmetics. The first challenge that we will face
is the elaboration of a proper encoding of the bitvector arithmetics
problems into dfg-syntax. The second issue which we will address is to
enhance the performance of SPASS when operating on problems defined
through this specific encoding.
entire computing systems. In order to prove that a piece of hardware is
doing exactly what it is intended to do, verification on the more abstract
level of bitvector arithmetics is essential. Here we will present a
technique for automated reasoning on problems derived from the domain of
fixed-sized bitvector arithmetics. The first challenge that we will face
is the elaboration of a proper encoding of the bitvector arithmetics
problems into dfg-syntax. The second issue which we will address is to
enhance the performance of SPASS when operating on problems defined
through this specific encoding.
Contact
Roxane Wetzel
900
--email hidden
passcode not visible
logged in users only
Roxane Wetzel, 06/09/2008 11:47
Viorica Sofronie-Stokkermans, 04/17/2008 10:58
Viorica Sofronie-Stokkermans, 04/17/2008 10:57 -- Created document.
Viorica Sofronie-Stokkermans, 04/17/2008 10:58
Viorica Sofronie-Stokkermans, 04/17/2008 10:57 -- Created document.