1949年，陪同着新中国的降生，中国科学院建设。 作为国家于科学技术方面的最高学术机谈判天下天然科学与高新技术的综合研究与生长中央，建院以来，中国科学院时刻服膺任务，与科学共进，与祖国偕行，以国家茂盛、人平易近幸福为己任，人材辈出，硕果累累，为我国科技前进、经济社会生长及国家宁静做出了不成替换的主要孝敬。 更多简介 + 中国科学院院级科技专项系统包罗战略性先导科技专项、重点部署科研专项、科技人材专项、科技相助专项、科技平台专项5类一级专项，实施分类定位、分级治理。 为利便科研职员周全快捷相识院级科技专项信息并举行项目申报等相干操作，特搭建中国科学院院级科技专项信息治理服务平台。相识科技专项更多内容，请点击进入→ 近期，中国科学院软件研究所研究员蔡少伟团队于逻辑约束求解器研究中取患上多项进展，并于命题逻辑可满意性问题（SAT）、可满意性模理论问题（SMT）等多项竞赛中斩获佳绩。 于逻辑约束求解器领域，SAT及SMT是两个最主要的逻辑约束问题。SAT是命题逻辑上的约束求解问题，SMT是一阶谓词逻辑上的约束求解问题。它们不仅于主动定理证实、软件工程等学术研究中有广泛运用，另有是信息宁静、集成电路设计主动化及软件验证等领域的底层盘算引擎。 近日，SAT聚会会议宣布SAT及MaxSAT角逐结果，FLoC（Federated Logic Conference，国际结合逻辑年夜会）的IJCAR（国际结合主动推理聚会会议）聚会会议宣布SMT 2022角逐结果。 于SAT角逐中，蔡少伟团队以较着上风获得主赛道并行组冠军及NoLimits赛道冠军；于MaxSAT角逐中，团队博得险些年夜满贯的成就，于统共6个赛道中获得5个冠军及1个亚军（此中1个冠军与华为理论试验室、东北师范年夜学等团队相助获得）。 于SMT 2022角逐中，蔡少伟团队研发的SMT求解器Z3++（基在国际主流求解器Z3的衍生求解器）于角逐中获得线性算术理论及非线性算术理论的多项第一，并于Model Validation的所有赛道综合评分中求解能力领先。其总分获得FLoC奥林匹克竞赛颁布的2块金牌（年夜赛共设6枚金牌2枚银牌）。这是海内团队初次于FLoC奥林匹克竞赛的SMT角逐中取患上金牌。FLoC每一四年举办一次，于数理逻辑及盘算机科学领域有着主要影响。
扫二维码用手机看
0551-65333939 
留言 