Complutense Group on Program Analyis and Transformation
COSTA
Universitat Politècnica de Catalunya
Barcelona, EspañaPublicacións en colaboración con investigadores/as de Universitat Politècnica de Catalunya (53)
2023
-
Circom: A Circuit Description Language for Building Zero-Knowledge Applications
IEEE Transactions on Dependable and Secure Computing, Vol. 20, Núm. 6, pp. 4733-4751
2019
-
The Termination and Complexity Competition
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2018
-
Constrained dynamic partial order reduction
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
-
EthIR: A Framework for High-Level Analysis of Ethereum Bytecode
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
-
SDN-Actors: Modeling and verification of SDN programs
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2017
-
Proving termination through conditional termination
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2016
-
Speeding up the constraint-based method in difference logic
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2015
-
Compositional safety verification with Max-SMT
Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015
-
Normal higher-order termination
ACM Transactions on Computational Logic, Vol. 16, Núm. 2
-
Termination competition (TermCOMP 2015)
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
-
The computability path ordering
Logical Methods in Computer Science, Vol. 11, Núm. 4
2014
-
Minimal-model-guided approaches to solving polynomial constraints and extensions
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
-
Proving non-termination using max-SMT
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2013
-
Paramodulation with non-monotonic orderings and simplification
Journal of Automated Reasoning, Vol. 50, Núm. 1, pp. 51-98
-
Proving termination of imperative programs using Max-SMT
2013 Formal Methods in Computer-Aided Design, FMCAD 2013
-
SMT-based array invariant generation
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
-
The recursive path and polynomial ordering for first-order and higher-order terms
Journal of Logic and Computation, Vol. 23, Núm. 1, pp. 263-305
2012
-
Nominal completion for rewrite systems with binders
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
-
SAT modulo linear arithmetic for solving polynomial constraints
Journal of Automated Reasoning, Vol. 48, Núm. 1, pp. 107-131
2009
-
Solving non-linear polynomial arithmetic via SAT modulo linear arithmetic
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)