Journal papers

• András Vörös, Dániel Darvas, Ákos Hajdu, Attila Klenik, Kristóf Marussy, Vince Molnár, Tamás Bartha, and István Majzik. Industrial applications of the PetriDotNet modelling and analysis tool.
  Science of Computer Programming, 157:17-40, 2018.
  doi  bib  mtmt  url  pdf
• Dániel Darvas, István Majzik, and Enrique Blanco Viñuela. PLC program translation for verification purposes.
  Periodica Polytechnica, Electrical Engineering and Computer Science, 61(2):151-165, 2017.
  doi  bib  mtmt  pdf
• Dániel Darvas, András Vörös, and Tamás Bartha. Improving saturation-based bounded model checking.
  Acta Cybernetica, 22(3):573-589, 2016.
  doi  bib  mtmt  url  pdf
• Vince Molnár, András Vörös, Dániel Darvas, Tamás Bartha, and István Majzik. Component-wise incremental LTL model checking.
  Formal Aspects of Computing, 28(3):345-379, 2016.
  doi  bib  mtmt  url  pdf
• Borja Fernández Adiego, Dániel Darvas, Enrique Blanco Viñuela, Jean-Charles Tournier, Simon Bliudze, Jan Olaf Blech, and Víctor M. González Suárez. Applying model checking to industrial-sized PLC programs.
  IEEE Transactions on Industrial Informatics, 11(6):1400-1410, 2015.
  doi  bib  mtmt  url  pdf
• András Vörös, Dániel Darvas, Attila Jámbor, and Tamás Bartha. Advanced saturation-based model checking of well-formed coloured Petri nets.
  Periodica Polytechnica, Electrical Engineering and Computer Science, 58(1):3-13, 2014.
  doi  bib  mtmt  pdf
• András Vörös, Dániel Darvas, and Tamás Bartha. Bounded saturation-based CTL model checking.
  Proceedings of the Estonian Academy of Sciences, 62(1):59-70, 2013.
  doi  bib  mtmt  pdf

Conference papers

• Gyula Salai, Dániel Darvas, and Enrique Blanco Viñuela. Testing solutions for Siemens PLC programs based on PLCSIM Advanced.
  In Karen S. White, Kevin A. Brown, Philip S. Dyer, and Volker R.W. Schaa, editors, Proceedings of the 17th International Conference on Accelerator and Large Experimental Physics Control Systems, pp. 1107-1110. JACoW, 2019.
  doi  bib  url  pdf
• Dániel Darvas, Enrique Blanco Viñuela, and Vince Molnár. PLCverif re-engineered: An open platform for the formal analysis of PLC programs.
  In Karen S. White, Kevin A. Brown, Philip S. Dyer, and Volker R.W. Schaa, editors, Proceedings of the 17th International Conference on Accelerator and Large Experimental Physics Control Systems, pp. 21-27. JACoW, 2019.
  doi  bib  mtmt  url  pdf
• Borja Fernández Adiego, Dániel Darvas, Enrique Blanco Viñuela, Gyula Sallai, Ignacio Prieto Diaz, Gisik Lee, Bhimavarapu Avinashkrishna, Yogesh Chandrakant Gaikwad, Sailaraj Sreekuttan, and Riccardo Pedica. Applying model checking to critical PLC applications: An ITER case study.
  In Volker R.W. Schaa, Isidre Costa, David Fernández, and Óscar Matilla, editors, Proceedings of the 16th International Conference on Accelerator and Large Experimental Physics Control Systems, pp. 1792-1796. JACoW, 2017.
  doi  bib  mtmt  url  pdf
• Dániel Darvas, Enrique Blanco Viñuela, and István Majzik. What is special about PLC software model checking?
  In Volker R.W. Schaa, Isidre Costa, David Fernández, and Óscar Matilla, editors, Proceedings of the 16th International Conference on Accelerator and Large Experimental Physics Control Systems, pp. 1781-1786. JACoW, 2017.
  doi  bib  mtmt  url  pdf
• Dániel Darvas, István Majzik, and Enrique Blanco Viñuela. Formal verification of safety PLC based control software.
  In Erika Ábrahám and Marieke Huisman, editors, Integrated Formal Methods, volume 9681 of Lecture Notes in Computer Science, pp. 508-522. Springer, 2016.
  doi  bib  mtmt  url  pdf
