150 citations
- University of LisbonPT6 papers
- Carnegie Mellon UniversityUS2 papers
- University College DublinIE2 papers
- Center for Theoretical PhysicsPL1 paper
- Centre National de la Recherche ScientifiqueFR1 paper
- Google (United States)US1 paper
- Instituto de Novas TecnologiasPT1 paper
- Instituto de TelecomunicaçõesPT1 paper
- Iscte – Instituto Universitário de LisboaPT1 paper
- Laboratoire Interdisciplinaire des Sciences du NumériqueFR1 paper
- LIP - Laboratory of Instrumentation and Experimental Particle PhysicsPT1 paper
- Queen Mary University of LondonGB1 paper
12 papers
Solving QBF with Counterexample Guided Refinement
Mikoláš Janota, William Klieber, Joao Marques-Silva +1
We propose two novel approaches for using Counterexample-Guided Abstraction Refinement (CEGAR) in Quantified Boolean Formula (QBF) solvers. The first approach develops a recursive…
Solving QBF by Clause Selection
Mikoláš Janota, Joao Marques-Silva
Algorithms based on the enumeration of implicit hitting sets find a growing number of applications, which include maximum satisfiability and model based diagnosis, among others. Th…
Welterweight Go: Boxing, Structural Subtyping, and Generics (Extended Version)
Raymond Hu, Julien Lange, Bernardo Toninho +3
Go's unique combination of structural subtyping between generics and types with non-uniform runtime representations presents significant challenges for formalising the language. We…
General-relativistic and non-ideal radiative cooling in neutron star magnetospheres
João Joaquim, Francisco Assunção, Pablo J. Bilbao +1
Radiation reaction cooling plays an important role in describing the extreme plasma conditions found in the magnetospheres of astrophysical compact objects. Strong electromagnetic…
CARM Tool: Cache-Aware Roofline Model Automatic Benchmarking and Application Analysis
José Morgado, Leonel Sousa, Aleksandar Ilic
In recent years, HPC systems and CPU architectures as their central components, have become increasingly complex, making application development and optimization quite challenging.…
PRISM: Processing-In-Memory Sparse MTTKRP for Tensor Decomposition Acceleration
Daniel Pacheco, Leonel Sousa, Aleksandar Ilic
Sparse tensors are the most used representation of sparse multidimensional data. Operations that decompose them, selecting their most important features while reducing their dimens…