Castellano

 

Maximiliano Cristiá
     

Professional

  

Head Professor
LCC - FCEIA - UNR

Director of the Software Engineering Group at CIFASIS

Curriculum Vitae
   
Courses  

System Analysis (first semester)

Software Engineering (second semester)

Formal Models in Information Security (2003)
   
I+D  

Research interests: formal methods, software architecture and design, model-based testing, multi-level security, tool development to assist and automate software development.

Tool development

  • Flowx. A multi-level Linux version implementing a noninterference model. Project co-founded by FONTAR.
  • Repose. Rapid prototyping using office software.
  • StateSim. Graphical Statecharts simulator.
  • Fastest 1.6. Model-based testing tool for the Z notation. It requires SWI-Prolog (versions before 7.2) and Java to be already installed (it can also work with other versions of Prolog). In MS Windows systems, swipl.exe must be renamed to prolog.exe.

Miembro de comité de programa

ACM SAC-SVT 2017 -- ASSE 2016 -- LADC 2016 -- ACM SAC-SVT 2016 -- FMSEET 2015 -- SETS 2015 -- JUI 2015 -- EST 2015 -- ACM SAC-SVT 2015 -- DEVS/TMS

Publications

  1. Juan Campo Camila Sanz Maximiliano Cristiá Felipe Gorostiaga Carlos Luna, Gustavo Betarte. A formal approach for the verification of the permission-based security model of Android. CLEI Electron. J., 2018. to appear.
  2. Maximiliano Cristiá, Diego Hollmann, and Claudia Frydman. A multi-target compiler for CML-DEVS. Simulation, 2018. to appear.
  3. Gustavo Betarte, Juan Campo, Maximiliano Cristiá, Felipe Gorostiaga, Carlos Luna, and Camila Sanz. Towards formal model-based analysis and testing of Android's security mechanisms. In XLIII Latin American Computing Conference, CLEI 2017, Córdoba, Argentina, September 4-8, 2017.
  4. Maximiliano Cristiá, Gianfranco Rossi, and Claudia Frydman. Using a set constraint solver for program verification. In Proceedings 4th Workshop on Horn Clauses for Verification and Synthesis, HCVS@CADE 2017, Gothenburg, Sweden, 7th August 2017., 2017.
  5. Maximiliano Cristiá and Gianfranco Rossi. A decision procedure for restricted intensional sets. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 185-201. Springer, 2017.
  6. Maximiliano Cristiá and Gianfranco Rossi. A decision procedure for sets, binary relations and partial functions. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, volume 9779 of Lecture Notes in Computer Science, pages 179-198. Springer, 2016.
  7. Maximiliano Cristiá, Joaquín Cuenca and Claudia Frydman. Coverage criteria for set-based specifications. RITA, 22(2):316-335 (2015).
  8. Maximiliano Cristiá, Gianfranco Rossi and Claudia Frydman. Adding partial functions to constraint logic programming with sets. Theory and Practice of Logic Programming, 15(4-5):651-665 (2015).
  9. Diego A. Hollmann, Maximiliano Cristiá and Claudia Frydman. CML-DEVS: A specification language for DEVS a conceptual models. Simulation Modelling Practice and Theory 57: 100-117 (2015).
  10. Maximiliano Cristiá, Gianfranco Rossi and Claudia Frydman. First steps in integrating {log} into Z/EVES. In 2nd International Workshop about Sets and Tools (SETS 2015), 2015.
  11. Maximiliano Cristiá, Gianfranco Rossi and Claudia Frydman. Helping programmers to adopt set-based specifications. In Andreas Bollin, Tiziana Margaria, and Isabelle Perseil, editors. Proceedings of the First Workshop on Formal Methods in Software Engineering Education and Training, FMSEE&T 2015, co-located with 20th International Symposium on Formal Methods (FM 2015), Oslo, Norway, June 23, 2015, volume 1385 of CEUR Workshop Proceedings. CEUR-WS.org, 2015, pages 3-10.
  12. Maximiliano Cristiá. Why, how and what should be taught about formal methods? . In Andreas Bollin, Tiziana Margaria, and Isabelle Perseil, editors. Proceedings of the First Workshop on Formal Methods in Software Engineering Education and Training, FMSEE&T 2015, co-located with 20th International Symposium on Formal Methods (FM 2015), Oslo, Norway, June 23, 2015, volume 1385 of CEUR Workshop Proceedings. CEUR-WS.org, 2015, pages 1-2.
  13. Maximiliano Cristiá and Claudia Frydman. Formal and semi-formal verification of a web voting system . IJWIS 11(2): 183-204 (2015).
  14. Diego A. Hollmann, Maximiliano Cristiá and Claudia Frydman. A family of simulation criteria to guide DEVS models validation rigorously, systematically and semi-automatically. Simulation Modelling Practice and Theory 49: 1-26 (2014).
  15. Maximiliano Cristiá, Joaquín Cuenca and Claudia Frydman. Coverage Criteria for Logical Specifications. In Proceedings of the 8th Brazilian Workshop on Systematic and Automated Software Testing (SAST'14), pages 11-20, 2014.
  16. Maximiliano Cristiá and Claudia Frydman. A functional verification of a web voting system. In Beniamino Murgante, Sanjay Misra, Ana Maria A. C. Rocha, Carmelo Maria Torre, Jorge Gustavo Rocha, Maria Irene Falcao, David Taniar, Bernady O. Apduhan, and Osvaldo Gervasi, editors, ICCSA (1), volume 8579 of Lecture Notes in Computer Science, pages 640-655. Springer, 2014.
  17. Maximiliano Cristiá and Gianfranco Rossi. Rapid prototyping and animation of Z specifications using {log}. In 1st International Workshop about Sets and Tools (SETS 2014), pages 4-18, 2014.
  18. Maximiliano Cristiá, Joaquín Mesuro and Claudia Frydman. Integration Testing in the Test Template Framework. In Stefania Gnesi and Arend Rensink, editors, FASE, volume 8411 of Lecture Notes in Computer Science, pages 400-414. Springer, 2014.
  19. Maximiliano Cristiá, Pablo Albertengo, Claudia Frydman, Brian Plüss and Pablo Rodríguez Monetti. Tool support for the Test Template Framework. Software Testing, Verification and Reliability, 24(1):3-37, 2014.
  20. Maximiliano Cristiá and Gianfranco Rossi. Using {log} as a Test Case Generator for Z Specifications. Presented at 28-esimo Convegno Italiano di Logica Computazionale, CILC 2013, 2013.
  21. Maximiliano Cristiá, Gianfranco Rossi and Claudia Frydman. {log} as a Test Case Generator for the Test Template Framework. In Robert M. Hierons, Mercedes Merayo, and Mario Bravetti, editors, SEFM, volume 8137 of Lecture Notes in Computer Science, pages 229-243. Springer, 2013.
  22. Maximiliano Cristiá and Claudia Frydman. Extending the Test Template Framework to deal with axiomatic descriptions, quantifiers and set comprehensions. In John Derrick, John Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves, and Elvinia Riccobene, editors, ASM, volume 7316 of Lecture Notes in Computer Science, pages 280-293. Springer, 2012.
  23. Diego Hollmann, Maximiliano Cristiá and Claudia Frydman. Adapting Model-Based Testing Techniques to DEVS Models Validation. In Proceedings Symposium on Theory of Modeling & Simulation 2012 (TMS/DEVS), Orlando, USA, 2012.
    Mejor artículo del Symposium on Theory of Modeling & Simulation 2012 (TMS/DEVS) y artículo finalista de la Spring Simulation Multi-Conference 2012 en reconocimiento a su calidad, originalidad e importancia para el modelado y la simulación.
  24. Maximiliano Cristiá and Claudia Frydman. Applying SMT Solvers to the Test Template Framework. In Proceedings 7th Workshop on Model-Based Testing, Tallinn, Estonia, 25 March 2012, Electronic Proceedings in Theoretical Computer Science 80, Open Publishing Association, pp. 28-42.
  25. Maximiliano Cristiá, Diego Hollmann, Pablo Albertengo, Claudia Frydman and Pablo Rodríguez Monetti. A Language for Test Case Refinement in the Test Template Framework. In Formal Methods and Software Engineering, 13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28, 2011.
  26. Maximiliano Cristiá, Pablo Albertengo, Claudia Frydman, Brian Plüss and Pablo Rodríguez Monetti. Applying the Test Template Framework to Aerospace Software. In Proceedings of the 34th IEEE Annual Software Engineering Workshop, 2011, Limerik, Ireland.
  27. Maximiliano Cristiá. Soporte Herramental para el Test Template Framework. En Anales del XIII Workshop de Investigadores en Ciencias de la Computación, 2011, Rosario, Argentina.
  28. Norbert Giambiasi, Diego Llarrull and Maximiliano Cristiá. System State Identification Using DEVS. In Gabriel A. Wainer and Pieter J. Mosterman eds.: Discrete-Event Modeling and Simulation: Theory and Applications. CRC Press Taylor & Francis Group, (2010).
  29. Maximiliano Cristá, Pablo Albertengo and Pablo Rodríguez Monetti. Fastest: a Model-Based Testing Tool for the Z Notation. In 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM), 2010. Posters and Tool Demo Session Track. Pisa, Italy.
  30. Maximiliano Cristiá, Pablo Albertengo and Pablo Rodríguez Monetti. Pruning Testing Trees in the Test Template Framework by Detecting Mathematical Contradictions. In 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM), 2010. Pisa, Italy.
  31. Maximiliano Cristiá and Brian Plüss. Generating Natural Language Descriptions of Z Test Cases. International Natural Language Generation Conference (INLG), 2010. Dublin, Ireland. (short paper)
  32. Maximiliano Cristiá, Valdivino Alexandre and N. L. Vijaykumar. On Comparing and Complementing Two MBT Approaches. In 11th IEEE Latin-American Test Workshop (LATW10), Punta del Este, Uruguay, 2010.
  33. Maximiliano Cristiá and Pablo Rodríguez Monetti. Implementing and Applying the Stocks-Carrington Framework for Model-Based Testing. In Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009.
  34. Maximiliano Cristiá and Pablo Mata. Runtime Enforcement of Noninterference by Duplicating Processes and their Memories. In Workshop de Seguridad Informática WSEGI 2009 (38 JAIIO), 2009. Mar del Plata, Argentina.
  35. Alejandro Sartorio and Maximiliano Cristiá. First Approximation to DHD Design and Implementation. In CLEI Electroninc Journal 12(3), 2009.
  36. Alejandro Sartorio and Maximiliano Cristiá. Primera Aproximación al Diseño e Implementación de los DHD. In Proceedings of XXXIV Conferencia Latinoamericana de Informática, 2008. Santa Fe, Argentina.
  37. Maximiliano Cristiá. Formalizing the Semantics of Modular DEVS Models with Temporal Logic. In Proceedings of 7ème Conférence Internationale de Modélisation, Optimisation et Simulation des Systèmes MOSIM 08, 2008. París, Francia.
  38. Maximiliano Cristiá. A TLA+ Encoding of DEVS Models. In Proceedings of the International Modeling and Simulation Multiconference, 2007. Buenos Aires, Argentina.
  39. Maximiliano Cristiá. Teaching Formal Methods in a Third World Country: What, Why and How. In Proceedings of Teaching Formal Methods 2006. London, UK.
  40. Maximiliano Cristiá, Gisela Giusti and Felipe Manzano. The Implementation of Lisex, a MLS Linux Prototype. In Proceedings of the 6th ASSE, 34th JAIIO, 2005. Rosario, Argentina.
  41. Maximiliano Cristiá. Formal verification of an extension of a secure, compatible UNIX file system. In Anales de la XXIX Conferencia Latinoamericana de Informtica, 2003. La Paz, Bolivia.
   
Contacto  

Universidad Nacional de Rosario
Facultad de Ciencias Exactas, Ingeniería y Agrimensura
Departamento de Ciencias de la Computación
Pellegrini 250
(2000) Rosario
Argentina

(54-341)4385559

cristia -AT- cifasis-conicet.gov.ar
   
Top   Last update: 04/2010
http://www.fceia.unr.edu.ar/~mcristia