Tools

• HyperQB is a push-button QBF-based bounded model checker for hyperproperties. HyperQube takes as input a set of NuSMV models and a hyperproperty expressed in the temporal logic HyperLTL. Unlike the existing similar tools, our QBF-based technique allows HyperQube to seamlessly deal with quantifier alternations. Based on the selection of either bug hunting or find witnesses, the instances of counterexamples or witnesses are returned. HyperQube comes with a rich set of case studies on a variety of case studies, including information security, concurrent data structures, path planning for robots, and mutation testing. The release of this tool is accompanied by an overview paper. HyperQube is available in this GitHub Repository.

 

• HyperProb
  • HyperProb is a model checker to verify probabilistic hyperproperties on Markov Decision Processes (MDP). Our tool receives as input a MDP expressed as a PRISM model and a HyperPCTL formula. By restricting the domain of scheduler quantification to memoryless non-probabilistic schedulers, our tool exploits an SMT-based encoding to model check probabilistic hyperproperties in HyperPCTL. Furthermore, when the property is satisfied, the tool can also provide a witness that can be used for synthesizing a DTMC that conforms with the specification. The release of this tool is accompanied by an overview paper. HyperProb is available in this GitHub Repository.

 

• ASSESS
  • Assess (Automated Synthesizer for SElf-Stabilizing Systems) implements a set of SMT-based techniques to synthesize distributed self-stabilizing programs. It takes as input (1) the topology of the distributed system in terms of read/write restrictions of processes, (2) the legitimate behavior of the system in the absence of faults, and (3) a set of high-level requirements such as the timing model (asynchronous or synchronous), and stabilization type (weak, strong, or monotonic). The legitimate behavior is specified either explicitly as a state predicate LS, or implicitly as a set of LTL formulas. The tool returns a finite-state self-stabilizing protocol as a set of guarded commands that realize the input specification. The synthesis engine of ASSESS is SMT-based and the tool supports the SMT-solver Z3 and the model finder Alloy. The internal algorithm are sound and complete, meaning that a synthesized solution by Assess is correct by construction and if the tool fails to synthesize a solution, then there does not exist one.

 

• RiTHM
  • The tool RiTHM (Runtime Time-triggered Heterogeneous Monitoring) takes a C program under inspection and a set of LTL properties as input and generates an instrumented C program that is verified at run time by a time-triggered monitor. The output C program can be instrumented in two ways: (1) it is monitored in a time-triggered fashion with a fixed polling period, or (2) the monitor is augmented with PID or fuzzy controllers that ensure minimum variation in monitor polling period while maximizing memory utilization. In both cases, the monitor is invoked in a time-triggered fashion, ensuring that the states of the program can be reconstructed at each invocation by using efficient instrumentation. The monitor verification decision procedure is sound and complete and takes advantage of the GPU many-core technology to speedup monitoring and reduce the runtime overhead.