{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T08:07:38Z","timestamp":1777536458289,"version":"3.51.4"},"reference-count":9,"publisher":"World Scientific Pub Co Pte Lt","issue":"06","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[2007,12]]},"abstract":"<jats:p> We describe a method of automating invariant verification of behavioral specifications, which are algebraic specifications of abstract machines. The proposed method is based on fixed-point computation, which is one of the standard techniques for automatic (invariant) verification. The proposed method has some notable features. Among them are as follow: <\/jats:p><jats:p> (1) the method finds and uses as lemmas state predicates whose invariant proofs may (even mutually) depend on other state predicates whose invariant proofs may not be completed, and <\/jats:p><jats:p> (2) the method finds a counterexample showing that an abstract machine does not satisfy an invariant property if any, which does not need to make the (reachable) state space of the abstract machine finite. <\/jats:p><jats:p> Cr\u00e8me is a tool based on the proposed method. We also report on two case studies in which <\/jats:p><jats:p> (1) Cr\u00e8me proves fully automatically that the NSLPK authentication protocol satisfies the secrecy property and <\/jats:p><jats:p> (2) Cr\u00e8me finds a counterexample showing that the NSPK authentication protocol does not satisfy the secrecy property. <\/jats:p>","DOI":"10.1142\/s0218194007003458","type":"journal-article","created":{"date-parts":[[2008,2,4]],"date-time":"2008-02-04T10:07:30Z","timestamp":1202119650000},"page":"783-804","source":"Crossref","is-referenced-by-count":12,"title":["CR\u00c8ME: AN AUTOMATIC INVARIANT PROVER OF BEHAVIORAL SPECIFICATIONS"],"prefix":"10.1142","volume":"17","author":[{"given":"MASAHIRO","family":"NAKANO","sequence":"first","affiliation":[{"name":"Graduate School of Information Science, Japan Advanced Institute of Science and Technology (JAIST), 1-1 Asahidai, Nomi, Ishikawa 923-1292, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"KAZUHIRO","family":"OGATA","sequence":"additional","affiliation":[{"name":"Graduate School of Information Science, Japan Advanced Institute of Science and Technology (JAIST), 1-1 Asahidai, Nomi, Ishikawa 923-1292, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"MASAKI","family":"NAKAMURA","sequence":"additional","affiliation":[{"name":"Graduate School of Information Science, Japan Advanced Institute of Science and Technology (JAIST), 1-1 Asahidai, Nomi, Ishikawa 923-1292, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"KOKICHI","family":"FUTATSUGI","sequence":"additional","affiliation":[{"name":"Graduate School of Information Science, Japan Advanced Institute of Science and Technology (JAIST), 1-1 Asahidai, Nomi, Ishikawa 923-1292, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2011,11,21]]},"reference":[{"key":"rf1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008744030390"},{"key":"rf2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00359-0"},{"key":"rf5","first-page":"74","volume":"6","author":"Diaconescu R.","journal-title":"J. UCS"},{"key":"rf6","doi-asserted-by":"publisher","DOI":"10.1007\/BF00124891"},{"key":"rf9","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2704-5"},{"key":"rf12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"rf14","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359659"},{"key":"rf19","doi-asserted-by":"publisher","DOI":"10.1145\/24592.24594"},{"key":"rf23","first-page":"115","author":"Tseitin G. S.","journal-title":"Studies in Constructive Mathematics and Mathematical Logic"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194007003458","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T16:13:30Z","timestamp":1565194410000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218194007003458"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,12]]},"references-count":9,"journal-issue":{"issue":"06","published-online":{"date-parts":[[2011,11,21]]},"published-print":{"date-parts":[[2007,12]]}},"alternative-id":["10.1142\/S0218194007003458"],"URL":"https:\/\/doi.org\/10.1142\/s0218194007003458","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"value":"0218-1940","type":"print"},{"value":"1793-6403","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,12]]}}}