• Dániel Darvas, Enrique Blanco Viñuela, and István Majzik. PLC code generation based on a formal specification language.
  In 14th IEEE International Conference on Industrial Informatics (INDIN), pp. 389-396. IEEE, 2016.
  doi  bib  mtmt  url  pdf
• András Vörös, Dániel Darvas, Vince Molnár, Attila Klenik, Ákos Hajdu, Attila Jámbor, Tamás Bartha, and István Majzik. PetriDotNet 1.5: Extensible Petri net editor and analyser for education and research.
  In Fabrice Kordon and Daniel Moldt, editors, Application and Theory of Petri Nets and Concurrency, volume 9698 of Lecture Notes in Computer Science, pp. 123-132. Springer, 2016.
  doi  bib  mtmt  url  pdf
• Dániel Darvas, István Majzik, and Enrique Blanco Viñuela. Conformance checking for programmable logic controller programs and specifications.
  In 11th IEEE International Symposium on Industrial Embedded Systems (SIES), pp. 29-36. IEEE, 2016.
  doi  bib  mtmt  url  pdf
• Dániel Darvas, Enrique Blanco Viñuela, and István Majzik. A formal specification method for PLC-based applications.
  In Lou Corvetti, Kathleen Riches, and Volker R.W. Schaa, editors, Proceedings of the 15th International Conference on Accelerator and Large Experimental Physics Control Systems, pp. 907-910. JACoW, 2015.
  doi  bib  mtmt  url  pdf
• Dániel Darvas, Borja Fernández Adiego, and Enrique Blanco Viñuela. PLCverif: A tool to verify PLC programs based on model checking techniques.
  In Lou Corvetti, Kathleen Riches, and Volker R.W. Schaa, editors, Proceedings of the 15th International Conference on Accelerator and Large Experimental Physics Control Systems, pp. 911-914. JACoW, 2015.
  doi  bib  mtmt  url  pdf
• Vince Molnár, Dániel Darvas, András Vörös, and Tamás Bartha. Saturation-based incremental LTL model checking with inductive proofs.
  In Christel Baier and Cesare Tinelli, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 9035 of Lecture Notes in Computer Science, pp. 643-657. Springer, 2015.
  doi  bib  mtmt  url  pdf
• Dániel Darvas, Borja Fernández Adiego, András Vörös, Tamás Bartha, Enrique Blanco Viñuela, and Víctor M. González Suárez. Formal verification of complex properties on PLC programs.
  In Erika Ábrahám and Catuscia Palamidessi, editors, Formal Techniques for Distributed Objects, Components, and Systems, volume 8461 of Lecture Notes in Computer Science, pp. 284-299. Springer, 2014.
  doi  bib  mtmt  url  pdf
• Borja Fernández Adiego, Dániel Darvas, Enrique Blanco Viñuela, Jean-Charles Tournier, Víctor M. González Suárez, and Jan Olaf Blech. Modelling and formal verification of timing aspects in large PLC programs.
  In Edward Boje and Xiaohua Xia, editors, Proceedings of the 19th IFAC World Congress, volume 47 (3) of IFAC Proceedings Volumes, pp. 3333-3339. Elsevier, 2014.
  doi  bib  mtmt  url  pdf
• Borja Fernández Adiego, Dániel Darvas, Jean-Charles Tournier, Enrique Blanco Viñuela, and Víctor M. González Suárez. Bringing automated model checking to PLC program development - A CERN case study.
  In Jean-Jacques Lesage, Jean-Marc Faure, José E. Ribiero Cury, and Bengt Lennartson, editors, Proceedings of the 12th International Workshop on Discrete Event Systems, volume 47 (2) of IFAC Proceedings Volumes, pp. 394-399. Elsevier, 2014.
  doi  bib  mtmt  url  pdf
• Dániel Darvas, András Vörös, and Tamás Bartha. Efficient saturation-based bounded model checking of asynchronous systems.
  In Ákos Kiss, editor, Proceedings of the 13th Symposium on Programming Languages and Software Tools, SPLST'13, pp. 259-273, Szeged, Hungary, 2013. University of Szeged.
  bib  mtmt  pdf
