Write a Blog >>
Fri 22 Jan 2016 14:20 - 14:45 at Grand Bay South - Track 2: Foundations of Model Checking Chair(s): Alexandra Silva

In the context of formal verification in general and model checking in particular, \emph{parity games} nowadays serve as a mighty vehicle: many problems are encoded as a parity game, which is then solved by the seminal algorithm by Jurdzinski. In this paper we identify the essence of this workflow to be the notion of \emph{progress measure}, and formalize it in general, possibly infinitary, lattice-theoretic terms. We then apply it to a general model-checking framework where systems are categorically presented as coalgebras, whose theoretical robustness is witnessed by a smooth transfer from the branching-time setting to the linear-time one. Although the framework can be used to derive some decision procedures for finite settings, we also expect the proposed framework to form a basis for sound proof methods for some undecidable/infinitary problems.

Fri 22 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

14:20 - 15:35: Track 2: Foundations of Model CheckingResearch Papers at Grand Bay South
Chair(s): Alexandra SilvaRadboud University Nijmegen
14:20 - 14:45
Talk
Lattice-Theoretic Progress Measures and Coalgebraic Model Checking
Research Papers
Ichiro HasuoUniversity of Tokyo, Shunsuke ShimizuUniversity of Tokyo, Corina CirsteaUniversity of Southampton
Media Attached
14:45 - 15:10
Talk
Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components
Research Papers
Media Attached
15:10 - 15:35
Talk
Memoryful Geometry of Interaction II: Recursion and Adequacy
Research Papers
Koko MuroyaUniversity of Tokyo, Naohiko HoshinoKyoto University, Ichiro HasuoUniversity of Tokyo
Media Attached