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