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 | 69 | 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 | 67 | 2013 |
SMT-based array invariant generation D Larraz, E Rodríguez-Carbonell, A Rubio International Workshop on Verification, Model Checking, and Abstract …, 2013 | 48 | 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 | 44 | 2017 |
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 | 26 | 2020 |
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 |
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 | 17 | 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 | 14 | 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 | 12 | 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 |