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