Campus Event Calendar
Event Entry
What and Who
"Encodings of Bounded LTL Model Checking in EffectivelyPropositional Logic"
Juan Navarro Perez
University of Manchester
SWS Colloquium
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
Thursday, 20 December 2007
14:00
60 Minutes
E1 5
rotunda 6th floor
Saarbrücken
Abstract
We present an encoding that is able to specify LTL bounded model
checking problems within the Bernays-Schönfinkel fragment of
first-order logic. This fragment, which also corresponds to the
category of effectively propositional problems (EPR) of the CASC
system competitions, allows a natural and succinct representation of
both a software/hardware system and the property that one wants to
verify.
This is part of the research I did during my PhD studies at the
University of Manchester, which deals with finding problems suitable
for encoding within the effectively propositional class of formulas, and
aims to encourage the interest on theorem proving in this restricted
fragment of first order logic.
Contact
Brigitta Hansen
0681 - 9325200
--email hidden
passcode not visible
logged in users only
Brigitta Hansen, 12/18/2007 12:46 -- Created document.