(A) name of the model checker ( for multiple-properties track ): 
mpmc

(B) authors:
Chi-An Wu, Cheng-Yin Wu, Chung-Yang (Ric) Huang

(C) affiliation:
Graduate Institute of Electronics Engineering, National Taiwan University

(D) some bullets on the technology/algorithms, as well as to which extend the code is based on other tools

We develop the mutiple-properties checking algorithms with abc and minisat package, and use their re-synthesis and solving techniques.

In our flow, we include three phases:
1. Simulation phase
Simulation consists of combinational circuit simulation (without initial states) and sequential circuit simulaiton, and 1-induction invariant checking [1].
A property is considered to be easy if combinational circuit simulation reports that it has higher possibility to fail or hold.
That is, it is in the extreme conidtion.
Otherwise, we think the reachability with the property is complex, and the property is considered to be hard.
Besides, if properties have similar score, we use the dfs order and the level of the circuit to break tie. ( the lower one has higher priority )

2. Probe Phase
We make three engines: PDR [2], BMC [3], Induction [4] with supporting incremental solving, constraints, and sharing learnt data.
Probe phase is like to BFS on multiple properties.
When solving properties one by one, it is better to localize the solving region.
In incremental solving, we turn off the assignment of the solver's variables which are not in the cone. Solvers can answer satisfying without touching all variabels.
The sharing learnt data includes overapproximate reachability, combinational/sequential constant variables, solving timeframes, and counterexamples.
We limit high bound of timeframe number and runtime in probe phase.
Then, we use the number of learnt clauses/reachability to reorder unsolved properties. (the lower one has higher priority)

3. Solve Phase
Solving phase is similar to probe phase, but it releases the bound of timeframe number and runtime into lower one.
It is like to DFS on multiple properties.
The solving procedure inherits the solving in proble phase since we support incremental solving.

Parrallel issues:
All solvers has one thread for running (implemented by pthread), and they only stop together when entering to another phase.
They do not need to solve the same property at the same time.

Reference:
[1] M. L. Case, A. Mishchenko, and R. K. Brayton, "Cut-based inductive invariant computation", IWLS 2008.
[2] N. Een, A. Mishchenko and R. Brayton, "Efficient implementation of property-directed reachability", FMCAD 2011.
[3] A. Biere, A. Cimatti, E. Clarke, O. Strichman, and Y. Zhu, "Bounded model checking", Advances in Computers, 2003.
[4] P. Bjesse and K. Claessen, "SAT-based verification without state space traversal", FMCAD 2000.