@inproceedings{
    Dub:VMCAI10,
    editor = "Barthe, Gilles and Hermenegildo, Manuel",
    author = "Dubrovin, Jori",
    volume = "5944",
    publisher = "Springer",
    onlinenote = "The original publication is available at www.springerlink.com",
    title = "Checking Bounded Reachability in Asynchronous Systems by Symbolic Event Tracing",
    url = "http://dx.doi.org/10.1007/978-3-642-11319-2_13",
    series = "Lecture Notes in Computer Science",
    booktitle = "Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2010)",
    corerank = "B",
    optpdf = "VMCAI2010_cameraready.pdf",
    abstract = "This paper presents a new framework for checking bounded reachability properties of asynchronous systems by reducing the problem to satisfiability in difference logic. The analysis is bounded by fixing a finite set of potential events, each of which may occur at most once in any order. The events are specified using high-level Petri nets. The proposed logic encoding describes the space of possible causal links between events rather than possible sequences of states as in Bounded Model Checking. Independence between events is exploited intrinsically without partial order reductions, and the handling of data is symbolic. Experiments with a proof-of-concept implementation of the technique show that it has the potential to far exceed the performance of Bounded Model Checking.",
    responsibleauthor = "Dubrovin, Jori",
    flags = "StMcDes public",
    year = "2010",
    keywords = "formal verification, Bounded Model Checking, partial order method, Coloured Petri Nets, difference logic",
    impactfactor = "A4",
    pages = "146--162"
}