EN | DE
Theoretische Informatik

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

theses [2018/12/20 17:57]
tadeusz
theses [2019/05/16 21:58] (current)
tadeusz [Dr. Tadeusz Litak In Kooperation mit Technische Hochschule Nürnberg]
Line 77: Line 77:
 ----- -----
  
-===  Formalizing CTL with fairness ===+===  CTL with fairness ===
  
  
-There are several possible ways of extending CTL with fairness constraints, as discussed in [[https://www8.cs.fau.de/_media/ws18:fmsoft:fmsoft_nov13pre.pdf|the model checking part of the Formal Methods lecture]]. The goal is to formalize their syntax and semantics in Coq, and formalize some  proofs about expressivity of such constraints in the recent extension proposed by Ghilardi and van Gool.+There are several possible ways of extending CTL with fairness constraints, as discussed in [[https://www8.cs.fau.de/_media/ws18:fmsoft:fmsoft_nov13pre.pdf|the model checking part of the Formal Methods lecture]]. There are at least two conceivable projects on this subject:  
 +  - The goal of the first one is to formalize their syntax and semantics in Coq, and formalize some  proofs about expressivity of such constraints in the recent extension proposed by Ghilardi and van Gool (CTL^f). 
 +  - The goal of the second one is to complexity of compare model checking of CTL^f, including [[https://www8.cs.fau.de/_media/ws18:fmsoft:fmsoft_nov27pre.pdf|bounded model checking]], with that of modern algorithms for well-behaved subclasses of modal fixpoint formulas, many of which are able to express CTL^f formulas. There are powerful modern tools based on such algorithms. The [[http://www.win.tue.nl/~timw/downloads/amc2016/pgsolver.pdf|PG Solver overview]] is a good starting point.
  
  
Line 88: Line 90:
  
 ------ ------
 +
 +
 +
  
 === Developing metatheory and proof support of GQM and SOPML ==== === Developing metatheory and proof support of GQM and SOPML ====
Line 230: Line 235:
 === Rebasing from VST to Iris ======= === Rebasing from VST to Iris =======
  
-At present, the development of VeriGHC is done in the framework of [[http://vst.cs.princeton.edu/|VST]] by Appel et al. However, in principle nothing would prevent using another major, European framework of the [[https://iris-project.org/|Iris project]] (currently used, e.g., in the [[http://plv.mpi-sws.org/rustbelt/|RustBelt]] project. In general, the degree of portability between these two projects is an important challenge for the community, which has not been fully clarified yet. VeriGHC may provide an important case study.+At present, the development of VeriGHC is done in the framework of [[http://vst.cs.princeton.edu/|VST]] by Appel et al. However, in principle nothing would prevent using another major, European framework of the [[https://iris-project.org/|Iris project]]currently used, e.g., in the [[http://plv.mpi-sws.org/rustbelt/|RustBelt]] project. In general, the degree of portability between these two projects is an important challenge for the community, which has not been fully clarified yet. VeriGHC may provide an important case study.