Tools/Case studies

These are the tools developed in our group:

  • PRODeep: a platform for robustness verification of deep neural networks.
  • dpCTL: a tool for checking differential privacy CTL properties on Markov chains and Markov decision processes, based on ePMC.
  • ePMC: the successor of IscasMC, from which it keeps all features about Linear Time Logic probabilistic model checking. ePMC is highly modular, which allows everyone to extend and improve the functionalities of the model checker.
  • QMC: a model checker for quantum Markov chains. The source code of the user interface can be found at here.
  • Petl: a tool for model checking probabilistic epistemic logic for probabilistic multiagent systems.
  • SVMRanker: a tool for synthesizing multiphase/nested ranking functions of loop programs based on SVM.
  • ROLL: a library of learning algorithms for ω-regular languages.  It consists of some learning algorithms for FDFAs and for Büchi automata.
  • Ppsdp : a tool for finding polynomail loop invariants of probabilistic programs.
  • IscasMCIscasMC is a model checker for probabilistic models. It supports Markov chains and Markov decision Processes (MDP), and properties specified in PCTLPLTL and their combination PCTL*. It implements the efficient algorithm in particularly tuned to handle linear time properties.

The development of the tools listed above is sponsored by the CAP Sino-German project.

Case studies