Publication Information

{'id': 'https://openalex.org/W2316925676', 'doi': 'https://doi.org/10.3724/sp.j.1001.2012.04196', 'title': 'Path Sensitive Program Verification Based on SMT Solvers', 'display_name': 'Path Sensitive Program Verification Based on SMT Solvers', 'publication_year': 2012, 'publication_date': '2012-11-13', 'ids': {'openalex': 'https://openalex.org/W2316925676', 'doi': 'https://doi.org/10.3724/sp.j.1001.2012.04196', 'mag': '2316925676'}, 'language': 'en', 'primary_location': {'is_oa': False, 'landing_page_url': 'https://doi.org/10.3724/sp.j.1001.2012.04196', 'pdf_url': None, 'source': {'id': 'https://openalex.org/S4210224179', 'display_name': 'Journal of Software', 'issn_l': '1000-9825', 'issn': ['1000-9825'], 'is_oa': False, 'is_in_doaj': False, 'is_core': True, 'host_organization': 'https://openalex.org/P4310319982', 'host_organization_name': 'Science Press', 'host_organization_lineage': ['https://openalex.org/P4310319982'], 'host_organization_lineage_names': ['Science Press'], 'type': 'journal'}, 'license': None, 'license_id': None, 'version': None, 'is_accepted': False, 'is_published': False}, 'type': 'article', 'type_crossref': 'journal-article', 'indexed_in': ['crossref'], 'open_access': {'is_oa': False, 'oa_status': 'closed', 'oa_url': None, 'any_repository_has_fulltext': False}, 'authorships': [{'author_position': 'first', 'author': {'id': 'https://openalex.org/A5024849649', 'display_name': 'Yanxiang He', 'orcid': None}, 'institutions': [], 'countries': [], 'is_corresponding': False, 'raw_author_name': 'Yan-Xiang HE', 'raw_affiliation_strings': [], 'affiliations': []}, {'author_position': 'middle', 'author': {'id': 'https://openalex.org/A5090160782', 'display_name': 'Wei Wu', 'orcid': 'https://orcid.org/0000-0001-8534-3667'}, 'institutions': [], 'countries': [], 'is_corresponding': False, 'raw_author_name': 'Wei WU', 'raw_affiliation_strings': [], 'affiliations': []}, {'author_position': 'middle', 'author': {'id': 'https://openalex.org/A5100454402', 'display_name': 'Yong Chen', 'orcid': 'https://orcid.org/0000-0002-4157-6773'}, 'institutions': [], 'countries': [], 'is_corresponding': False, 'raw_author_name': 'Yong CHEN', 'raw_affiliation_strings': [], 'affiliations': []}, {'author_position': 'last', 'author': {'id': 'https://openalex.org/A5081196371', 'display_name': 'Chao Xu', 'orcid': 'https://orcid.org/0000-0003-4417-3299'}, 'institutions': [], 'countries': [], 'is_corresponding': False, 'raw_author_name': 'Chao XU', 'raw_affiliation_strings': [], 'affiliations': []}], 'institution_assertions': [], 'countries_distinct_count': 0, 'institutions_distinct_count': 0, 'corresponding_author_ids': [], 'corresponding_institution_ids': [], 'apc_list': None, 'apc_paid': None, 'fwci': 0.576, 'has_fulltext': False, 'cited_by_count': 2, 'citation_normalized_percentile': {'value': 0.506436, 'is_in_top_1_percent': False, 'is_in_top_10_percent': False}, 'cited_by_percentile_year': {'min': 72, 'max': 75}, 'biblio': {'volume': '23', 'issue': '10', 'first_page': '2655', 'last_page': '2664'}, 'is_retracted': False, 'is_paratext': False, 'primary_topic': {'id': 'https://openalex.org/T10142', 'display_name': 'Formal Methods in Verification', 'score': 0.9965, 'subfield': {'id': 'https://openalex.org/subfields/1703', 'display_name': 'Computational Theory and Mathematics'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}, 'topics': [{'id': 'https://openalex.org/T10142', 'display_name': 'Formal Methods in Verification', 'score': 0.9965, 'subfield': {'id': 'https://openalex.org/subfields/1703', 'display_name': 'Computational Theory and Mathematics'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}, {'id': 'https://openalex.org/T10743', 'display_name': 'Software Testing and Debugging Techniques', 'score': 0.9941, 'subfield': {'id': 'https://openalex.org/subfields/1712', 'display_name': 'Software'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}, {'id': 'https://openalex.org/T10904', 'display_name': 'Embedded Systems Design Techniques', 'score': 0.9921, 'subfield': {'id': 'https://openalex.org/subfields/1708', 'display_name': 'Hardware and Architecture'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}], 'keywords': [{'id': 'https://openalex.org/keywords/satisfiability-modulo-theories', 'display_name': 'Satisfiability Modulo Theories', 'score': 0.6644833}, {'id': 'https://openalex.org/keywords/traverse', 'display_name': 'Traverse', 'score': 0.61857975}, {'id': 'https://openalex.org/keywords/software-verification', 'display_name': 'Software verification', 'score': 0.594931}, {'id': 'https://openalex.org/keywords/abstract-interpretation', 'display_name': 'Abstract Interpretation', 'score': 0.551474}, {'id': 'https://openalex.org/keywords/assertion', 'display_name': 'Assertion', 'score': 0.5138786}, {'id': 'https://openalex.org/keywords/solver', 'display_name': 'Solver', 'score': 0.45726714}, {'id': 'https://openalex.org/keywords/component', 'display_name': 'Component (thermodynamics)', 'score': 0.4542837}], 'concepts': [{'id': 'https://openalex.org/C41008148', 'wikidata': 'https://www.wikidata.org/wiki/Q21198', 'display_name': 'Computer science', 'level': 0, 'score': 0.7966547}, {'id': 'https://openalex.org/C2777735758', 'wikidata': 'https://www.wikidata.org/wiki/Q817765', 'display_name': 'Path (computing)', 'level': 2, 'score': 0.6918191}, {'id': 'https://openalex.org/C164155591', 'wikidata': 'https://www.wikidata.org/wiki/Q2067766', 'display_name': 'Satisfiability modulo theories', 'level': 2, 'score': 0.6644833}, {'id': 'https://openalex.org/C176809094', 'wikidata': 'https://www.wikidata.org/wiki/Q15401496', 'display_name': 'Traverse', 'level': 2, 'score': 0.61857975}, {'id': 'https://openalex.org/C33054407', 'wikidata': 'https://www.wikidata.org/wiki/Q6504747', 'display_name': 'Software verification', 'level': 5, 'score': 0.594931}, {'id': 'https://openalex.org/C2780654840', 'wikidata': 'https://www.wikidata.org/wiki/Q333341', 'display_name': 'Abstract interpretation', 'level': 2, 'score': 0.551474}, {'id': 'https://openalex.org/C8797682', 'wikidata': 'https://www.wikidata.org/wiki/Q2115', 'display_name': 'XML', 'level': 2, 'score': 0.5246109}, {'id': 'https://openalex.org/C40422974', 'wikidata': 'https://www.wikidata.org/wiki/Q741248', 'display_name': 'Assertion', 'level': 2, 'score': 0.5138786}, {'id': 'https://openalex.org/C98183937', 'wikidata': 'https://www.wikidata.org/wiki/Q2112188', 'display_name': 'Program analysis', 'level': 2, 'score': 0.4749056}, {'id': 'https://openalex.org/C2777904410', 'wikidata': 'https://www.wikidata.org/wiki/Q7397', 'display_name': 'Software', 'level': 2, 'score': 0.4695243}, {'id': 'https://openalex.org/C2778770139', 'wikidata': 'https://www.wikidata.org/wiki/Q1966904', 'display_name': 'Solver', 'level': 2, 'score': 0.45726714}, {'id': 'https://openalex.org/C168167062', 'wikidata': 'https://www.wikidata.org/wiki/Q1117970', 'display_name': 'Component (thermodynamics)', 'level': 2, 'score': 0.4542837}, {'id': 'https://openalex.org/C199360897', 'wikidata': 'https://www.wikidata.org/wiki/Q9143', 'display_name': 'Programming language', 'level': 1, 'score': 0.4415103}, {'id': 'https://openalex.org/C80444323', 'wikidata': 'https://www.wikidata.org/wiki/Q2878974', 'display_name': 'Theoretical computer science', 'level': 1, 'score': 0.41035494}, {'id': 'https://openalex.org/C11413529', 'wikidata': 'https://www.wikidata.org/wiki/Q8366', 'display_name': 'Algorithm', 'level': 1, 'score': 0.33245876}, {'id': 'https://openalex.org/C529173508', 'wikidata': 'https://www.wikidata.org/wiki/Q638608', 'display_name': 'Software development', 'level': 3, 'score': 0.19730473}, {'id': 'https://openalex.org/C186846655', 'wikidata': 'https://www.wikidata.org/wiki/Q3398377', 'display_name': 'Software construction', 'level': 4, 'score': 0.09415883}, {'id': 'https://openalex.org/C111919701', 'wikidata': 'https://www.wikidata.org/wiki/Q9135', 'display_name': 'Operating system', 'level': 1, 'score': 0.08070016}, {'id': 'https://openalex.org/C121332964', 'wikidata': 'https://www.wikidata.org/wiki/Q413', 'display_name': 'Physics', 'level': 0, 'score': 0.0}, {'id': 'https://openalex.org/C13280743', 'wikidata': 'https://www.wikidata.org/wiki/Q131089', 'display_name': 'Geodesy', 'level': 1, 'score': 0.0}, {'id': 'https://openalex.org/C97355855', 'wikidata': 'https://www.wikidata.org/wiki/Q11473', 'display_name': 'Thermodynamics', 'level': 1, 'score': 0.0}, {'id': 'https://openalex.org/C205649164', 'wikidata': 'https://www.wikidata.org/wiki/Q1071', 'display_name': 'Geography', 'level': 0, 'score': 0.0}], 'mesh': [], 'locations_count': 1, 'locations': [{'is_oa': False, 'landing_page_url': 'https://doi.org/10.3724/sp.j.1001.2012.04196', 'pdf_url': None, 'source': {'id': 'https://openalex.org/S4210224179', 'display_name': 'Journal of Software', 'issn_l': '1000-9825', 'issn': ['1000-9825'], 'is_oa': False, 'is_in_doaj': False, 'is_core': True, 'host_organization': 'https://openalex.org/P4310319982', 'host_organization_name': 'Science Press', 'host_organization_lineage': ['https://openalex.org/P4310319982'], 'host_organization_lineage_names': ['Science Press'], 'type': 'journal'}, 'license': None, 'license_id': None, 'version': None, 'is_accepted': False, 'is_published': False}], 'best_oa_location': None, 'sustainable_development_goals': [], 'grants': [], 'datasets': [], 'versions': [], 'referenced_works_count': 1, 'referenced_works': ['https://openalex.org/W2044590882'], 'related_works': ['https://openalex.org/W4320058113', 'https://openalex.org/W2970480852', 'https://openalex.org/W2568762190', 'https://openalex.org/W2525463489', 'https://openalex.org/W2185159868', 'https://openalex.org/W2157660637', 'https://openalex.org/W2058895276', 'https://openalex.org/W2020973245', 'https://openalex.org/W1836373119', 'https://openalex.org/W1524612439'], 'abstract_inverted_index': {'PDF': [0], 'HTML阅读': [1], 'XML下载': [2], '导出引用': [3], '引用提醒': [4], '基于SMT求解器的路径敏感程序验证': [5], 'DOI:': [6], '10.3724/SP.J.1001.2012.04196': [7], '作者:': [8], '作者单位:': [9], '作者简介:': [10], '通讯作者:': [11], '中图分类号:': [12], '基金项目:': [13], '国家自然科学基金(90818018,': [14], '91018009)': [15], 'Path': [16], 'Sensitive': [17], 'Program': [18], 'Verification': [19], 'Based': [20], 'on': [21, 178], 'SMT': [22, 44, 184], 'Solvers': [23], 'Author:': [24], 'Affiliation:': [25], 'Fund': [26], 'Project:': [27], '摘要': [28], '|': [29, 31, 33, 35, 37, 39, 41], '图/表': [30], '访问统计': [32], '参考文献': [34, 199], '相似文献': [36, 200], '引证文献': [38, 201], '资源附件': [40], '文章评论': [42], '摘要:随着软件规模的不断扩大以及复杂度的不断增长,人们越来越关注软件的可信性问题.验证程序是否满足断言所描述的性质,是保证软件可信性的一种常见方法.路径敏感的程序验证由于不可能遍历所有的路径,需要合并路径信息,因此造成精度上的损失.提出一种基于': [43], '求解器的路径敏感程序验证方法,在保证精确度的前提下,有效减少路径搜索空间.其基本思想是,利用最大强连通分量压缩循环路径,然后根据目标断言对控制流图进行切片.使用一种布尔表达式方法对路径空间进行抽象,结合抽象解释和符号执行技术对路径进行验证.结合': [45], 'F-Soft': [46], '平台和': [47], 'Z3': [48], '工具对该方法进行了实验验证,结果表明,该方法在验证的精确度和效率上都有较好的效果.': [49], 'Abstract:With': [50], 'the': [51, 73, 85, 119, 125, 128, 136, 147, 150, 156, 164, 179], 'rapid': [52], 'increase': [53], 'in': [54], 'size': [55], 'and': [56, 61, 123, 145, 162, 169, 183, 187, 197], 'complexity': [57], 'of': [58, 84, 105], 'software,': [59], 'more': [60, 62], 'attention': [63], 'is': [64, 78, 134], 'paid': [65], 'to': [66, 149], 'thesoftware’s': [67], 'trust.': [68], 'Verifying': [69], 'whether': [70], 'programs': [71], 'satisfy': [72], 'properties': [74], 'described': [75], 'by': [76, 139], 'assertions': [77], 'a': [79, 103, 110], 'common': [80], 'method': [81, 113, 192], 'toguarantee': [82], 'trust': [83], 'software.': [86], 'Since': [87], 'path': [88, 99, 120, 138, 157, 165], 'sensitive': [89], 'program': [90, 111], 'verification': [91, 112, 181], 'cannot': [92], 'traverse': [93], 'all': [94], 'paths,': [95], 'it': [96], 'needs': [97], 'mergethe': [98], 'information,': [100], 'which': [101, 116], 'causes': [102], 'loss': [104], 'precision.': [106], 'The': [107, 131, 153, 172], 'study': [108, 154, 173], 'proposes': [109], 'usingSMT': [114], 'solvers,': [115], 'can': [117], 'reduce': [118], 'search': [121], 'space': [122, 158], 'improve': [124], 'precision': [126], 'at': [127], 'same': [129], 'time.': [130], 'method’smain': [132], 'sprit': [133], 'impacting': [135], 'cycle': [137], 'using': [140, 159], 'maximal': [141], 'strongly': [142], 'connected': [143], 'component': [144], 'slicing': [146], 'CFGaccording': [148], 'aim': [151], 'assertion.': [152], 'abstracts': [155], 'Boolean': [160], 'formulas': [161], 'verifies': [163], 'bycombining': [166], 'abstract': [167], 'interpretation': [168], 'symbolic': [170], 'execution.': [171], 'has': [174], 'conducted': [175], 'experiments': [176], 'based': [177, 195], 'F-Softprogram': [180], 'platform': [182], 'solver': [185], 'Z3,': [186], 'results': [188], 'show': [189], 'that': [190], 'this': [191], 'performs': [193], 'well': [194], 'onprecision': [196], 'effect.': [198]}, 'cited_by_api_url': 'https://api.openalex.org/works?filter=cites:W2316925676', 'counts_by_year': [{'year': 2014, 'cited_by_count': 1}, {'year': 2013, 'cited_by_count': 1}], 'updated_date': '2024-12-11T11:28:37.289578', 'created_date': '2016-06-24'}