Counterexample-guided abstraction refinement

The main practical problem in model checking is the combinatorial explosion of system states commonly known as the state explosion problem. Abstraction methods attempt to reduce the size of the state space by employing knowledge about the system and the specification in order to model only relevant...

Full description

Saved in:
Bibliographic Details
Main Author: Clarke, E.
Format: Conference Proceeding
Language:English
Subjects:
Boolean functions
Collaboration
Computer science
Concrete
Contracts
Data mining
Data structures
Explosions
State-space methods
US Department of Defense
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by
cites
container_end_page 8
container_issue
container_start_page 7
container_title
container_volume
creator Clarke, E.
description The main practical problem in model checking is the combinatorial explosion of system states commonly known as the state explosion problem. Abstraction methods attempt to reduce the size of the state space by employing knowledge about the system and the specification in order to model only relevant features in the Kripke structure. Counterexample-guided abstraction refinement is an automatic abstraction method where, starting with a relatively small skeletal representation of the system to be verified, increasingly precise abstract representations of the system are computed. The key step is to extract information from false negatives ("spurious counterexamples") due to over-approximation.
doi_str_mv 10.1109/TIME.2003.1214874
format conference_proceeding
fullrecord <record><control><sourceid>ieee_CHZPO</sourceid><recordid>TN_cdi_ieee_primary_1214874</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><ieee_id>1214874</ieee_id><sourcerecordid>1214874</sourcerecordid><originalsourceid>FETCH-LOGICAL-i218t-6f9f41e0434e95159fae7dab0cf4bda0b9712652715330b616ee49fac388dfd13</originalsourceid><addsrcrecordid>eNotT8tOwzAQtHhIhNIPQFz6ATjd9TpOfERRgUqtuJRz5cRrZNSkVZJK8PdYonOZw4zmIcQjQo4Idrlbb1e5AqAcFeqq1FciU0RKGm2qa3EPpbEF2iTeiAwLAomEeCfm4_gNCWSNKVQmnuvjuZ944B_XnQ4sv87Rs1-4ZpwG107x2C8GDrHnjvvpQdwGdxh5fuGZ-Hxd7ep3ufl4W9cvGxkVVpM0wQaNDJo0pxGFDY5L7xpog268g8aWqFJ7mXYRNAYNs06mlqrKB480E0__uZGZ96chdm743V-O0h-uY0S-</addsrcrecordid><sourcetype>Publisher</sourcetype><iscdi>true</iscdi><recordtype>conference_proceeding</recordtype></control><display><type>conference_proceeding</type><title>Counterexample-guided abstraction refinement</title><source>IEEE Xplore All Conference Series</source><creator>Clarke, E.</creator><creatorcontrib>Clarke, E.</creatorcontrib><description>The main practical problem in model checking is the combinatorial explosion of system states commonly known as the state explosion problem. Abstraction methods attempt to reduce the size of the state space by employing knowledge about the system and the specification in order to model only relevant features in the Kripke structure. Counterexample-guided abstraction refinement is an automatic abstraction method where, starting with a relatively small skeletal representation of the system to be verified, increasingly precise abstract representations of the system are computed. The key step is to extract information from false negatives ("spurious counterexamples") due to over-approximation.</description><identifier>ISSN: 1530-1311</identifier><identifier>ISBN: 0769519121</identifier><identifier>ISBN: 9780769519128</identifier><identifier>EISSN: 2332-6468</identifier><identifier>DOI: 10.1109/TIME.2003.1214874</identifier><language>eng</language><publisher>IEEE</publisher><subject>Boolean functions ; Collaboration ; Computer science ; Concrete ; Contracts ; Data mining ; Data structures ; Explosions ; State-space methods ; US Department of Defense</subject><ispartof>10th International Symposium on Temporal Representation and Reasoning, 2003 and Fourth International Conference on Temporal Logic. Proceedings, 2003, p.7-8</ispartof><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><linktohtml>$$Uhttps://ieeexplore.ieee.org/document/1214874$$EHTML$$P50$$Gieee$$H</linktohtml><link.rule.ids>309,310,780,784,789,790,2058,4050,4051,27925,54555,54920,54932</link.rule.ids><linktorsrc>$$Uhttps://ieeexplore.ieee.org/document/1214874$$EView_record_in_IEEE$$FView_record_in_$$GIEEE</linktorsrc></links><search><creatorcontrib>Clarke, E.</creatorcontrib><title>Counterexample-guided abstraction refinement</title><title>10th International Symposium on Temporal Representation and Reasoning, 2003 and Fourth International Conference on Temporal Logic. Proceedings</title><addtitle>TIME</addtitle><description>The main practical problem in model checking is the combinatorial explosion of system states commonly known as the state explosion problem. Abstraction methods attempt to reduce the size of the state space by employing knowledge about the system and the specification in order to model only relevant features in the Kripke structure. Counterexample-guided abstraction refinement is an automatic abstraction method where, starting with a relatively small skeletal representation of the system to be verified, increasingly precise abstract representations of the system are computed. The key step is to extract information from false negatives ("spurious counterexamples") due to over-approximation.</description><subject>Boolean functions</subject><subject>Collaboration</subject><subject>Computer science</subject><subject>Concrete</subject><subject>Contracts</subject><subject>Data mining</subject><subject>Data structures</subject><subject>Explosions</subject><subject>State-space methods</subject><subject>US Department of Defense</subject><issn>1530-1311</issn><issn>2332-6468</issn><isbn>0769519121</isbn><isbn>9780769519128</isbn><fulltext>true</fulltext><rsrctype>conference_proceeding</rsrctype><creationdate>2003</creationdate><recordtype>conference_proceeding</recordtype><sourceid>6IE</sourceid><recordid>eNotT8tOwzAQtHhIhNIPQFz6ATjd9TpOfERRgUqtuJRz5cRrZNSkVZJK8PdYonOZw4zmIcQjQo4Idrlbb1e5AqAcFeqq1FciU0RKGm2qa3EPpbEF2iTeiAwLAomEeCfm4_gNCWSNKVQmnuvjuZ944B_XnQ4sv87Rs1-4ZpwG107x2C8GDrHnjvvpQdwGdxh5fuGZ-Hxd7ep3ufl4W9cvGxkVVpM0wQaNDJo0pxGFDY5L7xpog268g8aWqFJ7mXYRNAYNs06mlqrKB480E0__uZGZ96chdm743V-O0h-uY0S-</recordid><startdate>2003</startdate><enddate>2003</enddate><creator>Clarke, E.</creator><general>IEEE</general><scope>6IE</scope><scope>6IL</scope><scope>CBEJK</scope><scope>RIE</scope><scope>RIL</scope></search><sort><creationdate>2003</creationdate><title>Counterexample-guided abstraction refinement</title><author>Clarke, E.</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-i218t-6f9f41e0434e95159fae7dab0cf4bda0b9712652715330b616ee49fac388dfd13</frbrgroupid><rsrctype>conference_proceedings</rsrctype><prefilter>conference_proceedings</prefilter><language>eng</language><creationdate>2003</creationdate><topic>Boolean functions</topic><topic>Collaboration</topic><topic>Computer science</topic><topic>Concrete</topic><topic>Contracts</topic><topic>Data mining</topic><topic>Data structures</topic><topic>Explosions</topic><topic>State-space methods</topic><topic>US Department of Defense</topic><toplevel>online_resources</toplevel><creatorcontrib>Clarke, E.</creatorcontrib><collection>IEEE Electronic Library (IEL) Conference Proceedings</collection><collection>IEEE Proceedings Order Plan All Online (POP All Online) 1998-present by volume</collection><collection>IEEE Xplore All Conference Proceedings</collection><collection>IEEE Xplore (Online service)</collection><collection>IEEE Proceedings Order Plans (POP All) 1998-Present</collection></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext_linktorsrc</fulltext></delivery><addata><au>Clarke, E.</au><format>book</format><genre>proceeding</genre><ristype>CONF</ristype><atitle>Counterexample-guided abstraction refinement</atitle><btitle>10th International Symposium on Temporal Representation and Reasoning, 2003 and Fourth International Conference on Temporal Logic. Proceedings</btitle><stitle>TIME</stitle><date>2003</date><risdate>2003</risdate><spage>7</spage><epage>8</epage><pages>7-8</pages><issn>1530-1311</issn><eissn>2332-6468</eissn><isbn>0769519121</isbn><isbn>9780769519128</isbn><abstract>The main practical problem in model checking is the combinatorial explosion of system states commonly known as the state explosion problem. Abstraction methods attempt to reduce the size of the state space by employing knowledge about the system and the specification in order to model only relevant features in the Kripke structure. Counterexample-guided abstraction refinement is an automatic abstraction method where, starting with a relatively small skeletal representation of the system to be verified, increasingly precise abstract representations of the system are computed. The key step is to extract information from false negatives ("spurious counterexamples") due to over-approximation.</abstract><pub>IEEE</pub><doi>10.1109/TIME.2003.1214874</doi><tpages>2</tpages><oa>free_for_read</oa></addata></record>
fulltext fulltext_linktorsrc
identifier ISSN: 1530-1311
ispartof 10th International Symposium on Temporal Representation and Reasoning, 2003 and Fourth International Conference on Temporal Logic. Proceedings, 2003, p.7-8
issn 1530-1311
2332-6468
language eng
recordid cdi_ieee_primary_1214874
source IEEE Xplore All Conference Series
subjects Boolean functions
Collaboration
Computer science
Concrete
Contracts
Data mining
Data structures
Explosions
State-space methods
US Department of Defense
title Counterexample-guided abstraction refinement
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2024-12-29T09%3A36%3A42IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-ieee_CHZPO&rft_val_fmt=info:ofi/fmt:kev:mtx:book&rft.genre=proceeding&rft.atitle=Counterexample-guided%20abstraction%20refinement&rft.btitle=10th%20International%20Symposium%20on%20Temporal%20Representation%20and%20Reasoning,%202003%20and%20Fourth%20International%20Conference%20on%20Temporal%20Logic.%20Proceedings&rft.au=Clarke,%20E.&rft.date=2003&rft.spage=7&rft.epage=8&rft.pages=7-8&rft.issn=1530-1311&rft.eissn=2332-6468&rft.isbn=0769519121&rft.isbn_list=9780769519128&rft_id=info:doi/10.1109/TIME.2003.1214874&rft_dat=%3Cieee_CHZPO%3E1214874%3C/ieee_CHZPO%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-i218t-6f9f41e0434e95159fae7dab0cf4bda0b9712652715330b616ee49fac388dfd13%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_id=info:pmid/&rft_ieee_id=1214874&rfr_iscdi=true