{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:55:45Z","timestamp":1673477745132},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2003,8,1]],"date-time":"2003-08-01T00:00:00Z","timestamp":1059696000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["STTT"],"published-print":{"date-parts":[[2003,8]]},"DOI":"10.1007\/s100090100071","type":"journal-article","created":{"date-parts":[[2004,3,20]],"date-time":"2004-03-20T15:13:37Z","timestamp":1079795617000},"page":"405-420","source":"Crossref","is-referenced-by-count":21,"title":["A verification tool for ERLANG"],"prefix":"10.1007","volume":"4","author":[{"given":"Lars\u2013\u00c5ke","family":"Fredlund","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dilian","family":"Gurov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Noll","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mads","family":"Dam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Arts","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gennady","family":"Chugunov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,8,1]]},"reference":[{"key":"71_CITArm-Vir-Wik-Wil-96","unstructured":"Armstrong J., Virding R., Wikstr\u00f6m C., Williams M.: Concurrent programming in Erlang. Prentice-Hall, London, 2nd edn, 1996"},{"key":"71_CITMnesia99","doi-asserted-by":"crossref","unstructured":"Arts T., Dam M.: Verifying a distributed database lookup manager written in Erlang. In: Wing J.M., Woodcock J., Davies J., (eds.), Formal Methods Europe (FM\u201999), Lecture Notes in Computer Science, vol. 1708. Springer, Berlin Heidelberg New York, 1999, pp. 682\u2013700","DOI":"10.1007\/3-540-48119-2_38"},{"key":"71_CITArts-Dam-Fre-Gur-98","doi-asserted-by":"crossref","unstructured":"Arts T., Dam M., Fredlund L.-\u00c5., Gurov D.: System description: verification of distributed Erlang programs. In: Proc. CADE\u201998, Lecture Notes in Computer Science, vol. 1421. Springer, Berlin Heidelberg New York, 1998, pp. 38\u201341","DOI":"10.1007\/BFb0054244"},{"key":"71_CITArts-Nol-01","unstructured":"Arts T., Noll T.: Verifying generic Erlang client\u2013server implementations. In: Proc. 12th Int. Workshop on the Implementation of Functional Languages (IFL\u201900), Lecture Notes in Computer Science, vol. 2011. Springer, Berlin Heidelberg New York, 2001, pp. 37\u201352"},{"issue":"7","key":"71_CITBerThe98","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1006\/jsco.1997.0171","volume":"25","author":"Y. Bertot","year":"1998","unstructured":"Bertot Y., Thery L.: A generic approach to building user interfaces for theorem provers. J Symbolic Comput 25(7):161\u2013194, 1998","journal-title":"J Symbolic Comput"},{"key":"71_CITNuPrl","unstructured":"Constable R.L., Allen S.F., Bromley H.M., Cleaveland W.R., Cremer J.F., Harper R.W., Howe D.J., Knoblock T.B., Mendler N.P, Panangaden P., Sasaki J.T., Smith S.F.: Implementing mathematics with the Nuprl proof development system. Prentice-Hall, Englewood Cliffs, N.J., USA, 1986"},{"key":"71_CITDam-98-Dyn","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1006\/inco.1997.2680","volume":"140","author":"M. Dam","year":"1998","unstructured":"Dam M.: Proving properties of dynamic process networks. Inf Computat 140:95\u2013114, 1998","journal-title":"Inf Computat"},{"key":"71_CITDam-Fre-Gur-98","doi-asserted-by":"crossref","unstructured":"Dam M., Fredlund L.-\u00c5., Gurov D.: Toward parametric verification of open distributed systems. In: Langmaack H., Pnueli A., de Roever W.-P., (eds), Compositionality: the significant difference, Lecture Notes in Computer Science, vol. 1536. Springer, Berlin Heidelberg New York, 1998, pp. 150\u2013185","DOI":"10.1007\/3-540-49213-5_7"},{"key":"71_CITDam-Gur-99A","unstructured":"Dam M., Gurov D.: Compositional verification of CCS processes. In: Proc. PSI\u201999, Lecture Notes in Computer Science, vol. 1705. Springer, Berlin Heidelberg New York, 1999, pp. 247\u2013256"},{"key":"71_CITDam-Gur-99","unstructured":"Dam M., Gurov D.: \u03bc-calculus with explicit points and approximations. In: Proc. FICS\u20192000, 2000"},{"key":"71_CITCOQ","unstructured":"Dowek G., Felty A., Herbelin H., Huet G., Murthy C., Parent C., Paulin-Mohring C., Werner B.: The Coq proof assistant user\u2019s guide version 5.8. Technical Report 154, INRIA, 1993"},{"key":"71_CITFre-01","unstructured":"Fredlund L.-\u00c5.: A Framework for Reasoning about Erlang Code. PhD thesis, Department of Microelectronics and Information Technology, Royal Institute of Technology, 2001. KTH\/IT\/AVH\u201301\/04\u2013SE"},{"key":"71_CITFre-Gur-Nol-01","unstructured":"Fredlund L.-\u00c5., Gurov D., Noll T.: The Erlang Verification Tool. In: Proc. 7th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901), Lecture Notes in Computer Science, vol. 2031. Springer, Berlin Heidelberg New York, 2001, pp. 582\u2013585"},{"key":"71_CITFre-Gur-99","doi-asserted-by":"crossref","unstructured":"Fredlund L.-\u00c5., Gurov D.: A framework for formal reasoning about open distributed systems. In: Proc. ASIAN\u201999, Lecture Notes in Computer Science, vol. 1742. Springer, Berlin Heidelberg New York, 1999, pp. 87\u2013100","DOI":"10.1007\/3-540-46674-6_9"},{"key":"71_CITdaVinci","unstructured":"Fr\u00f6hlich M., Werner M.: The graph visualization system daVinci \u2013 a user interface for applications. Technical Report 5\/94, Department of Computer Science; Universit\u00e4t Bremen, 1994"},{"key":"71_CITHOL","unstructured":"Gordon M.J.C., Melham T.F. (eds.): Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University, Cambridge, UK, 1993"},{"key":"71_CITGur-Chu-00","unstructured":"Gurov D., Chugunov G.: Verification of Erlang programs: factoring out the side-effect-free fragment. In: Proc. FMICS 2000, GMD Report No.91, pp. 109\u2013122, 2000"},{"key":"71_CITHoa-69","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare C.A.R.: An axiomatic basis for computer programming. Comm ACM 12:576\u2013580, 1969","journal-title":"Comm ACM"},{"key":"71_CITHuc-99","doi-asserted-by":"crossref","unstructured":"Huch F.: Verification of Erlang programs using abstract interpretation and model checking. In: Proc. ICFP \u201999, ACM SIGPLAN Notices, 34(9):261\u2013272, 1999","DOI":"10.1145\/317765.317908"},{"key":"71_CITKoz-83","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen D.: Results on the propositional \u03bc-calculus. Theoret Comput Sci 27:333\u2013354, 1983","journal-title":"Theoret Comput Sci"},{"key":"71_CITMil-89","unstructured":"Milner R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs, N.J., USA, 1989"},{"key":"71_CITsml","doi-asserted-by":"crossref","unstructured":"Milner R., Tofte M., Harper R.: The definition of Standard ML \u2013 revised. MIT, Boston, Mass., USA, 1997","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"71_CITNec-97","doi-asserted-by":"crossref","unstructured":"Necula G.C.: Proof\u2013carrying code. In: Proc. POPL\u201997, pp. 106\u2013119. ACM, 1997","DOI":"10.1145\/263699.263712"},{"key":"71_CITNil-99","unstructured":"Nilsson H.: Patent Application, 1999"},{"key":"71_CITOwr-et-al-96","doi-asserted-by":"crossref","unstructured":"Owre S., Rajan S., Rushby J.M., Shankar N., Srivas M.K. PVS: combining specification, proof checking, model checking. In: Proc. CAV\u201996, Lecture Notes in Computer Science, vol. 1102. Springer, Berlin Heidelberg New York, 1996, pp. 411\u2013414","DOI":"10.1007\/3-540-61474-5_91"},{"key":"71_CITPar-76","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0304-3975(76)90022-0","volume":"3","author":"D. Park","year":"1976","unstructured":"Park D.: Finiteness is mu-Ineffable. Theoret Comput Sci 3:173\u2013181, 1976","journal-title":"Theoret Comput Sci"},{"key":"71_CITIsabelle","doi-asserted-by":"crossref","unstructured":"Paulson L.C.: Isabelle: a generic theorem prover, Lecture Notes in Computer Science, vol. 828. Springer, Berlin Heidelberg New York, 1994","DOI":"10.1007\/BFb0030541"},{"key":"71_CITPlo-81","unstructured":"Plotkin G.D.: A structural approach to operational semantics. Aarhus University report DAIMI FN-19, 1981"},{"key":"71_CITsah","doi-asserted-by":"crossref","unstructured":"Sahlin D., Franz\u00e9n T., Haridi S.: An intuitionistic predicate logic theorem prover. In: J Logic Comput 2(5):619\u2013656, 1992","DOI":"10.1093\/logcom\/2.5.619"},{"key":"71_CITSim-95","doi-asserted-by":"crossref","unstructured":"Simpson A.: Compositionality via cut-elimination: Hennessy-Milner logic for an arbitrary GSOS. In: Proc. LICS, pp. 420\u2013430. IEEE Computer Society, New York, 1995","DOI":"10.1109\/LICS.1995.523276"},{"key":"71_CITWik-Nil-Mat-97","unstructured":"Wikstr\u00f6m C., Nilsson H., Mattson H.: Mnesia database management system. In: Open Telecom Platform Users Manual. Open Systems, Ericsson Utvecklings, Stockholm, Sweden, 1997"},{"key":"71_CITWin-91","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/0304-3975(91)90043-2","volume":"83","author":"G. Winskel","year":"1991","unstructured":"Winskel G.: A note on model checking the modal \u03bd-calculus. Theoret Comput Sci 83:157\u2013187, 1991","journal-title":"Theoret Comput Sci"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s100090100071.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s100090100071\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s100090100071","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s100090100071.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,31]],"date-time":"2020-03-31T18:10:54Z","timestamp":1585678254000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s100090100071"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,8]]},"references-count":32,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2003,8]]}},"alternative-id":["71"],"URL":"https:\/\/doi.org\/10.1007\/s100090100071","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,8]]}}}