• Tamás Bartha, András Vörös, Attila Jámbor, and Dániel Darvas. Verification of an industrial safety function using coloured Petri nets and model checking.
  In Elisabeth Ilie-Zudor, Zsolt Kemény, and László Monostori, editors, Proceedings of the 14th International Conference on Modern Information Technology in the Innovation Processes of the Industrial Enterprises (MITIP 2012), pp. 472-485. Hungarian Academy of Sciences, Computer and Automation Research Institute, 2012.
  bib  mtmt  pdf
• András Vörös, Tamás Bartha, Dániel Darvas, Tamás Szabó, Attila Jámbor, and Ákos Horváth. Parallel saturation based model checking.
  In Proceedings of the 10th International Symposium on Parallel and Distributed Computing (ISPDC), pp. 94-101. IEEE Computer Society, 2011.
  doi  bib  mtmt  pdf
• András Vörös, Dániel Darvas, and Tamás Bartha. Bounded saturation based CTL model checking.
  In Jaan Penjam, editor, Proceedings of the 12th Symposium on Programming Languages and Software Tools, SPLST'11, pp. 149-160, Tallinn, Estonia, 2011. Tallinn University of Technology, Institute of Cybernetics.
  bib  mtmt  pdf

Theses

• Dániel Darvas. Practice-oriented formal methods to support the software development of industrial control systems.
  PhD thesis, Budapest University of Technology and Economics, 2017.
  doi  bib  mtmt  url  pdf
• Dániel Darvas. Incremental extension of the saturation algorithm-based bounded model checking of Petri nets.
  Master's thesis, Budapest University of Technology and Economics, 2014.
  bib  url  pdf
• Dániel Darvas. Petri-háló alapú formális modellek analízise hatékony korlátos modellellenőrzési technikák segítségével [in Hungarian; Efficient bounded model checking techniques for Petri net based formal models].
  Bachelor's thesis, Budapest University of Technology and Economics, 2011.
  bib  url

Technical reports

• Gyula Sallai, Dániel Darvas, and Enrique Blanco Viñuela. Testing, simulation, and visualisation of PLC programs using x86 code generation.
  Technical report EDMS 1844850, CERN, 2017.
  bib  mtmt  url  pdf
• Dániel Darvas, Enrique Blanco Viñuela, and István Majzik. What is special about PLC software model checking? - Extended version.
  Technical report EDMS 1851093, CERN, 2017.
  bib  url
• Dániel Darvas, Enrique Blanco Viñuela, and István Majzik. Syntax and semantics of PLCspecif.
  Report EDMS 1523877, CERN, 2015.
  bib  mtmt  url
• Borja Fernández Adiego, Dániel Darvas, Jean-Charles Tournier, Enrique Blanco Viñuela, Jan Olaf Blech, and Víctor M. González Suárez. Automated generation of formal models from ST control programs for verification purposes.
  Internal Note CERN-ACC-NOTE-2014-0037, CERN, 2014.
  bib  mtmt  url
• Dániel Darvas, Borja Fernández Adiego, and Enrique Blanco Viñuela. Transforming PLC programs into formal models for verification purposes.
  Internal Note CERN-ACC-NOTE-2013-0040, CERN, 2013.
  bib  mtmt  url

Local events

• Dániel Darvas, István Majzik, and Enrique Blanco Viñuela. Well-formedness and invariant checking of PLCspecif specifications.
  In Proceedings of the 24th PhD Mini-Symposium, pp. 10-13. Budapest University of Technology and Economics, Department of Measurement and Information Systems, 2017.
  doi  bib  mtmt  url  pdf
• Dániel Darvas, István Majzik, and Enrique Blanco Viñuela. Generic representation of PLC programming languages for formal verification.
  In Proceedings of the 23rd PhD Mini-Symposium, pp. 6-9. Budapest University of Technology and Economics, Department of Measurement and Information Systems, 2016.
  doi  bib  mtmt  url  pdf
• Dániel Darvas. Practice-oriented formal methods for PLC programs of industrial control systems.
  In Proceedings of the PhD Symposium at iFM'16 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM'16). Reykjavik University, 2016. Extended abstract. Proceedings number: RUTR-SCS16002.
  bib  pdf
