| Proving non-termination using Max-SMT D Larraz, K Nimkar, A Oliveras, E Rodríguez-Carbonell, A Rubio Computer Aided Verification: 26th International Conference, CAV 2014, Held …, 2014 | 70 | 2014 |
| Proving termination of imperative programs using Max-SMT D Larraz, A Oliveras, E Rodríguez-Carbonell, A Rubio 2013 Formal Methods in Computer-Aided Design, 218-225, 2013 | 68 | 2013 |
| SMT-based array invariant generation D Larraz, E Rodríguez-Carbonell, A Rubio International Workshop on Verification, Model Checking, and Abstract …, 2013 | 49 | 2013 |
| Proving termination through conditional termination C Borralleras, M Brockschmidt, D Larraz, A Oliveras, ... International Conference on Tools and Algorithms for the Construction and …, 2017 | 43 | 2017 |
| Minimal-model-guided approaches to solving polynomial constraints and extensions D Larraz, A Oliveras, E Rodríguez-Carbonell, A Rubio International Conference on Theory and Applications of Satisfiability …, 2014 | 24 | 2014 |
| SYSLITE: syntax-guided synthesis of PLTL formulas from finite traces MF Arif, D Larraz, M Echeverria, A Reynolds, O Chowdhury, C Tinelli # PLACEHOLDER_PARENT_METADATA_VALUE# 1, 93-103, 2020 | 23 | 2020 |
| Verdict: a language and framework for engineering cyber resilient and safe system B Meng, D Larraz, K Siu, A Moitra, J Interrante, W Smith, S Paul, D Prince, ... Systems 9 (1), 18, 2021 | 22 | 2021 |
| Architectural and behavioral analysis for cyber security K Siu, A Moitra, M Li, M Durling, H Herencia-Zapana, J Interrante, B Meng, ... 2019 IEEE/AIAA 38th Digital Avionics Systems Conference (DASC), 1-10, 2019 | 21 | 2019 |
| Extending enumerative function synthesis via SMT-driven classification H Barbosa, A Reynolds, D Larraz, C Tinelli 2019 Formal Methods in Computer Aided Design (FMCAD), 212-220, 2019 | 16 | 2019 |
| Compositional safety verification with Max-SMT M Brockschmidt, D Larra, A Oliveras, E Rodrıguez-Carbonell, A Rubio 2015 Formal Methods in Computer-Aided Design (FMCAD), 33-40, 2015 | 13 | 2015 |
| Incomplete SMT techniques for solving non-linear formulas over the integers C Borralleras, D Larraz, E Rodríguez-Carbonell, A Oliveras, A Rubio ACM Transactions on Computational Logic (TOCL) 20 (4), 1-36, 2019 | 11 | 2019 |
| Scalable algorithms for abduction via enumerative syntax-guided synthesis A Reynolds, H Barbosa, D Larraz, C Tinelli International Joint Conference on Automated Reasoning, 141-160, 2020 | 10 | 2020 |
| Speeding up the constraint-based method in difference logic L Candeago, D Larraz, A Oliveras, E Rodríguez-Carbonell, A Rubio International Conference on Theory and Applications of Satisfiability …, 2016 | 8 | 2016 |
| Merit and blame assignment with Kind 2 D Larraz, M Laurent, C Tinelli Formal Methods for Industrial Critical Systems: 26th International …, 2021 | 5 | 2021 |
| VeryMax: tool description for termCOMP 2016 C Borralleras, D Larraz, A Oliveras, JM Rivero, E Rodríguez-Carbonell, ... 15th International Workshop on Termination 18, 2016 | 5 | 2016 |
| CRV: Automated Cyber-Resiliency Reasoning for System Design Models. D Larraz, R Lorch, M Yahyazadeh, MF Arif, O Chowdhury, C Tinelli FMCAD, 209-220, 2023 | 2 | 2023 |
| Finding locally smallest cut sets using max-smt D Larraz, C Tinelli ACM SIGAda Ada Letters 42 (2), 32-39, 2023 | 2 | 2023 |
| Beyond model checking of idealized Lustre in Kind 2 D Larraz, A Viswanathan, C Tinelli, M Laurent ACM SIGAda Ada Letters 42 (2), 40-44, 2023 | 2 | 2023 |
| Realizability Checking of Contracts with Kind 2 D Larraz, C Tinelli arXiv preprint arXiv:2205.09082, 2022 | 1 | 2022 |
| A Comprehensive, Automated Security Analysis of the Uptane Automotive Over-the-Air Update Framework R Lorch, D Larraz, C Tinelli, O Chowdhury Proceedings of the 27th International Symposium on Research in Attacks …, 2024 | | 2024 |
Albert RubioProfessor of Computer Science, Complutense University of Madrid (UCM)Dirección de correo verificada de ucm.es
