Tools/Case studies

Tools

These are the tools developed in our group:

ISS: Iscas Self-driving System strives to deliver a highly modularized autonomous driving platform.
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 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 polynomial loop invariants of probabilistic programs.
IscasMC: IscasMC is a model checker for probabilistic models. It supports Markov chains and Markov decision Processes (MDP), and properties specified in PCTL, PLTL and their combination PCTL*. It implements the efficient algorithm in particularly tuned to handle linear time properties.
TransFace: A Transferable Attack Framework against the Deep Face Recognition.