{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T14:04:26Z","timestamp":1776261866893,"version":"3.50.1"},"publisher-location":"Cham","reference-count":103,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227485","type":"print"},{"value":"9783032227492","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22749-2_5","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T13:10:38Z","timestamp":1776258638000},"page":"85-108","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Deciding Serializability in Network Systems"],"prefix":"10.1007","author":[{"given":"Guy","family":"Amir","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Barbone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Amat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jules","family":"Jacobs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,15]]},"reference":[{"key":"5_CR1","unstructured":"The Rocq Prover. https:\/\/rocq-prover.org\/, accessed: 2025-12-13"},{"key":"5_CR2","unstructured":"CockroachDB: Revision 7. https:\/\/dbdb.io\/db\/cockroachdb\/revisions\/7 (2018), [Online; accessed 2025-10-02]"},{"key":"5_CR3","unstructured":"Supplementary Artifact (2025), https:\/\/zenodo.org\/records\/17253581"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Jonsson, B., Trinh, C.: Automated Verification of Linearization Policies. In: Proc. 23rd Int. Symposium on Static Analysis (SAS). pp. 61\u201383 (2016)","DOI":"10.1007\/978-3-662-53413-7_4"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Alur, R., McMillan, K., Peled, D.: Model-Checking of Correctness Conditions for Concurrent Objects. In: Proc. 11th ACM\/IEEE Symposium on Logic in Computer Science (LICS). pp. 219\u2013228 (1996)","DOI":"10.1109\/LICS.1996.561322"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Amat, N., Berthomieu, B., Dal\u00a0Zilio, S.: On the Combination of Polyhedral Abstraction and SMT-Based Model Checking for Petri Nets. In: Proc. 42nd Int. Conf. on Applications and Theory of Petri Nets and Concurrency (PETRI NETS). pp. 164\u2013185 (2021)","DOI":"10.1007\/978-3-030-76983-3_9"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Amat, N., Dal\u00a0Zilio, S.: SMPT: A Testbed for Reachability Methods in Generalized Petri Nets. In: Proc. 25th Int. Symposium on Formal Methods (FM). pp. 445\u2013453 (2023)","DOI":"10.1007\/978-3-031-27481-7_25"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Amat, N., Dal\u00a0Zilio, S., Berthomieu, B.: A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking. Fundamenta Informaticae 187 (2022)","DOI":"10.46298\/.8831"},{"key":"5_CR9","unstructured":"Amir, G., Barbone, M., Amat, N., Jacobs, J.: Deciding Serializability in Network Systems (2026), Technical Report. http:\/\/arxiv.org\/abs\/2601.02251"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Amit, D., Rinetzky, N., Reps, T., Sagiv, M., Yahav, E.: Comparison Under Abstraction for Verifying Linearizability. In: Proc. 19th Int. Conf. on Computer Aided Verification (CAV). pp. 477\u2013490 (2007)","DOI":"10.1007\/978-3-540-73368-3_49"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Berdine, J., Lev-Ami, T., Manevich, R., Ramalingam, G., Sagiv, M.: Thread Quantification for Concurrent Shape Analysis. In: Proc. 20th Int. Conf. on Computer Aided Verification (CAV). pp. 399\u2013413 (2008)","DOI":"10.1007\/978-3-540-70545-1_37"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Berthelot, G.: Transformations and Decompositions of Nets. In: Petri Nets: Central Models and their Properties. Springer (1987)","DOI":"10.1007\/978-3-540-47919-2_13"},{"key":"5_CR13","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/s10009-019-00519-1","volume":"22","author":"B Berthomieu","year":"2020","unstructured":"Berthomieu, B., Le Botlan, D., Dal Zilio, S.: Counting Petri Net Markings from Reduction Equations. International Journal on Software Tools for Technology Transfer (STTT) 22, 163\u2013181 (2020)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Proc. 5th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (1999)","DOI":"10.21236\/ADA360973"},{"key":"5_CR15","unstructured":"Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol.\u00a0185. IOS Press (2009)"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Biswas, R., Enea, C.: On the Complexity of Checking Transactional Consistency. In: Proc. ACM Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). pp. 1\u201328 (2019)","DOI":"10.1145\/3360591"},{"issue":"3","key":"5_CR17","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/2656877.2656890","volume":"44","author":"P Bosshart","year":"2014","unstructured":"Bosshart, P., Daly, D., Gibb, G., Izzard, M., McKeown, N., Rexford, J., Schlesinger, C., Talayco, D., Vahdat, A., Varghese, G., Walker, D.: P4: Programming Protocol-Independent Packet Processors. SIGCOMM Computer Communication Review 44(3), 87\u201395 (2014)","journal-title":"SIGCOMM Computer Communication Review"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Verifying Concurrent Programs Against Sequential Specifications. In: Proc. 22nd European Symposium on Programming (ESOP). pp. 290\u2013309 (2013)","DOI":"10.1007\/978-3-642-37036-6_17"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Tractable Refinement Checking for Concurrent Objects. In: Proc. 42nd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). pp. 651\u2013662 (2015)","DOI":"10.1145\/2676726.2677002"},{"key":"5_CR20","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1016\/j.ic.2018.02.014","volume":"261","author":"A Bouajjani","year":"2018","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: On Reducing Linearizability to State Reachability. Inf. Comput. 261, 383\u2013400 (2018)","journal-title":"Inf. Comput."},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Mutluergil, S.: Proving Linearizability Using Forward Simulations. In: Proc. 29th Int. Conf. on Computer Aided Verification (CAV). pp. 542\u2013563 (2017)","DOI":"10.1007\/978-3-319-63390-9_28"},{"key":"5_CR22","unstructured":"Bouajjani, A., Enea, C., Wang, C.: Checking Linearizability of Concurrent Priority Queues. In: Proc. 28th Int. Conf. on Concurrency Theory (CONCUR) (2017)"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Alur, R., Martin, M.: Checkfence: Checking Consistency of Concurrent Data Types on Relaxed Memory Models. In: Proc. 28th ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI). pp. 12\u201321 (2007)","DOI":"10.1145\/1250734.1250737"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: A Complete and Automatic Linearizability Checker. In: Proc. 31st ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI). pp. 330\u2013340 (2010)","DOI":"10.1145\/1806596.1806634"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Gotsman, A., Musuvathi, M., Yang, H.: Concurrent Library Correctness on the TSO Memory Model. In: Proc. 21st European Symposium on Programming (ESOP). pp. 87\u2013107 (2012)","DOI":"10.1007\/978-3-642-28869-2_5"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Burnim, J., Necula, G., Sen, K.: Specifying and Checking Semantic Atomicity for Multithreaded Programs. In: Proc. 16th Int. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS). pp. 79\u201390 (2011)","DOI":"10.1145\/1950365.1950377"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Burnim, J., Sen, K.: Asserting and Checking Determinism for Multithreaded Programs. In: Proc. 7th Symposium on the Foundations of Software Engineering (FSE). pp. 3\u201312 (2009)","DOI":"10.1145\/1595696.1595700"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"\u010cern\u1ef3, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., Alur, R.: Model Checking of Linearizability of Concurrent List Implementations. In: Proc. 22nd Int. Conf. on Computer Aided Verification (CAV). pp. 465\u2013479 (2010)","DOI":"10.1007\/978-3-642-14295-6_41"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Henzinger, T., Sezgin, A., Vafeiadis, V.: Aspect-Oriented Linearizability Proofs. Logical Methods in Computer Science 11 (2015)","DOI":"10.2168\/LMCS-11(1:20)2015"},{"key":"5_CR30","unstructured":"CockroachDB Contributors: GitHub Issue #14099: UPSERT Anomaly Under SNAPSHOT Isolation. https:\/\/github.com\/cockroachdb\/cockroach\/issues\/14099 (2018), [Online; accessed 2025-07-10]"},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"Cohen, A., O\u2019Leary, J., Pnueli, A., Tuttle, M., Zuck, L.: Verifying Correctness of Transactional Memories. In: Proc. 7th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD). pp. 37\u201344 (2007)","DOI":"10.1109\/FAMCAD.2007.40"},{"issue":"2","key":"5_CR32","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/j.entcs.2005.04.026","volume":"137","author":"R Colvin","year":"2005","unstructured":"Colvin, R., Doherty, S., Groves, L.: Verifying Concurrent Data Structures by Simulation. Electronic Notes in Theoretical Computer Science 137(2), 93\u2013110 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Colvin, R., Groves, L., Luchangco, V., Moir, M.: Formal Verification of a Lazy Concurrent List-Based Set Algorithm. In: Proc. 18th Int. Conf. on Computer Aided Verification (CAV). pp. 475\u2013488 (2006)","DOI":"10.1007\/11817963_44"},{"key":"5_CR34","doi-asserted-by":"crossref","unstructured":"Czerwi\u0144ski, W., Orlikowski, \u0141.: Reachability in Vector Addition Systems is Ackermann-Complete. In: Proc. 62nd Annual Symposium on Foundations of Computer Science (FOCS). pp. 1229\u20131240 (2022)","DOI":"10.1109\/FOCS52979.2021.00120"},{"key":"5_CR35","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Proc. 14th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A Storm is Coming: A Modern Probabilistic Model Checker. In: Proc. 29th Int. Conf. on Computer Aided Verification (CAV). pp. 592\u2013600 (2017)","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"5_CR37","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1889997.1890001","volume":"1","author":"J Derrick","year":"2011","unstructured":"Derrick, J., Schellhorn, G., Wehrheim, H.: Mechanically Verified Proof Obligations for Linearizability. ACM Transactions on Programming Languages and Systems (TOPLAS) 1, 1\u201343 (2011)","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"5_CR38","doi-asserted-by":"crossref","unstructured":"Drachsler-Cohen, D., Petrank, E.: LCD: Local Combining on Demand. In: Proc. 18th Int. Conf. on Principles of Distributed Systems (OPODIS). pp. 355\u2013371 (2014)","DOI":"10.1007\/978-3-319-14472-6_24"},{"key":"5_CR39","unstructured":"Emmi, M., Enea, C.: Exposing Non-Atomic Methods of Concurrent Objects (2017), Technical Report. http:\/\/arxiv.org\/abs\/1706.09305"},{"key":"5_CR40","doi-asserted-by":"crossref","unstructured":"Emmi, M., Enea, C.: Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections. In: Proc. 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). pp. 1\u201327 (2018)","DOI":"10.1145\/3158113"},{"key":"5_CR41","doi-asserted-by":"crossref","unstructured":"Emmi, M., Enea, C.: Violat: Generating Tests of Observational Refinement for Concurrent Objects. In: Proc. 31st Int. Conf. on Computer Aided Verification (CAV). pp. 534\u2013546 (2019)","DOI":"10.1007\/978-3-030-25543-5_30"},{"key":"5_CR42","doi-asserted-by":"crossref","unstructured":"Emmi, M., Enea, C., Hamza, J.: Monitoring Refinement via Symbolic Reasoning. In: Proc. 36th ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI). pp. 260\u2013269 (2015)","DOI":"10.1145\/2737924.2737983"},{"key":"5_CR43","doi-asserted-by":"crossref","unstructured":"Enea, C., Koskinen, E.: Scenario-Based Proofs for Concurrent Objects. In: Proc. ACM Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). pp. 1294\u20131323 (2024)","DOI":"10.1145\/3649857"},{"issue":"11","key":"5_CR44","doi-asserted-by":"publisher","first-page":"624","DOI":"10.1145\/360363.360369","volume":"19","author":"K Eswaran","year":"1976","unstructured":"Eswaran, K., Gray, J., Lorie, R., Traiger, I.: The Notions of Consistency and Predicate Locks in a Database System. Commun. ACM 19(11), 624\u2013633 (1976)","journal-title":"Commun. ACM"},{"key":"5_CR45","doi-asserted-by":"crossref","unstructured":"Farzan, A., Madhusudan, P.: Monitoring Atomicity in Concurrent Programs. In: Proc. 20th Int. Conf. on Computer Aided Verification (CAV). pp. 52\u201365 (2008)","DOI":"10.1007\/978-3-540-70545-1_8"},{"key":"5_CR46","unstructured":"Feldman, Y., Enea, C., Morrison, A., Rinetzky, N., Shoham, S.: Order Out of Chaos: Proving Linearizability Using Local Views. In: Proc. Int. Symposium on Distributed Computing (DISC) (2018)"},{"issue":"51\u201352","key":"5_CR47","doi-asserted-by":"publisher","first-page":"4379","DOI":"10.1016\/j.tcs.2010.09.021","volume":"411","author":"I Filipovi\u0107","year":"2010","unstructured":"Filipovi\u0107, I., O\u2019Hearn, P., Rinetzky, N., Yang, H.: Abstraction for Concurrent Objects. Theoret. Comput. Sci. 411(51\u201352), 4379\u20134398 (2010)","journal-title":"Theoret. Comput. Sci."},{"key":"5_CR48","doi-asserted-by":"crossref","unstructured":"Flanagan, C.: Verifying Commit-Atomicity Using Model-Checking. In: Proc. 11th Int. Symposium on Model Checking Software (SPIN). pp. 252\u2013266 (2004)","DOI":"10.1007\/978-3-540-24732-6_18"},{"key":"5_CR49","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S., Yi, J.: Velodrome: A Sound and Complete Dynamic Atomicity Checker for Multithreaded Programs. In: Proc. 29th ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI). pp. 293\u2013303 (2008)","DOI":"10.1145\/1375581.1375618"},{"issue":"4","key":"5_CR50","doi-asserted-by":"publisher","first-page":"1208","DOI":"10.1137\/S0097539794279614","volume":"26","author":"P Gibbons","year":"1997","unstructured":"Gibbons, P., Korach, E.: Testing Shared Memories. SIAM J. Comput. 26(4), 1208\u20131244 (1997)","journal-title":"SIAM J. Comput."},{"key":"5_CR51","doi-asserted-by":"crossref","unstructured":"Golovin, P., Kokologiannakis, M., Vafeiadis, V.: Relinche: Automatically Checking Linearizability under Relaxed Memory Consistency. In: Proc. 52nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). pp. 2090\u20132117 (2025)","DOI":"10.1145\/3704906"},{"key":"5_CR52","doi-asserted-by":"crossref","unstructured":"Herlihy, M., Wing, J.: Axioms for Concurrent Objects. In: Proc. 14th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). pp. 13\u201326 (1987)","DOI":"10.1145\/41625.41627"},{"key":"5_CR53","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"3","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.: Linearizability: A Correctness Condition for Concurrent Objects. ACM Transactions on Programming Languages and Systems (TOPLAS) 3, 463\u2013492 (1990)","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"5_CR54","unstructured":"Hochstein, L.: Serializability and TLA+ (Oct 2024), https:\/\/surfingcomplexity.blog\/2024\/10\/28\/serializability-and-tla\/"},{"key":"5_CR55","unstructured":"Hogan, M., Landau-Feibish, S., Arashloo, M.T., Rexford, J., Walker, D.: Modular Switch Programming Under Resource Constraints. In: Proc. 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI). pp. 193\u2013207 (2022)"},{"issue":"5","key":"5_CR56","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G Holzmann","year":"1997","unstructured":"Holzmann, G.: The Model Checker SPIN. IEEE Trans. Software Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Software Eng."},{"key":"5_CR57","doi-asserted-by":"crossref","unstructured":"Kim, D., Liu, Z., Zhu, Y., Kim, C., Lee, J., Sekar, V., Seshan, S.: TEA: Enabling State-Intensive Network Functions on Programmable Switches. In: Proc. Int. Conf. of the ACM Special Interest Group on Data Communication (SIGCOMM). pp. 90\u2013106 (2020)","DOI":"10.1145\/3387514.3405855"},{"key":"5_CR58","doi-asserted-by":"crossref","unstructured":"Kleene, S.C.: Representation of Events in Nerve Nets and Finite Automata, vol.\u00a034. Princeton University Press Princeton (1956)","DOI":"10.1515\/9781400882618-002"},{"key":"5_CR59","doi-asserted-by":"crossref","unstructured":"Konnov, I., Kukovec, J., Tran, T.H.: TLA+ Model Checking Made Symbolic. In: Proc. ACM Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). pp. 1\u201330 (2019)","DOI":"10.1145\/3360549"},{"key":"5_CR60","doi-asserted-by":"crossref","unstructured":"Kosaraju, S.: Decidability of Reachability in Vector Addition Systems. In: Proc. 14th Annual ACM Symposium on Theory of Computing (STOC). pp. 267\u2013281 (1982)","DOI":"10.1145\/800070.802201"},{"key":"5_CR61","doi-asserted-by":"crossref","unstructured":"Koval, N., Fedorov, A., Sokolova, M., Tsitelov, D., Alistarh, D.: Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM. In: Proc. 35th Int. Conf. on Computer Aided Verification (CAV). pp. 156\u2013169 (2023)","DOI":"10.1007\/978-3-031-37706-8_8"},{"issue":"1","key":"5_CR62","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/JPROC.2014.2371999","volume":"103","author":"D Kreutz","year":"2014","unstructured":"Kreutz, D., Ramos, F., Verissimo, P.E., Rothenberg, C., Azodolmolky, S., Uhlig, S.: Software-Defined Networking: A Comprehensive Survey. Proc. of the IEEE 103(1), 14\u201376 (2014)","journal-title":"Proc. of the IEEE"},{"key":"5_CR63","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic Symbolic Model Checker. In: Proc. 12th Int. Conf. on Modelling Techniques and Tools for Computer Performance Evaluation (TOOLS). pp. 200\u2013204 (2002)","DOI":"10.1007\/3-540-46029-2_13"},{"issue":"1","key":"5_CR64","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0304-3975(92)90173-D","volume":"99","author":"JL Lambert","year":"1992","unstructured":"Lambert, J.L.: A Structure to Decide Reachability in Petri Nets. Theoret. Comput. Sci. 99(1), 79\u2013104 (1992)","journal-title":"Theoret. Comput. Sci."},{"key":"5_CR65","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"3","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems (TOPLAS) 3, 872\u2013923 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"5_CR66","doi-asserted-by":"crossref","unstructured":"Leroux, J.: The Reachability Problem for Petri Nets is Not Primitive Recursive. In: Proc. 62nd Annual Symposium on Foundations of Computer Science (FOCS). pp. 1241\u20131252 (2022)","DOI":"10.1109\/FOCS52979.2021.00121"},{"key":"5_CR67","doi-asserted-by":"crossref","unstructured":"Leroux, J.: The General Vector Addition System Reachability Problem by Presburger Inductive Invariants. Logical Methods in Computer Science (LMCS) (2010)","DOI":"10.1109\/LICS.2009.10"},{"key":"5_CR68","doi-asserted-by":"crossref","unstructured":"Liang, H., Feng, X.: Modular Verification of Linearizability with Non-Fixed Linearization Points. In: Proc. 34th ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI). pp. 459\u2013470 (2013)","DOI":"10.1145\/2491956.2462189"},{"key":"5_CR69","doi-asserted-by":"crossref","unstructured":"Liu, Y., Chen, W., Liu, Y., Sun, J.: Model Checking Linearizability via Refinement. In: Proc. 16th Int. Symposium on Formal Methods (FM). pp. 321\u2013337 (2009)","DOI":"10.1007\/978-3-642-05089-3_21"},{"issue":"7","key":"5_CR70","doi-asserted-by":"publisher","first-page":"1018","DOI":"10.1109\/TSE.2012.82","volume":"39","author":"Y Liu","year":"2012","unstructured":"Liu, Y., Chen, W., Liu, Y., Sun, J., Zhang, S.J., Dong, J.S.: Verifying Linearizability via Optimized Refinement Checking. IEEE Trans. Software Eng. 39(7), 1018\u20131039 (2012)","journal-title":"IEEE Trans. Software Eng."},{"issue":"4","key":"5_CR71","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.3928","volume":"29","author":"G Lowe","year":"2017","unstructured":"Lowe, G.: Testing for Linearizability. Concurrency and Computation: Practice and Experience 29(4), e3928 (2017)","journal-title":"Concurrency and Computation: Practice and Experience"},{"key":"5_CR72","doi-asserted-by":"crossref","unstructured":"Manevich, R., Lev-Ami, T., Sagiv, M., Ramalingam, G., Berdine, J.: Heap Decomposition for Concurrent Shape Analysis. In: Proc. 15th Int. Symposium on Static Analysis (SAS). pp. 363\u2013377 (2008)","DOI":"10.1007\/978-3-540-69166-2_24"},{"key":"5_CR73","doi-asserted-by":"crossref","unstructured":"Mayr, E.: An Algorithm for the General Petri Net Reachability Problem. In: Proc. 13th Annual ACM Symposium on Theory of Computing (STOC). pp. 238\u2013246 (1981)","DOI":"10.1145\/800076.802477"},{"key":"5_CR74","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1109\/TAC.1977.1101509","volume":"22","author":"T Murata","year":"1977","unstructured":"Murata, T.: State Equation, Controllability, and Maximal Matchings of Petri Nets. Transactions on Automatic Control 22, 412\u2013416 (1977)","journal-title":"Transactions on Automatic Control"},{"key":"5_CR75","unstructured":"Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and Reproducing Heisenbugs in Concurrent Programs. In: Proc. 8th USENIX Symposium on Operating Systems Design and Implementations (OSDI) (2008)"},{"key":"5_CR76","doi-asserted-by":"crossref","unstructured":"Namjoshi, K., Gheissi, S., Sabnani, K.: Algorithms for In-Place, Consistent Network Update. In: Proc. Int. Conf. of the ACM Special Interest Group on Data Communication (SIGCOMM). pp. 244\u2013257 (2024)","DOI":"10.1145\/3651890.3672266"},{"key":"5_CR77","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P., Rinetzky, N., Vechev, M., Yahav, E., Yorsh, G.: Verifying Linearizability with Hindsight. In: Proc. 29th Symposium on Principles of Distributed Computing (PODC). pp. 85\u201394 (2010)","DOI":"10.1145\/1835698.1835722"},{"key":"5_CR78","doi-asserted-by":"crossref","unstructured":"Ou, P., Demsky, B.: Checking Concurrent Data Structures Under the C\/C++ 11 Memory Model. In: Proc. 22nd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP). pp. 45\u201359 (2017)","DOI":"10.1145\/3018743.3018749"},{"issue":"4","key":"5_CR79","doi-asserted-by":"publisher","first-page":"631","DOI":"10.1145\/322154.322158","volume":"26","author":"C Papadimitriou","year":"1979","unstructured":"Papadimitriou, C.: The Serializability of Concurrent Database Updates. Journal of the ACM (JACM) 26(4), 631\u2013653 (1979)","journal-title":"Journal of the ACM (JACM)"},{"issue":"4","key":"5_CR80","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1145\/321356.321364","volume":"13","author":"RJ Parikh","year":"1966","unstructured":"Parikh, R.J.: On Context-Free Languages. Journal of the ACM (JACM) 13(4), 570\u2013581 (1966)","journal-title":"Journal of the ACM (JACM)"},{"key":"5_CR81","doi-asserted-by":"crossref","unstructured":"Pradel, M., Gross, T.: Fully Automatic and Precise Detection of Thread Safety Violations. In: Proc. 33rd ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI). pp. 521\u2013530 (2012)","DOI":"10.1145\/2254064.2254126"},{"key":"5_CR82","doi-asserted-by":"crossref","unstructured":"Pradel, M., Gross, T.: Automatic Testing of Sequential and Concurrent Substitutability. In: Proc. 35th Int. Conf. on Software Engineering (ICSE). pp. 282\u2013291 (2013)","DOI":"10.1109\/ICSE.2013.6606574"},{"key":"5_CR83","unstructured":"Presburger, M.: Uber die vollstandigkeiteines gewissen systems der arithmetik ganzer zahlen, in welchen die addition als einzige operation hervortritt. In: Comptes-rendus du ler congres des mathematiciens des pays slavs (1929)"},{"issue":"2","key":"5_CR84","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(78)90036-1","volume":"6","author":"C Rackoff","year":"1978","unstructured":"Rackoff, C.: The Covering and Boundedness Problems for Vector Addition Systems. Theoret. Comput. Sci. 6(2), 223\u2013231 (1978)","journal-title":"Theoret. Comput. Sci."},{"key":"5_CR85","doi-asserted-by":"crossref","unstructured":"Rakow, A.: Safety Slicing Petri Nets. In: Proc. 33rd Int. Conf. on Applications and Theory of Petri Nets and Concurrency (PETRI NETS). pp. 268\u2013287 (2012)","DOI":"10.1007\/978-3-642-31131-4_15"},{"key":"5_CR86","doi-asserted-by":"crossref","unstructured":"Sinha, A., Malik, S., Wang, C., Gupta, A.: Predicting Serializability Violations: SMT-Based Search vs. DPOR-Based Search. In: Proc. 7th Haifa Verification Conference (HVC). pp. 95\u2013114 (2011)","DOI":"10.1007\/978-3-642-34188-5_11"},{"key":"5_CR87","doi-asserted-by":"crossref","unstructured":"Sinha, A., Malik, S., Wang, C., Gupta, A.: Predictive Analysis for Detecting Serializability Violations Through Trace Segmentation. In: Proc. 9th ACM\/IEEE Int. Conf. on Formal Methods and Models for Codesign (MEMPCODE). pp. 99\u2013108 (2011)","DOI":"10.1109\/MEMCOD.2011.5970516"},{"key":"5_CR88","doi-asserted-by":"crossref","unstructured":"Soethout, T., van\u00a0der Storm, T., Vinju, J.J.: Automated Validation of State-Based Client-Centric Isolation with TLA+. In: Proc. 18th Int. Conf. Software Engineering and Formal Methods (SEFM). pp. 43\u201357 (2020)","DOI":"10.1007\/978-3-030-67220-1_4"},{"key":"5_CR89","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification Under Fairness. In: Proc. 21st Int. Conf. on Computer Aided Verification (CAV). pp. 709\u2013714 (2009)","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"5_CR90","unstructured":"Tasiran, S.: A Compositional Method for Verifying Software Transactional Memory Implementations. Microsoft Research, Technical Report MSR-TR-2008\u201356 (2008)"},{"key":"5_CR91","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Shape-Value Abstraction for Verifying Linearizability. In: Proc. 9th Int. Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI). pp. 335\u2013348 (2009)","DOI":"10.1007\/978-3-540-93900-9_27"},{"key":"5_CR92","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Automatically Proving Linearizability. In: Proc. 22nd Int. Conf. on Computer Aided Verification (CAV). pp. 450\u2013464 (2010)","DOI":"10.1007\/978-3-642-14295-6_40"},{"key":"5_CR93","doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E.: Deriving Linearizable Fine-Grained Concurrent Objects. In: Proc. 29th ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI). pp. 125\u2013135 (2008)","DOI":"10.1145\/1375581.1375598"},{"key":"5_CR94","doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Experience with Model Checking Linearizability. In: Proc. 16th Int. Symposium on Model Checking Software (SPIN). pp. 261\u2013278 (2009)","DOI":"10.1007\/978-3-642-02652-2_21"},{"key":"5_CR95","doi-asserted-by":"crossref","unstructured":"Verma, K.N., Seidl, H., Schwentick, T.: On the Complexity of Equational Horn Clauses. In: Proc. 20th Int. Conf. on Automated Deduction (CADE). pp. 337\u2013352 (2005)","DOI":"10.1007\/11532231_25"},{"issue":"11","key":"5_CR96","doi-asserted-by":"publisher","first-page":"2021","DOI":"10.1109\/JPROC.2015.2455034","volume":"103","author":"Y Vizel","year":"2015","unstructured":"Vizel, Y., Weissenbacher, G., Malik, S.: Boolean Satisfiability Solvers and their Applications in Model Checking. Proc. of the IEEE 103(11), 2021\u20132035 (2015)","journal-title":"Proc. of the IEEE"},{"key":"5_CR97","doi-asserted-by":"crossref","unstructured":"Wang, L., Stoller, S.: Accurate and Efficient Runtime Detection of Atomicity Errors in Concurrent Programs. In: Proc. 11th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP). pp. 137\u2013146 (2006)","DOI":"10.1145\/1122971.1122993"},{"issue":"2","key":"5_CR98","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1109\/TSE.2006.1599419","volume":"32","author":"L Wang","year":"2006","unstructured":"Wang, L., Stoller, S.: Runtime Analysis of Atomicity for Multithreaded Programs. IEEE Trans. Software Eng. 32(2), 93\u2013110 (2006b)","journal-title":"IEEE Trans. Software Eng."},{"issue":"1\u20132","key":"5_CR99","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1006\/jpdc.1993.1015","volume":"17","author":"J Wing","year":"1993","unstructured":"Wing, J., Gong, C.: Testing and Verifying Concurrent Objects. Journal of Parallel and Distributed Computing 17(1\u20132), 164\u2013182 (1993)","journal-title":"Journal of Parallel and Distributed Computing"},{"issue":"1","key":"5_CR100","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1109\/COMST.2014.2330903","volume":"17","author":"W Xia","year":"2015","unstructured":"Xia, W., Wen, Y., Foh, C.H., Niyato, D., Xie, H.: A Survey on Software-Defined Networking. IEEE Communications Surveys & Tutorials 17(1), 27\u201351 (2015)","journal-title":"IEEE Communications Surveys & Tutorials"},{"key":"5_CR101","doi-asserted-by":"crossref","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model Checking TLA+ Specifications. In: Proc. Int. Conf. Correct Hardware Design and Verification Methods (CHARME). pp. 54\u201366 (1999)","DOI":"10.1007\/3-540-48153-2_6"},{"key":"5_CR102","doi-asserted-by":"crossref","unstructured":"Zhang, S.J.: Scalable Automatic Linearizability Checking. In: Proc. 33rd Int. Conf. on Software Engineering (ICSE). pp. 1185\u20131187 (2011)","DOI":"10.1145\/1985793.1986037"},{"key":"5_CR103","doi-asserted-by":"crossref","unstructured":"Zhu, H., Petri, G., Jagannathan, S.: Poling: SMT Aided Linearizability Proofs. In: Proc. 27th Int. Conf. on Computer Aided Verification (CAV). pp. 3\u201319 (2015)","DOI":"10.1007\/978-3-319-21668-3_1"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22749-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T13:11:19Z","timestamp":1776258679000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22749-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227485","9783032227492"],"references-count":103,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22749-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"15 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}