???global.info.a_carregar???
Identification

Personal identification

Full name
Néstor Cataño

Citation names

  • Cataño, Néstor

Author identifiers

Ciência ID
3012-389B-281D
ORCID iD
0000-0001-5015-5893
Education
Degree Classification
2001/08/01 - 2004/08/01
Concluded
 Formal Methods for Java Programs (Doktor (PhD))
Major in Formal Methods
Université de Paris, France
Affiliation

Science

Category
Host institution 		Employer
2020/01/01 - 2022/01/01 Coordinating Researcher (Research) Rochester Institute of Technology, United States

Teaching in Higher Education

Category
Host institution 		Employer
2015/01/01 - 2018/01/01 Associate Professor (University Teacher) Universitet Innopolis, Russia
2008/01/01 - 2014/01/01 Assistant Professor (University Teacher) Universidade da Madeira, Portugal
Projects

Contract

Designation Funders
2009/01/01 - 2013/01/01 WeSP: Web Security and Privacy with human and policy considerations
CMU-PT/SE/0028/2008
Researcher
Associação para a Inovação e Desenvolvimento da FCT, Portugal
Concluded
2009/01/01 - 2013/01/01 Aeminium: Freeing Programmers from the Shackles of Sequentially
CMU-PT/SE/0038/2008
Researcher
Associação para a Inovação e Desenvolvimento da FCT, Portugal
Concluded
2011/01/01 - 2012/01/01 B2Dafny: Extending Boogie to Support the Analysis of B Machines
SEIF
Principal investigator
Microsoft Research, United States
Concluded
2009/01/01 - 2012/01/01 Favas: A Formal Verification Platform for Real-Time Systems
PTDC/EIA-CCO/105034/2008
Principal investigator
Associação para a Inovação e Desenvolvimento da FCT, Portugal
 Associação para a Inovação e Desenvolvimento da FCT
Concluded
Outputs

Publications

Journal article
  1. Cataño, N.; Ahmed, I.; Siminiceanu, R.I.; Aldrich, J.. "A case study on the lightweight verification of a multi-threaded task server". Science of Computer Programming (2013): http://www.scopus.com/inward/record.url?eid=2-s2.0-84874035905&partnerID=MN8TOARS.
    10.1016/j.scico.2013.01.004
  2. Cataño, N.; Leino, K.R.M.; Rivera, V.. "The EventB2Dafny Rodin plug-in". 2012 2nd International Workshop on Developing Tools as Plug-Ins, TOPI 2012 - Proceedings (2012): 49-54. http://www.scopus.com/inward/record.url?eid=2-s2.0-84864225584&partnerID=MN8TOARS.
    10.1109/TOPI.2012.6229810
  3. Cataño, N.; Wahls, T.; Rueda, C.; Rivera, V.; Yu, D.. "Translating B machines to JML specifications". Proceedings of the ACM Symposium on Applied Computing (2012): 1271-1277. http://www.scopus.com/inward/record.url?eid=2-s2.0-84863588132&partnerID=MN8TOARS.
    10.1145/2245276.2231978
  4. Cataño, N.; Hanvey, S.; Rueda, C.. "Poporo: A formal methods tool for fast-checking of social network privacy policies". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 7304 LNCS (2012): 9-16. http://www.scopus.com/inward/record.url?eid=2-s2.0-84862199146&partnerID=MN8TOARS.
    10.1007/978-3-642-30561-0_2
  5. Olarte, C.; Rueda, C.; Pimentel, E.; Cataño, N.. "A linear concurrent constraint approach for the automatic verification of access permissions". PPDP'12 - Proceedings of the 2012 ACM SIGPLAN Principles and Practice of Declarative Programming (2012): 207-219. http://www.scopus.com/inward/record.url?eid=2-s2.0-84867525651&partnerID=MN8TOARS.
    10.1145/2370776.2370802
  6. Cataño, N.; Rueda, C.; Hanvey, S.. "Verification of JML generic types with Yices". 2011 6th Colombian Computing Congress, CCC 2011 (2011): http://www.scopus.com/inward/record.url?eid=2-s2.0-79960695338&partnerID=MN8TOARS.
    10.1109/COLOMCC.2011.5936279
  7. Cataño, N.; Ahmed, I.. "Lightweight verification of a multi-task threaded server: A case study with the plural tool". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 6959 LNCS (2011): 6-20. http://www.scopus.com/inward/record.url?eid=2-s2.0-80052705925&partnerID=MN8TOARS.
    10.1007/978-3-642-24431-5_3
  8. Catano, N.; Rueda, C.. "Matelas: A predicate calculus common formal definition for social networking". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 5977 LNCS (2010): 259-272. http://www.scopus.com/inward/record.url?eid=2-s2.0-77950804437&partnerID=MN8TOARS.
    10.1007/978-3-642-11811-1_20
  9. Catano, N.; Rueda, C.. "Teaching formal methods for the unconquered territory". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 5846 LNCS (2009): 2-19. http://www.scopus.com/inward/record.url?eid=2-s2.0-71549124368&partnerID=MN8TOARS.
    10.1007/978-3-642-04912-5_2
  10. Cataño, N.; Barraza, F.; García, D.; Ortega, P.; Rueda, C.. "A Case Study in JML-Assisted Software Development". Electronic Notes in Theoretical Computer Science 240 C (2009): 5-21. http://www.scopus.com/inward/record.url?eid=2-s2.0-67649422449&partnerID=MN8TOARS.
    10.1016/j.entcs.2009.05.042
  11. Cataño, N.. "Formal modeling of a slicing algorithm for Java event spaces in PVS". Lecture Notes in Computer Science 3603 (2005): 82-97. http://www.scopus.com/inward/record.url?eid=2-s2.0-26844534996&partnerID=MN8TOARS.
  12. Breunesse, C.-B.; Cataño, N.; Huisman, M.; Jacobs, B.. "Formal methods for smart cards: An experience report". Science of Computer Programming 55 1-3 SPEC. (2005): 53-80. http://www.scopus.com/inward/record.url?eid=2-s2.0-13144257773&partnerID=MN8TOARS.
    10.1016/j.scico.2004.05.011
  13. Cataño, N.; Huisman, M.. "CHASE: A static checker for JML's assignable clause". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2575 (2003): 26-40. http://www.scopus.com/inward/record.url?eid=2-s2.0-35248836879&partnerID=MN8TOARS.
  14. Cataño, N.. "Slicing event spaces: Towards a Java programs checking framework". Electronic Notes in Theoretical Computer Science 80 (2003): 63-78. http://www.scopus.com/inward/record.url?eid=2-s2.0-18944403823&partnerID=MN8TOARS.
    10.1016/S1571-0661(04)80809-0

Other

Other output
  1. Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS. Lecture Notes in Computer Science. 2005.
    10.1007/11541868_6
  2. CHASE:A Static Checker for JML’s Assignable Clause. Lecture Notes in Computer Science. 2003.
    10.1007/3-540-36384-x_6
  3. Formal Specification and Static Checking of Gemplus’ Electronic Purse Using ESC/Java. Lecture Notes in Computer Science. 2002.
    10.1007/3-540-45614-7_16