@inproceedings(fmrailsurvey2,
 author       = {Maurice H. ter Beek and Arne Bor{\"{a}}lv and Alessandro Fantechi and Alessio Ferrari and Stefania Gnesi and Christer L{\"{o}}fving and Franco Mazzanti},
 year         = {2019},
 title        = {Adopting Formal Methods in an Industrial Setting: The Railways Case},
 editor       = {Maurice H. ter Beek and Annabelle McIver and Jos{\'{e}} N. Oliveira},
 booktitle    = {Formal Methods - The Next 30 Years, {FM} 2019, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {11800},
 publisher    = {Springer},
 pages        = {762--772},
 doi          = {10.1007/978-3-030-30942-8\_46},
)
@article(bmc,
 author       = {Armin Biere and Alessandro Cimatti and Edmund M. Clarke and Ofer Strichman and Yunshan Zhu},
 year         = {2003},
 title        = {Bounded model checking},
 journal      = {Adv. Comput.},
 volume       = {58},
 pages        = {117--148},
 doi          = {10.1016/S0065-2458(03)58003-2},
)
@inproceedings(BiereFazekasFleuryHeisinger-SAT-Competition-2020-solvers,
 author       = {Armin Biere and Katalin Fazekas and Mathias Fleury and Maximillian Heisinger},
 year         = {2020},
 title        = {{CaDiCaL}, {Kissat}, {Paracooba}, {Plingeling} and {Treengeling} Entering the {SAT Competition 2020}},
 editor       = {Tomas Balyo and Nils Froleyks and Marijn Heule and Markus Iser and Matti J{\"a}rvisalo and Martin Suda},
 booktitle    = {Proc.~of {SAT Competition} 2020 -- Solver and Benchmark Descriptions},
 series       = {Department of Computer Science Report Series B},
 volume       = {B-2020-1},
 publisher    = {University of Helsinki},
 pages        = {51--53},
)
@proceedings(sathandbook,
 editor       = {Armin Biere and Marijn Heule and Hans van Maaren and Toby Walsh},
 year         = {2009},
 title        = {Handbook of Satisfiability},
 series       = {Frontiers in Artificial Intelligence and Applications},
 volume       = {185},
 publisher    = {{IOS} Press},
)
@article(bjorksatencoding,
 author       = {Magnus Bj{\"{o}}rk},
 year         = {2011},
 title        = {Successful {SAT} Encoding Techniques},
 journal      = {J. Satisf. Boolean Model. Comput.},
 volume       = {7},
 number       = {4},
 pages        = {189--201},
 doi          = {10.3233/sat190085},
)
@book(handbookrailwayoptimization,
 editor       = {Bornd\IeC{\"o}rfer, Ralf and Torsten Klug and Leonardo Lamorgese and Carlo Mannino and Markus Reuther and Thomas Schlechte},
 year         = {2018},
 title        = {Handbook of Optimization in the Railway Industry},
 publisher    = {Springer},
 doi          = {10.1007/978-3-319-72153-8},
)
@article(temporalinduction,
 author       = {Niklas E{\'{e}}n and Niklas S{\"{o}}rensson},
 year         = {2003},
 title        = {Temporal induction by incremental {SAT} solving},
 journal      = {Electron. Notes Theor. Comput. Sci.},
 volume       = {89},
 number       = {4},
 pages        = {543--560},
 doi          = {10.1016/S1571-0661(05)82542-3},
)
@article(fang,
 author       = {Wei Fang and Shengxiang Yang and Xin Yao},
 year         = {2015},
 title        = {A Survey on Problem Models and Solution Approaches to Rescheduling in Railway Networks},
 journal      = {{IEEE} Trans. Intell. Transp. Syst.},
 volume       = {16},
 number       = {6},
 pages        = {2997--3016},
 doi          = {10.1109/TITS.2015.2446985},
)
@inproceedings(fmrailsurvey1,
 author       = {Alessandro Fantechi},
 year         = {2013},
 title        = {Twenty-Five Years of Formal Methods and Railways: What Next?},
 editor       = {Steve Counsell and N{\'{u}}{\~{n}}ez, Manuel},
 booktitle    = {Software Engineering and Formal Methods - {SEFM} 2013, Revised Selected Papers},
 series       = {Lecture Notes in Computer Science},
 volume       = {8368},
 publisher    = {Springer},
 pages        = {167--183},
 doi          = {10.1007/978-3-319-05032-4\_13},
)
@article(FANTI20061231,
 author       = {M.P. Fanti and A. Giua and C. Seatzu},
 year         = {2006},
 title        = {Monitor design for colored Petri nets: An application to deadlock prevention in railway networks},
 journal      = {Control Engineering Practice},
 volume       = {14},
 number       = {10},
 pages        = {1231--1247},
 doi          = {10.1016/j.conengprac.2006.02.007},
 note         = {The Seventh Workshop On Discrete Event Systems (WODES2004)},
)
@inproceedings(DBLP:conf/dasc/HasebeTK17,
 author       = {Koji Hasebe and Mitsuaki Tsuji and Kazuhiko Kato},
 year         = {2017},
 title        = {Deadlock Detection in the Scheduling of Last-Mile Transportation Using Model Checking},
 booktitle    = {15th {IEEE} Intl Conf on Dependable, Autonomic and Secure Computing, DASC/PiCom/DataCom/CyberSciTech 2017},
 publisher    = {{IEEE} Computer Society},
 pages        = {423--430},
 doi          = {10.1109/DASC-PICom-DataCom-CyberSciTec.2017.84},
)
@inproceedings(DBLP:conf/concur/Heljanko01,
 author       = {Keijo Heljanko},
 year         = {2001},
 title        = {Bounded Reachability Checking with Process Semantics},
 editor       = {Kim Guldstrand Larsen and Mogens Nielsen},
 booktitle    = {{CONCUR} 2001 - Concurrency Theory, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {2154},
 publisher    = {Springer},
 pages        = {218--232},
 doi          = {10.1007/3-540-44685-0\_15},
)
@article(DBLP:journals/scp/HongHP17,
 author       = {Linh Vu Hong and Anne E. Haxthausen and Jan Peleska},
 year         = {2017},
 title        = {Formal modelling and verification of interlocking systems featuring sequential release},
 journal      = {Sci. Comput. Program.},
 volume       = {133},
 pages        = {91--115},
 doi          = {10.1016/j.scico.2016.05.010},
)
@article(fengli,
 author       = {Feng Li and Jiuh-Biing Sheu and Zi-You Gao},
 year         = {2014},
 title        = {Deadlock analysis, prevention and train optimal travel mechanism in single-track railway system},
 journal      = {Transportation Research Part B: Methodological},
 volume       = {68},
 pages        = {385--414},
 doi          = {10.1016/j.trb.2014.06.014},
)
@article(DBLP:journals/tomacs/LuDL04,
 author       = {Quan Lu and Maged M. Dessouky and Robert C. Leachman},
 year         = {2004},
 title        = {Modeling train movements through complex rail networks},
 journal      = {{ACM} Trans. Model. Comput. Simul.},
 volume       = {14},
 number       = {1},
 pages        = {48--75},
 doi          = {10.1145/974734.974737},
)
@article(lutebergetsatmodsim,
 author       = {Bj{\o}rnar Luteberget and Koen Claessen and Christian Johansen and Martin Steffen},
 year         = {2021},
 title        = {SAT modulo discrete event simulation applied to railway design capacity analysis},
 journal      = {Formal Methods in System Design},
 pages        = {1--35},
 doi          = {10.1007/s10703-021-00368-2},
)
@inproceedings(mazzanti2,
 author       = {Franco Mazzanti and Alessio Ferrari and Giorgio Oronzo Spagnolo},
 year         = {2016},
 title        = {Experiments in Formal Modelling of a Deadlock Avoidance Algorithm for a {CBTC} System},
 editor       = {Tiziana Margaria and Bernhard Steffen},
 booktitle    = {Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part {II}},
 series       = {Lecture Notes in Computer Science},
 volume       = {9953},
 pages        = {297--314},
 doi          = {10.1007/978-3-319-47169-3\_22},
)
@inproceedings(mazzanti,
 author       = {Franco Mazzanti and Giorgio Oronzo Spagnolo and Simone Della Longa and Alessio Ferrari},
 year         = {2014},
 title        = {Deadlock Avoidance in Train Scheduling: {A} Model Checking Approach},
 editor       = {Fr{\'{e}}d{\'{e}}ric Lang and Francesco Flammini},
 booktitle    = {Formal Methods for Industrial Critical Systems, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {8718},
 publisher    = {Springer},
 pages        = {109--123},
 doi          = {10.1007/978-3-319-10702-8\_8},
)
@inproceedings(pachldeadlock,
 author       = {J{\"o}rn Pachl},
 year         = {2007},
 title        = {Avoiding Deadlocks in Synchronous Railway Simulations},
 booktitle    = {2nd International Seminar on Railway Operations Modelling and Analysis. 2007, Hannover, Germany},
 doi          = {10.24355/dbbs.084-200704030200-0},
 url          = {https://publikationsserver.tu-braunschweig.de/receive/dbbs_mods_00020794},
)
@article(rintanen,
 author       = {Jussi Rintanen and Keijo Heljanko and Ilkka Niemel{\"{a}}},
 year         = {2006},
 title        = {Planning as satisfiability: parallel plans and algorithms for plan search},
 journal      = {Artif. Intell.},
 volume       = {170},
 number       = {12-13},
 pages        = {1031--1080},
 doi          = {10.1016/j.artint.2006.08.002},
)
@article(sassoticks,
 author       = {Veronica Dal Sasso and Leonardo Lamorgese and Carlo Mannino and Andrea Onofri and Paolo Ventura},
 year         = {2021},
 title        = {The Tick Formulation for deadlock detection and avoidance in railways traffic control},
 journal      = {J. Rail Transp. Plan. Manag.},
 volume       = {17},
 pages        = {100239},
 doi          = {10.1016/j.jrtpm.2021.100239},
)
@inproceedings(sheeraninduction,
 author       = {Mary Sheeran and Satnam Singh and St{\r a}lmarck, Gunnar},
 year         = {2000},
 title        = {Checking Safety Properties Using Induction and a SAT-Solver},
 editor       = {Warren A. Hunt Jr. and Steven D. Johnson},
 booktitle    = {Formal Methods in Computer-Aided Design, {FMCAD} 2000, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {1954},
 publisher    = {Springer},
 pages        = {108--125},
 doi          = {10.1007/3-540-40922-X\_8},
)
@inproceedings(DBLP:conf/cp/Sinz05,
 author       = {Carsten Sinz},
 year         = {2005},
 title        = {Towards an Optimal {CNF} Encoding of Boolean Cardinality Constraints},
 editor       = {Peter van Beek},
 booktitle    = {Principles and Practice of Constraint Programming - {CP} 2005},
 series       = {Lecture Notes in Computer Science},
 volume       = {3709},
 publisher    = {Springer},
 pages        = {827--831},
 doi          = {10.1007/11564751\_73},
)
@article(vizelsatmodelchecking,
 author       = {Yakir Vizel and Georg Weissenbacher and Sharad Malik},
 year         = {2015},
 title        = {Boolean Satisfiability Solvers and Their Applications in Model Checking},
 journal      = {Proc. {IEEE}},
 volume       = {103},
 number       = {11},
 pages        = {2021--2035},
 doi          = {10.1109/JPROC.2015.2455034},
)