• Dániel Darvas, István Majzik, and Enrique Blanco Viñuela. Requirements towards a formal specification language for PLCs.
  In Proceedings of the 22nd PhD Mini-Symposium, pp. 18-21. Budapest University of Technology and Economics, Department of Measurement and Information Systems, 2015.
  doi  bib  mtmt  url  pdf
• Dániel Darvas and András Vörös. Szaturációalapú tesztbemenet-generálás színezett Petri-hálókkal [in Hungarian; Saturation-based test input generation using coloured Petri nets].
  In Mesterpróba 2013. Konferenciakiadvány, pp. 48-51. Budapest University of Technology and Economics, 2013.
  bib  mtmt  url  pdf
• Dániel Darvas. Szaturáció alapú korlátos modellellenőrzési technikák Petri-hálók analízisére [in Hungarian; Saturation based bounded model checking methods for the analysis of Petri nets].
  In XVII. Fiatal Műszakiak Tudományos Ülésszaka, pp. 83-86, Cluj Napoca, Romania, 2012. Erdélyi Múzeum-Egyesület Műszaki Tudományok Szakosztálya.
  bib  mtmt  url  pdf
• Dániel Darvas and Attila Jámbor. Komplex rendszerek modellezése és verifikációja [in Hungarian; Modeling and verification of complex systems].
  Scientific students' association report, 2011. 1st prize on the Competition of the Scientific Students' Association, Budapest University of Technology and Economics.
  bib  url  pdf
• Dániel Darvas. Szaturáció alapú automatikus modellellenőrző fejlesztése aszinkron rendszerekhez [in Hungarian; Implementing a saturation-based model checker of asynchronous systems].
  Scientific students' association report, 2010. 1st prize on the Competition of the Scientific Students' Association, Budapest University of Technology and Economics.
  bib  pdf

Selected talks

• Dániel Darvas. Bounded saturation based CTL model checking, Presented at the 12th Symposium on Programming Languages and Software Tools, 06/10/2011. url
• Dániel Darvas. Domain-specific languages -- What, how and when?, Presented at the CERN ICE Tea meeting, 21/02/2014. url
• Dániel Darvas. Formal verification of industrial control systems at CERN, Presented at the VTSA 2014 Student Session, 30/10/2014. url
• Dániel Darvas. Verification of a safety PLC program, Presented at the RVT Day, Fault Tolerant Systems Research Group, Budapest University of Technology and Economics, 29/05/2015. url
• Dániel Darvas. Formal verification of industrial control systems... at CERN, Presented at the 1st Developers@CERN Forum on Software Quality, Reliability and Testing, 29/09/2015. url
• Dániel Darvas. Quantitative and formal methods for the industrial control systems at CERN, Presented at the Dagstuhl Seminar on Formal Evaluation of Critical Infrastructures, 07/12/2015. url
• Dániel Darvas. Spécification formelle pour les API (PLCspecif) [in French], Presented at the CERN-ESTEREL Technical Seminar, 21/01/2016. url
• Dániel Darvas. Formal verification of industrial control systems, Presented at the 3th Workshop on PLC/COTS-based Interlock and Protection Systems, 02/02/2016. url
• Dániel Darvas. Conformance checking for PLC programs and specifications, Presented at the 11th IEEE International Symposium on Industrial Embedded Systems, 23/05/2016. url
• Dániel Darvas. Formal verification of safety PLC based control software, Presented at the 12th International Conference on Integrated Formal Methods, 03/06/2016. url
• Dániel Darvas. Practice-oriented formal methods for PLC programs of industrial control systems, Presented at the PhD Symposium at iFM'16 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM'16), 05/06/2016. url
• Dániel Darvas. PLC code generation based on a formal specification language, Presented at the 14th IEEE International Conference on Industrial Informatics, 20/07/2016. url
• István Majzik, Dániel Darvas. PLCverif: Model checking PLC programs (case study), Presented at the Formal Methods course, Budapest University of University of Technology and Economics, 22/02/2017. url
• Dániel Darvas. Practice-oriented formal methods to support the software development of industrial control systems, Presented at the Ph.D. defence, 15/05/2017. url
• Dániel Darvas. Finding bugs in the LHC: Verification methods for PLC programs, Presented at the Alpine Verification Meeting 2017, 18/09/2017. url

Generated at: 29/08/2023