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

Date, Time and Location

Thursday, 20 December 2007
60 Minutes
E1 5
rotunda 6th floor


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

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.


Brigitta Hansen
0681 - 9325200
--email hidden
passcode not visible
logged in users only

Brigitta Hansen, 12/18/2007 12:46 -- Created document.