{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:01:04Z","timestamp":1762459264543,"version":"3.41.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2015,1,21]],"date-time":"2015-01-21T00:00:00Z","timestamp":1421798400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ProFun project"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2015,1,21]]},"abstract":"<jats:p>Psi-calculi is a parametric framework for extensions of the pi-calculus with arbitrary data and logic. All instances of the framework inherit machine-checked proofs of the metatheory such as compositionality and bisimulation congruence. We present a generic analysis tool for psi-calculus instances, enabling symbolic execution and (bi)simulation checking for both unicast and broadcast communication. The tool also provides a library for implementing new psi-calculus instances. We provide examples from traditional communication protocols and wireless sensor networks. We also describe the theoretical foundations of the tool, including an improved symbolic operational semantics, with additional support for scoped broadcast communication.<\/jats:p>","DOI":"10.1145\/2682570","type":"journal-article","created":{"date-parts":[[2015,1,28]],"date-time":"2015-01-28T14:05:51Z","timestamp":1422453951000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["The Psi-Calculi Workbench"],"prefix":"10.1145","volume":"14","author":[{"given":"Johannes","family":"Borgstrom","sequence":"first","affiliation":[{"name":"Uppsala University, Sweden"}]},{"given":"Ram\u016bnas","family":"Gutkovas","sequence":"additional","affiliation":[{"name":"Uppsala University, Sweden"}]},{"given":"Ioana","family":"Rodhe","sequence":"additional","affiliation":[{"name":"Uppsala University, Sweden"}]},{"given":"Bj\u00f6rn","family":"Victor","sequence":"additional","affiliation":[{"name":"Uppsala University, Sweden"}]}],"member":"320","published-online":{"date-parts":[[2015,1,21]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360213"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/266420.266432"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/362946.362970"},{"volume-title":"Psi-calculi: A framework for mobile processes with nominal data and logic. Logical Methods Comput. Sci. 7, 1","year":"2011","author":"Bengtson Jesper","key":"e_1_2_2_5_1"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_9"},{"volume-title":"Formal Models and Techniques for Analyzing Security Protocols, V\u00e9ronique Cortier and Steve Kremer (Eds.).","author":"Blanchet Bruno","key":"e_1_2_2_7_1"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0032"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2013.22"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/2075679.2075688"},{"volume-title":"Software and Systems Modeling","year":"2013","author":"Borgstr\u00f6m Johannes","key":"e_1_2_2_11_1"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1762174.1762179"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/941344.941346"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151648"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_15"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2008.25"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13414-2_1"},{"key":"e_1_2_2_18_1","unstructured":"Ram\u016bnas Gutkovas and Johannes Borgstr\u00f6m. 2013. The Psi-Calculi Workbench. Retrieved from http:\/\/www.it.uu.se\/research\/group\/mobility\/applied\/psiworkbench.  Ram\u016bnas Gutkovas and Johannes Borgstr\u00f6m. 2013. The Psi-Calculi Workbench. Retrieved from http:\/\/www.it.uu.se\/research\/group\/mobility\/applied\/psiworkbench."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00172-F"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_5"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.30"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.01.001"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/646731.703698"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02951922"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2011.19"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/844128.844142"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.039"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90009-5"},{"key":"e_1_2_2_30_1","doi-asserted-by":"crossref","unstructured":"Joachim Parrow Johannes Borgstr\u00f6m Palle Raabjerg and Johannes \u00c5man Pohjola. 2013. Higher-order psi-calculi. Math. Struct. Comput. Sci. FirstView (June 2013) 1--37. DOI: http:\/\/dx.doi.org\/10.1017\/S0960129513000170  Joachim Parrow Johannes Borgstr\u00f6m Palle Raabjerg and Johannes \u00c5man Pohjola. 2013. Higher-order psi-calculi. Math. Struct. Comput. Sci. FirstView (June 2013) 1--37. DOI: http:\/\/dx.doi.org\/10.1017\/S0960129513000170","DOI":"10.1017\/S0960129513000170"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"e_1_2_2_32_1","unstructured":"PolyML. 2013. Poly\/ML. Retrieved from http:\/\/www.polyml.org.  PolyML. 2013. Poly\/ML. Retrieved from http:\/\/www.polyml.org."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2009.32"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_4"},{"key":"e_1_2_2_35_1","volume-title":"Proc. of CAV\u201994","volume":"818","author":"Victor Bj\u00f6rn","year":"1994"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.03.017"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2682570","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2682570","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:14:07Z","timestamp":1750277647000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2682570"}},"subtitle":["A Generic Tool for Applied Process Calculi"],"short-title":[],"issued":{"date-parts":[[2015,1,21]]},"references-count":35,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,1,21]]}},"alternative-id":["10.1145\/2682570"],"URL":"https:\/\/doi.org\/10.1145\/2682570","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2015,1,21]]},"assertion":[{"value":"2013-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-01-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}