公司动态——国际联合逻辑大会SMT金牌

2022年8月11日，在FLoC (Federated Logic Conference，国际联合逻辑大会 )的IJCAR（国际联合自动推理会议）会议上宣布了SMT 2022比赛结果。由中科院软件所和晞德联合研发的SMT求解器Z3++在比赛中获得线性算术理论和非线性算术理论的多项第一，并在Model Validation的所有赛道综合评分中求解能力领先。其总分获得FLoC奥林匹克竞赛颁发的2块金牌。这是国内团队首次在每四年举办一次的FLoC奥林匹克竞赛的SMT比赛中取得金牌。Z3++针对位向量，线性算术和非线性算术都进行了深入优化。