{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:05Z","timestamp":1753889765679,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2007,2,26]],"date-time":"2007-02-26T00:00:00Z","timestamp":1172448000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We propose an abstraction-based model checking method which relies on\nrefinement of an under-approximation of the feasible behaviors of the system\nunder analysis. The method preserves errors to safety properties, since all\nanalyzed behaviors are feasible by definition. The method does not require an\nabstract transition relation to be generated, but instead executes the concrete\ntransitions while storing abstract versions of the concrete states, as\nspecified by a set of abstraction predicates. For each explored transition the\nmethod checks, with the help of a theorem prover, whether there is any loss of\nprecision introduced by abstraction. The results of these checks are used to\ndecide termination or to refine the abstraction by generating new abstraction\npredicates. If the (possibly infinite) concrete system under analysis has a\nfinite bisimulation quotient, then the method is guaranteed to eventually\nexplore an equivalent finite bisimilar structure. We illustrate the application\nof the approach for checking concurrent programs.<\/jats:p>","DOI":"10.2168\/lmcs-3(1:5)2007","type":"journal-article","created":{"date-parts":[[2008,6,3]],"date-time":"2008-06-03T14:44:50Z","timestamp":1212504290000},"source":"Crossref","is-referenced-by-count":8,"title":["Predicate Abstraction with Under-approximation Refinement"],"prefix":"10.46298","volume":"Volume 3, Issue 1","author":[{"given":"Corina S.","family":"Pasareanu","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8877-4729","authenticated-orcid":false,"given":"Radek","family":"Pelanek","sequence":"additional","affiliation":[]},{"given":"Willem","family":"Visser","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2007,2,26]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/2227\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/2227\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:10:02Z","timestamp":1681243802000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/2227"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,2,26]]},"references-count":0,"URL":"https:\/\/doi.org\/10.2168\/lmcs-3(1:5)2007","relation":{"is-same-as":[{"id-type":"arxiv","id":"cs\/0701140","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.cs\/0701140","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2007,2,26]]},"article-number":"2227"}}