{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T15:02:27Z","timestamp":1694617347619},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[1999,12,1]],"date-time":"1999-12-01T00:00:00Z","timestamp":944006400000},"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":[[1999,12]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>The paper proposes an induction based approach, that employs automata as inductive invariants, for verifying safety and liveness properties of linear networks of arbitrary size. The proposed method has been shown to be complete for verifying safety properties. Automated methods that check for correcteness of such families of networks are proposed. These methods are based on generating an invariant automaton from the correctness property which is also specified by an automaton. These methods have been implemented and successfully tested on some examples.<\/jats:p>","DOI":"10.1007\/s001650050040","type":"journal-article","created":{"date-parts":[[2002,8,25]],"date-time":"2002-08-25T06:53:02Z","timestamp":1030258382000},"page":"402-425","source":"Crossref","is-referenced-by-count":6,"title":["Parameterized Verification of Linear Networks using Automata as Invariants"],"prefix":"10.1145","volume":"11","author":[{"given":"A.","family":"Prasad Sistla","sequence":"first","affiliation":[{"name":"Department of Electrical Engineering and Computer Science, The University of Illinois at Chicago, USA, , , , , , US"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Gyuris","sequence":"additional","affiliation":[{"name":"Department of Mathematics, Computer Science and Statistics, The University of Illinois at Chicago, USA, , , , , , US"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"issue":"6","key":"p_1","first-page":"307","article-title":"Limits to Automatic Program Verification","volume":"22","author":"Ap","year":"1986","journal-title":"Information Processing Letters"},{"key":"p_2","first-page":"1","volume-title":"Proceedings of International Cong. on Logic, Methodology and Philosophy of Science 1960","author":"Buc","year":"1962"},{"issue":"1","key":"p_3","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"Browne M.","year":"1989","journal-title":"Information and Computation"},{"key":"p_4","first-page":"5","article-title":"Verifying Parameterized Networks Using Abstraction and Regular Languages. CONCUR 95; revised version appeared","volume":"19","author":"Clarke E. M.","year":"1997","journal-title":"ACM TOPLAS"},{"key":"p_5","volume-title":"Proceedings of ACM Symposium on Principles of Distributed Computing","author":"Cl","year":"1987"},{"key":"p_6","volume-title":"Proceedings of 22nd POPL conference","author":"Em","year":"1995"},{"key":"p_7","volume-title":"Proceeding of the International Conference on Computer Aide Verification","author":"Em","year":"1996"},{"key":"p_8","first-page":"675","volume-title":"JACM","author":"Ge","year":"1992"},{"key":"p_9","first-page":"406","volume-title":"Proc 6th IEEE Symposium on Logic in Computer Science","author":"Go","year":"1991"},{"issue":"1","key":"p_10","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","article-title":"Algebraic Laws for Non-determinism and Concurrency","volume":"32","author":"He","year":"1985","journal-title":"Journal of the Association for Computing Machinery"},{"key":"p_11","volume-title":"Proceedings of 9th International Conference, CAV '97","author":"Kes","year":"1997"},{"key":"p_12","volume-title":"ACM Sym. on Principles of Distributed Computing","author":"Ku","year":"1989"},{"key":"p_13","volume-title":"Proceedings of ACM Symposium on Principles of Programming Languages","author":"Lesens D.","year":"1996"},{"key":"p_14","first-page":"481","volume-title":"IN Proceedings of 2nd International Joint Conference on Artificial Intelligence","author":"Mil","year":"1971"},{"key":"p_16","volume-title":"Reasoning About many Processes. LICS 87","author":"Si"},{"key":"p_17","volume-title":"Communication Behaviors and Automatic Verification. Proc. of International Workshop on Automatic Verification Methods for Finite State Systems","author":"Sh","year":"1989"},{"key":"p_18","volume-title":"Proceedings of International Conference, CAV'97","author":"Sis","year":"1997"},{"key":"p_19","first-page":"217","volume-title":"Proceedings Of The 12th International Colloquium On Automata, Languages And Programming","author":"Sistla A. P.","year":"1987"},{"key":"p_20","volume-title":"J","author":"Tho","year":"1990"},{"key":"p_21","volume-title":"Proc. 1989 Intl Workshop on Automatic Verification Methods for Finite State Systems","author":"Wo","year":"1989"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650050040.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650050040\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650050040","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:31:59Z","timestamp":1641483119000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650050040"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,12]]},"references-count":20,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1999,12]]}},"alternative-id":["10.1007\/s001650050040"],"URL":"https:\/\/doi.org\/10.1007\/s001650050040","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,12]]}}}