peter-Unpublished.bib

@comment{{This file has been generated by bib2bib 1.95}}

@comment{{Command line: bib2bib -c annote:"unpublished" -ob peter-Unpublished.bib -oc peter-Unpublished.cite peter.bib}}

@unpublished{Bauer:etal:reasoning-BP:draft,
  author = {Andreas Bauer and Peter Baumgartner and Michael Norrish},
  title = {Reasoning with Data-Centric Business Processes},
  note = {Draft},
  optkey = {},
  optmonth = {},
  optyear = {},
  optannote = {},
  url = {reasoning-BP-draft.pdf},
  abstract = {We describe an approach to modelling and reasoning about
    data-centric business processes and present a form of general
    model checking.  Our technique extends existing approaches, which
    explore systems only from concrete initial states.
    \par
    Specifically, we model business processes in terms of smaller
    fragments, whose possible interactions are constrained by
    first-order logic formulae.  In turn, process fragments are
    connected graphs annotated with instructions to modify data.
    Correctness properties concerning the evolution of data with
    respect to processes can be stated in a first-order
    branching-time logic over built-in theories, such as linear
    integer arithmetic, records and arrays.
    \par
    Solving general model checking problems over this logic is
    considerably harder than model checking when a concrete initial
    state is given.  To this end, we present a tableau procedure that
    reduces these model checking problems to first-order logic over
    arithmetic. The resulting proof obligations are passed on to
    appropriate ``off-the-shelf'' theorem provers.  We also detail our
    modelling approach, describe the reasoning components and report
    on first experiments.},
  annote = unpublished
}

@unpublished{Baumgartner:MEV3:draft,
  author = {Peter Baumgartner},
  title = {Model Evolution With Built-in Theories -- Version 3},
  note = {Draft},
  optkey = {},
  optmonth = {},
  optyear = {},
  optannote = {},
  url = {MEV3-draft.pdf},
  abstract = {Model Evolution is a lifted version of the propositional DPLL
  procedure for first-order logic with equality. This paper combines and extends
  the essentials of the latest Model Evolution variants with and without theory reasoning into a new
  calculus. The new calculus is described in detail. The main results reported here
  are the calculus'  completeness under (unavoidable) conditions, and its application
  as a decison procedure for the quantifier-free fragment of the  
  combined theory of free function symbols with equality and linear integer
  arithmetic.},
  annote = unpublished
}