Optimization techniques and formal verification for the software design of boolean algebra based safety-critical systems J Perez, JL Flores, C Blum, J Cerquides, A Abuin IEEE Transactions on Industrial Informatics 18 (1), 620-630, 2021 | 7 | 2021 |
Towards certified model checking for PLTL using one-pass tableaux A Abuin, A Bolotov, U de Cerio, M Hermo, P Lucio Leibniz International Proceedings in Informatics 147, 12, 2019 | 7 | 2019 |
One-pass context-based tableaux systems for CTL and ECTL A Abuin, A Bolotov, M Hermo, P Lucio Leibniz International Proceedings in Informatics 178, 14, 2020 | 5 | 2020 |
Tableaux and sequent calculi for CTL and ECTL: Satisfiability test with certifying proofs and models A Abuin, A Bolotov, M Hermo, P Lucio Journal of Logical and Algebraic Methods in Programming 130, 100828, 2023 | 4 | 2023 |
Using contexts in tableaux for pltl: An illustrative example A Abuin, A Bolotov, UD de Cerio, M Hermo, P Lucio Proceedings of the 26th Automated Reasoning Workshop, 23, 2019 | 2 | 2019 |
Context-based model checking using smt-solvers (work in progress) A Abuin, UD de Cerio, M Hermo, P Lucio PROLE2018. SISTEDES, 2018 | 2 | 2018 |
Towards the automatic verification of QCSP tractability results A Abuin, H Chen, M Hermo, P Lucio Proceedings of the XVII Jornadas sobre Programación y Lenguajes (PROLE 2017), 2017 | 2 | 2017 |
Tableaux and Sequent Calculi for CTL and ECTL: Satisfiability Test with Certifying Proofs and Models A Bolotov, M Garcia-Closas, P Lucio, A Abuin Journal of Logical and Algebraic Methods in Programming 130, 2022 | | 2022 |
Verified Model Checking for Conjunctive Positive Logic A Abuin, UD de Cerio, M Hermo, P Lucio SN Computer Science 2 (5), 344, 2021 | | 2021 |