@inproceedings(AbdullaCJT96, author = {Parosh Aziz Abdulla and Karlis Cerans and Bengt Jonsson and Yih{-}Kuen Tsay}, year = {1996}, title = {General Decidability Theorems for Infinite-State Systems}, booktitle = {{LICS}}, publisher = {{IEEE} Computer Society}, pages = {313--321}, doi = {10.1109/LICS.1996.561359}, ) @article(AbdullaHH16, author = {Parosh Aziz Abdulla and Fr{\'{e}}d{\'{e}}ric Haziza and Hol{\'{\i}}k, Luk{\'{a}}s}, year = {2016}, title = {Parameterized verification through view abstraction}, journal = {Int. J. Softw. Tools Technol. Transf.}, volume = {18}, number = {5}, pages = {495--516}, doi = {10.1007/s10009-015-0406-x}, ) @inproceedings(AbdullaHDR08, author = {Parosh Aziz Abdulla and Noomene Ben Henda and Giorgio Delzanno and Ahmed Rezine}, year = {2008}, title = {Handling Parameterized Systems with Non-atomic Global Conditions}, booktitle = {{VMCAI}}, series = {Lecture Notes in Computer Science}, volume = {4905}, publisher = {Springer}, pages = {22--36}, doi = {10.1007/978-3-540-78163-9\_7}, ) @inproceedings(AbdullaJNS04, author = {Parosh Aziz Abdulla and Bengt Jonsson and Marcus Nilsson and Mayank Saksena}, year = {2004}, title = {A Survey of Regular Model Checking}, booktitle = {{CONCUR}}, series = {LNCS}, volume = {3170}, publisher = {Springer}, pages = {35--48}, doi = {10.1007/978-3-540-28644-8\_3}, ) @incollection(AbdullaST18, author = {Parosh Aziz Abdulla and A. Prasad Sistla and Muralidhar Talupur}, year = {2018}, title = {Model Checking Parameterized Systems}, booktitle = {Handbook of Model Checking}, publisher = {Springer}, pages = {685--725}, doi = {10.1007/978-3-319-10575-8\_21}, ) @inproceedings(DBLP:conf/cav/BarrettCDHJKRT11, author = {Clark W. Barrett and Christopher L. Conway and Morgan Deters and Liana Hadarean and Dejan Jovanovic and Tim King and Andrew Reynolds and Cesare Tinelli}, year = {2011}, title = {{CVC4}}, booktitle = {{CAV}}, series = {Lecture Notes in Computer Science}, volume = {6806}, publisher = {Springer}, pages = {171--177}, doi = {10.1007/978-3-642-22110-1\_14}, ) @inproceedings(BaukusBLS00, author = {Kai Baukus and Saddek Bensalem and Yassine Lakhnech and Karsten Stahl}, year = {2000}, title = {Abstracting {WS1S} Systems to Verify Parameterized Networks}, booktitle = {{TACAS}}, series = {LNCS}, volume = {1785}, publisher = {Springer}, pages = {188--203}, doi = {10.1007/3-540-46419-0\_14}, ) @inproceedings(BlondinEH0M20, author = {Michael Blondin and Javier Esparza and Martin Helfrich and Anton{\'{\i}}n Kucera and Philipp J. Meyer}, year = {2020}, title = {Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling}, booktitle = {{CAV} {(2)}}, series = {LNCS}, volume = {12225}, publisher = {Springer}, pages = {372--397}, doi = {10.1007/978-3-030-53291-8\_20}, ) @inproceedings(BozgaEISW20, author = {Marius Bozga and Javier Esparza and Radu Iosif and Joseph Sifakis and Christoph Welzel}, year = {2020}, title = {Structural Invariants for the Verification of Systems with Parameterized Architectures}, booktitle = {{TACAS} {(1)}}, series = {Lecture Notes in Computer Science}, volume = {12078}, publisher = {Springer}, pages = {228--246}, doi = {10.1007/978-3-030-45190-5\_13}, ) @article(BozgaIS21, author = {Marius Bozga and Radu Iosif and Joseph Sifakis}, year = {2021}, title = {Checking deadlock-freedom of parametric component-based systems}, journal = {J. Log. Algebraic Methods Program.}, volume = {119}, pages = {100621}, doi = {10.1016/j.jlamp.2020.100621}, ) @article(DBLP:journals/cacm/Bruijn67, author = {N. G. de Bruijn}, year = {1967}, title = {Additional comments on a problem in concurrent programming control}, journal = {Commun. {ACM}}, volume = {10}, number = {3}, pages = {137--138}, doi = {10.1145/363162.363167}, ) @inbook(Dijkstra2002, author = {Edsger W. Dijkstra}, year = {2002}, title = {Cooperating Sequential Processes}, pages = {65--138}, publisher = {Springer New York}, address = {New York, NY}, doi = {10.1007/978-1-4757-3472-0_2}, ) @article(DBLP:journals/cacm/EisenbergM72, author = {Murray A. Eisenberg and Michael R. McGuire}, year = {1972}, title = {Further Comments on Dijkstra's Concurrent Programming Control Problem}, journal = {Commun. {ACM}}, volume = {15}, number = {11}, pages = {999}, doi = {10.1145/355606.361895}, ) @article(EsparzaGLM17, author = {Javier Esparza and Pierre Ganty and J{\'{e}}r{\^{o}}me Leroux and Rupak Majumdar}, year = {2017}, title = {Verification of population protocols}, journal = {Acta Informatica}, volume = {54}, number = {2}, pages = {191--215}, doi = {10.1007/s00236-016-0272-3}, ) @inproceedings(EsparzaLMMN14, author = {Javier Esparza and Ledesma{-}Garza, Rusl{\'{a}}n and Rupak Majumdar and Philipp J. Meyer and Filip Niksic}, year = {2014}, title = {An SMT-Based Approach to Coverability Analysis}, booktitle = {{CAV}}, series = {Lecture Notes in Computer Science}, volume = {8559}, publisher = {Springer}, pages = {603--619}, doi = {10.1007/978-3-319-08867-9\_40}, ) @inproceedings(EsparzaM15, author = {Javier Esparza and Philipp J. Meyer}, year = {2015}, title = {An SMT-based Approach to Fair Termination Analysis}, booktitle = {{FMCAD}}, publisher = {{IEEE}}, pages = {49--56}, doi = {10.1109/FMCAD.2015.7542252}, ) @misc(esparza2021abduction, author = {Javier Esparza and Mikhail Raskin and Christoph Welzel}, year = {2021}, title = {Abduction of trap invariants in parameterized systems}, url = {https://arxiv.org/abs/2108.09101}, ) @misc(heron-gitlab, author = {Javier Esparza and Mikhail Raskin and Christoph Welzel}, year = {2021}, title = {heron, git repository}, howpublished = {\url{https://gitlab.lrz.de/i7/heron}}, ) @inproceedings(ERW21, author = {Javier Esparza and Mikhail A. Raskin and Christoph Welzel}, year = {2021}, title = {Computing Parameterized Invariants of Parameterized Petri Nets}, booktitle = {Petri Nets}, series = {Lecture Notes in Computer Science}, volume = {12734}, publisher = {Springer}, pages = {141--163}, doi = {10.1007/978-3-030-76983-3\_8}, ) @article(FinkelS01, author = {Alain Finkel and Philippe Schnoebelen}, year = {2001}, title = {Well-structured transition systems everywhere!}, journal = {Theor. Comput. Sci.}, volume = {256}, number = {1-2}, pages = {63--92}, doi = {10.1016/S0304-3975(00)00102-X}, ) @article(GantyM12, author = {Pierre Ganty and Rupak Majumdar}, year = {2012}, title = {Algorithmic verification of asynchronous programs}, journal = {ACM Trans. Program. Lang. Syst.}, volume = {34}, number = {1}, pages = {6}, doi = {10.1145/2160910.2160915}, ) @article(DBLP:journals/aicom/GebserKKOSS11, author = {Martin Gebser and Benjamin Kaufmann and Roland Kaminski and Max Ostrowski and Torsten Schaub and Marius Schneider}, year = {2011}, title = {Potassco: The Potsdam Answer Set Solving Collection}, journal = {{AI} Commun.}, volume = {24}, number = {2}, pages = {107--124}, doi = {10.3233/AIC-2011-0491}, ) @article(GS92, author = {Steven M. German and A. Prasad Sistla}, year = {1992}, title = {Reasoning about systems with many processes}, journal = {Journal of the ACM (JACM)}, volume = {39}, number = {3}, pages = {675--735}, doi = {10.1145/146637.146681}, ) @inproceedings(GhilardiR10, author = {Silvio Ghilardi and Silvio Ranise}, year = {2010}, title = {{MCMT:} {A} Model Checker Modulo Theories}, booktitle = {{IJCAR}}, series = {Lecture Notes in Computer Science}, volume = {6173}, publisher = {Springer}, pages = {22--29}, doi = {10.1007/978-3-642-14203-1\_3}, ) @inproceedings(DBLP:conf/ifm/GleissKS19, author = {Bernhard Gleiss and Laura Kov{\'{a}}cs and Lena Schnedlitz}, year = {2019}, title = {Interactive Visualization of Saturation Attempts in Vampire}, booktitle = {{IFM}}, series = {Lecture Notes in Computer Science}, volume = {11918}, publisher = {Springer}, pages = {504--513}, doi = {10.1007/978-3-030-34968-4\_28}, ) @book(HerlihyS08, author = {Maurice Herlihy and Nir Shavit}, year = {2008}, title = {The art of multiprocessor programming}, publisher = {Morgan Kaufmann}, ) @article(DBLP:journals/tcs/Jeandel10, author = {Emmanuel Jeandel}, year = {2010}, title = {The periodic domino problem revisited}, journal = {Theor. Comput. Sci.}, volume = {411}, number = {44-46}, pages = {4010--4016}, doi = {10.1016/j.tcs.2010.08.017}, ) @article(DBLP:journals/cacm/Knuth66, author = {Donald E. Knuth}, year = {1966}, title = {Additional comments on a problem in concurrent programming control}, journal = {Commun. {ACM}}, volume = {9}, number = {5}, pages = {321--322}, doi = {10.1145/355592.365595}, ) @inproceedings(DBLP:conf/cav/KovacsV13, author = {Laura Kov{\'{a}}cs and Andrei Voronkov}, year = {2013}, title = {First-Order Theorem Proving and Vampire}, booktitle = {{CAV}}, series = {Lecture Notes in Computer Science}, volume = {8044}, publisher = {Springer}, pages = {1--35}, doi = {10.1007/978-3-642-39799-8\_1}, ) @book(Lynch96, author = {Nancy A. Lynch}, year = {1996}, title = {Distributed Algorithms}, publisher = {Morgan Kaufmann}, ) @inproceedings(MSZ18, author = {Christian M{\"{u}}ller and Helmut Seidl and Eugen Zalinescu}, year = {2018}, title = {Inductive Invariants for Noninterference in Multi-agent Workflows}, booktitle = {{CSF}}, publisher = {{IEEE} Computer Society}, pages = {247--261}, doi = {10.1109/CSF.2018.00025}, ) @inproceedings(PadonMPSS16, author = {Oded Padon and Kenneth L. McMillan and Aurojit Panda and Mooly Sagiv and Sharon Shoham}, year = {2016}, title = {Ivy: safety verification by interactive generalization}, booktitle = {{PLDI}}, publisher = {{ACM}}, pages = {614--630}, doi = {10.1145/2908080.2908118}, ) @inproceedings(DBLP:conf/cade/Reger16, author = {Giles Reger}, year = {2016}, title = {Better Proof Output for Vampire}, booktitle = {Vampire@IJCAR}, series = {EPiC Series in Computing}, volume = {44}, publisher = {EasyChair}, pages = {46--60}, doi = {10.29007/5dmz}, ) @article(Sut17, author = {G. Sutcliffe}, year = {2017}, title = {{The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0}}, journal = {Journal of Automated Reasoning}, volume = {59}, number = {4}, pages = {483--502}, doi = {10.1007/s10817-017-9407-7}, ) @(heron-artifact, author = {Christoph Welzel and Javier Esparza and Mikhail Raskin}, year = {2020}, title = {heron, software artifact}, howpublished = {\url{https://doi.org/10.5281/zenodo.5068849}}, doi = {10.5281/zenodo.5068849}, )