{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T01:30:30Z","timestamp":1785202230210,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642288906","type":"print"},{"value":"9783642288913","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28891-3_28","type":"book-chapter","created":{"date-parts":[[2012,3,30]],"date-time":"2012-03-30T12:53:01Z","timestamp":1333111981000},"page":"279-294","source":"Crossref","is-referenced-by-count":12,"title":["Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Bruttomesso","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alessandro","family":"Carioni","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Silvio","family":"Ghilardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1007\/978-3-540-71209-1_56","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2007","unstructured":"Abdulla, P.A., Delzanno, G., Ben Henda, N., Rezine, A.: Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems). In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 721\u2013736. Springer, Heidelberg (2007)"},{"key":"28_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-540-73368-3_17","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"2007","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, A.: Parameterized Verification of Infinite-State Processes with Global Conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 145\u2013157. Springer, Heidelberg (2007)"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B.: Model checking of systems with many identical timed processes. Theoretical Computer Science, pp. 241\u2013264 (2003)","DOI":"10.1016\/S0304-3975(01)00330-9"},{"key":"28_CR4","first-page":"29","volume":"8","author":"F. Alberti","year":"2012","unstructured":"Alberti, F., Ghilardi, S., Pagani, E., Ranise, S., Rossi, G.P.: Universal Guards, Relativization of Quantifiers, and Failure Models in Model Checking Modulo Theories. JSAT\u00a08, 29\u201361 (2012), http:\/\/jsat.ewi.tudelft.nl\/content\/volume8\/JSAT8_2_Alberti.pdf","journal-title":"JSAT"},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/11691372_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G.M. Brown","year":"2006","unstructured":"Brown, G.M., Pike, L.: Easy Parameterized Verification of Biphase Mark and 8N1 Protocols. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 58\u201372. Springer, Heidelberg (2006)"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"Carioni, A., Bruttomesso, R., Ghilardi, S., Ranise, S.: Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms (Extended Version) (2012), http:\/\/www.oprover.org\/mcmt_lynch_shavit.html","DOI":"10.1007\/978-3-642-28891-3_28"},{"key":"28_CR7","unstructured":"Carioni, A., Ghilardi, S., Ranise, S.: MCMT in the Land of Parametrized Timed Automata. In: Proc. of VERIFY 2010 (2010)"},{"key":"28_CR8","unstructured":"Dutertre, B., Sorea, M.: Timed systems in sal. Technical Report SRI-SDL-04-03, SRI International, Menlo Park, CA (2004)"},{"key":"28_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-642-16265-7_12","volume-title":"Integrated Formal Methods","author":"J. Faber","year":"2010","unstructured":"Faber, J., Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: Automatic Verification of Parametric Specifications with Complex Topologies. In: M\u00e9ry, D., Merz, S. (eds.) IFM 2010. LNCS, vol.\u00a06396, pp. 152\u2013167. Springer, Heidelberg (2010)"},{"issue":"3","key":"28_CR10","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10009-005-0193-x","volume":"8","author":"Y. Fang","year":"2006","unstructured":"Fang, Y., Piterman, N., Pnueli, A., Zuck, L.D.: Liveness with invisible ranking. Software Tools for Technology\u00a08(3), 261\u2013279 (2006)","journal-title":"Software Tools for Technology"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT-solving: termination and invariant synthesis. LMCS\u00a06(4) (2010), http:\/\/www.lmcs-online.org\/ojs\/viewarticle.php?id=694&layout=abstract","DOI":"10.2168\/LMCS-6(4:10)2010"},{"key":"28_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-14203-1_3","volume-title":"Automated Reasoning","author":"S. Ghilardi","year":"2010","unstructured":"Ghilardi, S., Ranise, S.: MCMT: A Model Checker Modulo Theories. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 22\u201329. Springer, Heidelberg (2010)"},{"key":"28_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/3-540-45319-9_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Hune","year":"2001","unstructured":"Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear Parametric Model Checking of Timed Automata. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 189\u2013203. Springer, Heidelberg (2001)"},{"key":"28_CR14","unstructured":"Krstic, S.: Parameterized system verification with guard strengthening and parameter abstraction. In: AVIS (2005)"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Bryant, R.E.: Predicate abstraction with indexed predicates. ACM Transactions on Computational Logic (TOCL)\u00a09(1) (2007)","DOI":"10.1145\/1297658.1297662"},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"Lynch, N.A., Shavit, N.: Timing-based mutual exclusion. In: Proc. of IEEE Real-Time Systems Symposium, pp. 2\u201311 (1992)","DOI":"10.1109\/REAL.1992.242681"},{"key":"28_CR17","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann (1996)"},{"key":"28_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.D.: Automatic Deductive Verification with Invisible Invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"key":"28_CR19","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB Standard: Version 1.2. Technical report (2006), http:\/\/www.SMT-LIB.org\/papers"},{"key":"28_CR20","doi-asserted-by":"crossref","unstructured":"Steiner, W., Dutertre, B.: Automated Formal Verification of the TTEthernet Synchronization Quality. In: Proc. of the NASA Formal Methods Symposium (2011)","DOI":"10.1007\/978-3-642-20398-5_27"},{"key":"28_CR21","doi-asserted-by":"crossref","unstructured":"Talupur, M., Tuttle, M.: Going with the flow: Parameterized verification using message flows. In: Proc. of FMCAD 2008, pp. 1\u20138 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.14"},{"key":"28_CR22","unstructured":"MCMT web site, http:\/\/www.dsi.unimi.it\/~ghilardi\/mcmt\/"},{"key":"28_CR23","unstructured":"Uppaal, http:\/\/www.uppaal.com"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28891-3_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,24]],"date-time":"2025-03-24T13:58:17Z","timestamp":1742824697000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28891-3_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288906","9783642288913"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28891-3_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}