Publication Information

{'id': 'https://openalex.org/W2144996318', 'doi': None, 'title': 'Design Verification for Sequential Systems at Various Abstraction Levels', 'display_name': 'Design Verification for Sequential Systems at Various Abstraction Levels', 'publication_year': 2005, 'publication_date': '2005-01-27', 'ids': {'openalex': 'https://openalex.org/W2144996318', 'mag': '2144996318'}, 'language': 'en', 'primary_location': {'is_oa': False, 'landing_page_url': 'http://scholar.lib.vt.edu/theses/available/etd-01282005-102938/unrestricted/dissertation_v3.pdf', 'pdf_url': None, 'source': None, 'license': None, 'license_id': None, 'version': None, 'is_accepted': False, 'is_published': False}, 'type': 'dissertation', 'type_crossref': 'dissertation', 'indexed_in': [], '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/A5044007676', 'display_name': 'Liang Zhang', 'orcid': 'https://orcid.org/0000-0003-4201-8535'}, 'institutions': [], 'countries': [], 'is_corresponding': True, 'raw_author_name': 'Liang Zhang', 'raw_affiliation_strings': [], 'affiliations': []}], 'institution_assertions': [], 'countries_distinct_count': 0, 'institutions_distinct_count': 0, 'corresponding_author_ids': ['https://openalex.org/A5044007676'], 'corresponding_institution_ids': [], 'apc_list': None, 'apc_paid': None, 'fwci': None, 'has_fulltext': False, 'cited_by_count': 0, 'citation_normalized_percentile': {'value': 0.0, 'is_in_top_1_percent': False, 'is_in_top_10_percent': False}, 'cited_by_percentile_year': {'min': 0, 'max': 61}, 'biblio': {'volume': None, 'issue': None, 'first_page': None, 'last_page': None}, 'is_retracted': False, 'is_paratext': False, 'primary_topic': {'id': 'https://openalex.org/T10142', 'display_name': 'Formal Methods in Verification', 'score': 0.9999, '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.9999, '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/T11005', 'display_name': 'Radiation Effects in Electronics', 'score': 0.9939, 'subfield': {'id': 'https://openalex.org/subfields/2208', 'display_name': 'Electrical and Electronic Engineering'}, 'field': {'id': 'https://openalex.org/fields/22', 'display_name': 'Engineering'}, '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.9875, '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'}}], 'keywords': [{'id': 'https://openalex.org/keywords/abstraction-model-checking', 'display_name': 'Abstraction model checking', 'score': 0.9196104}, {'id': 'https://openalex.org/keywords/abstraction', 'display_name': 'Abstraction', 'score': 0.89781594}, {'id': 'https://openalex.org/keywords/symbolic-trajectory-evaluation', 'display_name': 'Symbolic trajectory evaluation', 'score': 0.4176864}], 'concepts': [{'id': 'https://openalex.org/C30888246', 'wikidata': 'https://www.wikidata.org/wiki/Q4669969', 'display_name': 'Abstraction model checking', 'level': 3, 'score': 0.9196104}, {'id': 'https://openalex.org/C124304363', 'wikidata': 'https://www.wikidata.org/wiki/Q673661', 'display_name': 'Abstraction', 'level': 2, 'score': 0.89781594}, {'id': 'https://openalex.org/C110251889', 'wikidata': 'https://www.wikidata.org/wiki/Q1569697', 'display_name': 'Model checking', 'level': 2, 'score': 0.84085536}, {'id': 'https://openalex.org/C41008148', 'wikidata': 'https://www.wikidata.org/wiki/Q21198', 'display_name': 'Computer science', 'level': 0, 'score': 0.7909952}, {'id': 'https://openalex.org/C80444323', 'wikidata': 'https://www.wikidata.org/wiki/Q2878974', 'display_name': 'Theoretical computer science', 'level': 1, 'score': 0.49787045}, {'id': 'https://openalex.org/C199360897', 'wikidata': 'https://www.wikidata.org/wiki/Q9143', 'display_name': 'Programming language', 'level': 1, 'score': 0.48622504}, {'id': 'https://openalex.org/C23123167', 'wikidata': 'https://www.wikidata.org/wiki/Q7661193', 'display_name': 'Symbolic trajectory evaluation', 'level': 3, 'score': 0.4176864}, {'id': 'https://openalex.org/C11413529', 'wikidata': 'https://www.wikidata.org/wiki/Q8366', 'display_name': 'Algorithm', 'level': 1, 'score': 0.41366428}, {'id': 'https://openalex.org/C138885662', 'wikidata': 'https://www.wikidata.org/wiki/Q5891', 'display_name': 'Philosophy', 'level': 0, 'score': 0.0}, {'id': 'https://openalex.org/C111472728', 'wikidata': 'https://www.wikidata.org/wiki/Q9471', 'display_name': 'Epistemology', 'level': 1, 'score': 0.0}], 'mesh': [], 'locations_count': 1, 'locations': [{'is_oa': False, 'landing_page_url': 'http://scholar.lib.vt.edu/theses/available/etd-01282005-102938/unrestricted/dissertation_v3.pdf', 'pdf_url': None, 'source': None, 'license': None, 'license_id': None, 'version': None, 'is_accepted': False, 'is_published': False}], 'best_oa_location': None, 'sustainable_development_goals': [{'score': 0.46, 'display_name': 'Responsible consumption and production', 'id': 'https://metadata.un.org/sdg/12'}], 'grants': [], 'datasets': [], 'versions': [], 'referenced_works_count': 57, 'referenced_works': ['https://openalex.org/W1495266209', 'https://openalex.org/W1498403163', 'https://openalex.org/W1511155470', 'https://openalex.org/W1511688816', 'https://openalex.org/W1517173520', 'https://openalex.org/W1536007121', 'https://openalex.org/W1549820563', 'https://openalex.org/W1552503736', 'https://openalex.org/W1605593319', 'https://openalex.org/W1749917042', 'https://openalex.org/W1779418668', 'https://openalex.org/W1801221103', 'https://openalex.org/W1819209966', 'https://openalex.org/W1836483134', 'https://openalex.org/W2011848140', 'https://openalex.org/W2023730632', 'https://openalex.org/W2044560939', 'https://openalex.org/W2046239089', 'https://openalex.org/W2047457200', 'https://openalex.org/W2057361103', 'https://openalex.org/W2075959177', 'https://openalex.org/W2080267935', 'https://openalex.org/W2098046166', 'https://openalex.org/W2103351789', 'https://openalex.org/W2103534830', 'https://openalex.org/W2107519162', 'https://openalex.org/W2110123236', 'https://openalex.org/W2110648791', 'https://openalex.org/W2110728526', 'https://openalex.org/W2115180022', 'https://openalex.org/W2115383281', 'https://openalex.org/W2118325845', 'https://openalex.org/W2118623093', 'https://openalex.org/W2118919709', 'https://openalex.org/W2118970405', 'https://openalex.org/W2119890788', 'https://openalex.org/W2123329891', 'https://openalex.org/W2124537426', 'https://openalex.org/W2124618076', 'https://openalex.org/W2127005882', 'https://openalex.org/W2129508712', 'https://openalex.org/W2140132043', 'https://openalex.org/W2141393830', 'https://openalex.org/W2142306100', 'https://openalex.org/W2142785340', 'https://openalex.org/W2143744297', 'https://openalex.org/W2145199041', 'https://openalex.org/W2146297576', 'https://openalex.org/W2146422945', 'https://openalex.org/W2152280960', 'https://openalex.org/W2159503942', 'https://openalex.org/W2160667400', 'https://openalex.org/W2162116017', 'https://openalex.org/W2162945176', 'https://openalex.org/W2165566357', 'https://openalex.org/W2167452021', 'https://openalex.org/W2913459036'], 'related_works': ['https://openalex.org/W7015221', 'https://openalex.org/W63955974', 'https://openalex.org/W3145288617', 'https://openalex.org/W3113715973', 'https://openalex.org/W2567280546', 'https://openalex.org/W2526106663', 'https://openalex.org/W2416062364', 'https://openalex.org/W2402578157', 'https://openalex.org/W2394566511', 'https://openalex.org/W2221978111', 'https://openalex.org/W2178390125', 'https://openalex.org/W2160811033', 'https://openalex.org/W2159789838', 'https://openalex.org/W2152147436', 'https://openalex.org/W2143208164', 'https://openalex.org/W2143015677', 'https://openalex.org/W2142928983', 'https://openalex.org/W2107840120', 'https://openalex.org/W1504525241', 'https://openalex.org/W1498113537'], 'abstract_inverted_index': {'ion': [0], 'and': [1, 110, 146, 248, 284], 'Refinement': [2], 'for': [3, 18, 29, 156, 167], 'Design': [4], 'Verification': [5], 'at': [6], 'Logic': [7], 'Level': [8], 'Abstraction': [9], 'refinement': [10, 31, 144, 148, 169, 282], 'has': [11, 149], 'recently': [12, 150], 'emerged': [13, 151], 'as': [14, 152], 'an': [15, 92, 153, 230], 'enabling': [16, 154], 'technology': [17, 155], 'applying': [19, 157], 'model': [20, 40, 52, 71, 78, 102, 114, 120, 158, 178, 190, 209, 216, 240, 252, 258], 'checking': [21, 72, 103, 159, 210, 241], 'techniques': [22, 28, 160, 166], 'to': [23, 74, 112, 122, 161, 212, 250, 260], 'large': [24, 162], 'real-life': [25, 163], 'designs.': [26, 164], 'Previous': [27, 165], 'abstraction': [30, 44, 83, 136, 143, 168, 182, 221, 274, 281], 'work': [32, 123, 170, 261], 'on': [33, 106, 129, 171, 244, 267], 'static': [34, 82, 172, 220], 'abstractions,': [35, 173], 'in': [36, 174], 'that': [37, 134, 175, 272], 'the': [38, 43, 50, 70, 77, 95, 107, 113, 119, 139, 142, 176, 181, 188, 208, 215, 233, 245, 251, 257, 277, 280], 'abstract': [39, 76, 126, 177, 214, 264], 'produced': [41, 79, 179, 217], 'by': [42, 49, 80, 88, 180, 187, 218, 226], 'algorithm': [45, 73, 183, 211], 'is': [46, 86, 184, 224], 'not': [47, 185], 'modified': [48, 186], 'downstream': [51, 189], 'checking.': [53, 191], 'We': [54, 192], 'propose': [55, 193], 'a': [56, 194], 'new,': [57, 195], 'dynamic': [58, 135, 196, 273], 'method': [59, 197], 'of': [60, 69, 94, 97, 99, 141, 198, 207, 232, 235, 237, 279], 'abstraction,': [61, 199], 'which': [62, 200], 'can': [63, 201], 'be': [64, 202], 'applied': [65, 203], 'during': [66, 204], 'successive': [67, 205], 'steps': [68, 206], 'further': [75, 213], 'traditional': [81, 219], 'methods.': [84, 222], 'This': [85, 223], 'facilitated': [87, 225], 'information': [89, 227], 'gathered': [90, 228], 'from': [91, 229], 'analysis': [93, 231], 'proof': [96, 234], 'unsatisfiability': [98, 236], 'SAT-based': [100, 238], 'bounded': [101, 239], 'problems,': [104, 242], 'solved': [105, 243], 'concrete': [108, 246], 'model,': [109, 247], 'passed': [111, 249], 'checker.': [115, 253], 'It': [116, 254], 'effectively': [117, 255], 'allows': [118, 256], 'checker': [121, 259], 'with': [124, 262], 'smaller': [125, 263], 'models.': [127, 265], 'Experiments': [128, 266], 'several': [130, 268], 'industrial': [131, 269], 'benchmarks': [132, 270], 'demonstrate': [133, 271], 'significantly': [137, 275], 'improves': [138, 276], 'performance': [140, 278], 'flow': [145, 283], 'alsoion': [147], 'also': [285]}, 'cited_by_api_url': 'https://api.openalex.org/works?filter=cites:W2144996318', 'counts_by_year': [], 'updated_date': '2024-12-14T12:16:33.501292', 'created_date': '2016-06-24'}