{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:03Z","timestamp":1761611163532},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2005,8,1]],"date-time":"2005-08-01T00:00:00Z","timestamp":1122854400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2005,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a symbolic model checking approach that allows verifying a unit of code, e.g., a single procedure or a collection of procedures that interact with each other. We allow temporal specifications that assert over both the<jats:italic>program counters<\/jats:italic>and the<jats:italic>program variables<\/jats:italic>. We decompose the verification into two parts: (1) a search that is based on the temporal behavior of the<jats:italic>program counters<\/jats:italic>, and (2) the formulation and refutation of a path condition, which inherits conditions constraining the<jats:italic>program variables<\/jats:italic>from the temporal specification. This verification approach is modular, as we do not require that all the involved procedures are provided. Furthermore, we do not request that the code is based on a finite domain. The presented approach can also be used for automating the generation of test cases for unit testing.<\/jats:p>","DOI":"10.1007\/s00165-005-0059-8","type":"journal-article","created":{"date-parts":[[2005,8,4]],"date-time":"2005-08-04T13:19:21Z","timestamp":1123161561000},"page":"201-221","source":"Crossref","is-referenced-by-count":25,"title":["Model checking, testing and verification working together"],"prefix":"10.1145","volume":"17","author":[{"given":"Elsa","family":"Gunter","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Illinois at Urbana\u2013Champaign, 61801-2302, Urbana, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[{"name":"Dept. of Computer Science, The University of Warwick, CV4 7AL, Coventry, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","doi-asserted-by":"crossref","first-page":"747","DOI":"10.1145\/325478.325480","article-title":"Model-checking concurrent systems with unbounded integer variables: symbolic representation, and experimental results","volume":"21","author":"Bultan T","year":"1999","journal-title":"ACM Trans Program Syst"},{"key":"p_2","volume-title":"Model checking","author":"Clarke EM","year":"2000"},{"issue":"8","key":"p_3","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","article-title":"Guarded commands, nondeterminacy and formal derivation of programs","volume":"18","author":"Dij EW","year":"1975","journal-title":"Commun ACM"},{"key":"p_4","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1145\/512529.512558","volume-title":"PLDI","author":"Flanagan C","year":"2002"},{"key":"p_5","doi-asserted-by":"crossref","first-page":"1203","DOI":"10.1002\/1097-024X(200009)30:11<1203::AID-SPE338>3.0.CO;2-N","article-title":"An open graph visualization system and its applications to software engineering","volume":"30","author":"Gansner ER","year":"2000","journal-title":"Softw Pract Exp"},{"key":"p_6","first-page":"431","volume-title":"TACAS","author":"Gunter EL","year":"2002"},{"key":"p_7","first-page":"3","volume-title":"Protocol Specification Testing and Verification","author":"Gerth R","year":"1995"},{"key":"p_8","doi-asserted-by":"crossref","first-page":"564","DOI":"10.1145\/357114.357119","article-title":"Assignment and procedure call proof rules","volume":"2","author":"Gries D","year":"1980","journal-title":"ACM Trans Program Lang Sys"},{"key":"p_9","volume-title":"Introduction to HOL","author":"Gordon MJC","year":"1993"},{"key":"p_10","first-page":"327","article-title":"A temporal logic based theory of test coverage and generation, tools and algorithms for the construction and analysis of systems, Grenoble, France","volume":"2280","author":"Hong HS","year":"2002","journal-title":"LNCS"},{"key":"p_11","doi-asserted-by":"crossref","unstructured":"[KPV01] Kesten Y Pnueli A Vardi MY ( 2001 ) Verification by augmented abstraction: the automata-theoretic view JCSS 62 : 668 - 690","DOI":"10.1006\/jcss.2000.1744"},{"key":"p_12","volume-title":"Computer-aided reasoning: an approach","author":"Kaufmann M","year":"2000"},{"issue":"7","key":"p_13","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","article-title":"Symbolic execution and program testing","volume":"17","author":"King JC","year":"1976","journal-title":"Commun ACM"},{"issue":"2","key":"p_14","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1017\/S0956796899003421","article-title":"Functional design and implementation of graphical user interfaces for theorem provers","volume":"9","author":"Lue C","year":"1999","journal-title":"J Funct Program"},{"key":"p_15","volume-title":"Hilbert's tenth problem","author":"Mat Y","year":"1993"},{"key":"p_16","volume-title":"The art of software testing","author":"Mye GJ","year":"1979"},{"key":"p_17","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","article-title":"Completing the temporal picture","volume":"83","author":"Manna Z","year":"1991","journal-title":"Theor Comput Sci"},{"key":"p_18","volume-title":"Berlin Heidelberg New York","author":"Manna Z","year":"1991"},{"key":"p_19","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The definition of standard ML (revised)","author":"Milner R","year":"1997"},{"issue":"3","key":"p_20","first-page":"323","article-title":"A 222pn upper bound on the complexity of Presburger arithmetic","volume":"16","author":"Opp DC","year":"1978","journal-title":"JCSS"},{"key":"p_21","volume-title":"Software reliability methods","author":"Pel D","year":"2002"},{"key":"p_22","volume-title":"Runtime Verification","author":"Peled D","year":"2004"},{"key":"p_23","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1109\/TSE.1985.232226","article-title":"Selecting software test data using data flow information","volume":"4","author":"Rapps S","year":"1985","journal-title":"IEEE Trans softw Eng SE-11"},{"issue":"9","key":"p_24","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1109\/32.713327","article-title":"Subtypes for specifications: predicate subtyping in PVS","volume":"24","author":"Rushby JM","year":"1998","journal-title":"Trans Softw Eng"},{"key":"p_25","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1109\/71.342135","article-title":"Going beyond integer programming with the omega test to eliminate false data dependencies","volume":"6","author":"Pugh W","year":"1995","journal-title":"IEEE Trans Parallel Distrib Sys"},{"key":"p_26","first-page":"149","volume-title":"Generating test data for functions with point input 17th IEEE international conference on automated software engineering","author":"Visvanathan S","year":"2002"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-005-0059-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-005-0059-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-005-0059-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,4]],"date-time":"2023-05-04T00:46:39Z","timestamp":1683161199000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-005-0059-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,8]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,8]]}},"alternative-id":["10.1007\/s00165-005-0059-8"],"URL":"https:\/\/doi.org\/10.1007\/s00165-005-0059-8","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,8]]}}}