Abschnittsübersicht

  • Matteo Acclavio (Università Roma Tre) will speak in this week: 

    • A Graphical Proof Theory for "happens-before"

    Abstract: The "happens-before" is an order relation over events playing a crucial role in formal verification. 
    Logics modelling this relation by means of a non-commutative connective have been introduced in the literature. 
    However, their expressiveness is limited to series-parallel orders. In this talk, after recalling the proof theoretical results for these logics and their connections to process calculi, I will present proof systems operating on graphs instead of formulas. This innovative framework allows us to overcome the restrictions of in-line formulas and to handle non-series parallel orders.