Recent Submissions

  • On the power of symmetric linear programs 

    Atserias, Albert; Dawar, Anuj; Ochremiak, Joanna (Institute of Electrical and Electronics Engineers (IEEE), 2019)
    Conference report
    Open Access
    We consider families of symmetric linear programs (LPs) that decide a property of graphs (or other relational structures) in the sense that, for each size of graph, there is an LP defining a polyhedral lift that separates ...
  • Size-degree trade-offs for Sums-of-Squares and Positivstellensatz proofs 

    Atserias, Albert; Hakoniemi, Tuomas Antero (Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019)
    Conference report
    Open Access
    We show that if a system of degree-k polynomial constraints on n Boolean variables has a Sums-of-Squares (SOS) proof of unsatisfiability with at most s many monomials, then it also has one whose degree is of the order of ...
  • Circular (yet sound) proofs 

    Atserias, Albert; Lauria, Massimo (Springer, 2019)
    Conference report
    Open Access
    We introduce a new way of composing proofs in rule-based proof systems that generalizes tree-like and dag-like proofs. In the new definition, proofs are directed graphs of derived formulas, in which cycles are allowed as ...
  • RTL-aware dataflow-driven macro placement 

    Vidal Obiols, Alexandre; Cortadella, Jordi; Petit Silvestre, Jordi; Galcerán Oms, Marc; Martorell Cid, Ferran (Institute of Electrical and Electronics Engineers (IEEE), 2019)
    Conference report
    Open Access
    When RTL designers define the hierarchy of a system, they exploit their knowledge about the conceptual abstractions devised during the design and the functional interactions between the logical components. This valuable ...
  • The dynamic pipeline paradigm 

    Zoltán, Cristina; Pasarella Sánchez, Ana Edelmira; Aráoz Durand, Julián Arturo; Vidal, Maria-Esther (Sociedad de Ingeniería de Software y Tecnologías de Desarrollo de Software (SISTEDES), 2019)
    Conference report
    Open Access
    Nowadays, in the era of Big Data and Internet of Things, large volumes of data in motion are produced in heterogeneous formats, frequencies, densities, and quantities. In general, data is continuously produced by diverse ...
  • Exact and heuristic allocation of multi-kernel applications to multi-FPGA platforms 

    Shan, Junnan; Casu, Mario R.; Cortadella, Jordi; Lavagno, Luciano; Lazarescu, Mihai T.
    Conference report
    Open Access
    FPGA-based accelerators demonstrated high energy efficiency compared to GPUs and CPUs. However, single FPGA designs may not achieve sufficient task parallelism. In this work, we optimize the mapping of high-performance ...
  • Sesquickselect: One and a half pivots for cache-efficient selection 

    Martínez Parra, Conrado; Nebel, Markus; Wild, Sebastian (Curran, 2019)
    Conference report
    Open Access
    Because of unmatched improvements in CPU performance, memory transfers have become a bottleneck of program execution. As discovered in recent years, this also affects sorting in internal memory. Since partitioning around ...
  • Genet: a tool for the synthesis and mining of Petri nets 

    Carmona Vargas, Josep; Cortadella, Jordi; Kishinevsky, Michael (Institute of Electrical and Electronics Engineers (IEEE), 2009)
    Conference report
    Open Access
    State-based representations of concurrent systems suffer from the well known state explosion problem. In contrast, Petri nets are good models for this type of systems both in terms of complexity of the analysis and in ...
  • Lazy transition systems: application to timing optimization of asynchronous circuits 

    Cortadella, Jordi; Kishinevsky, Michael; Kondratyev, Alex; Lavagno, Luciano; Taubin, Alexander; Yakovlev, Alex (Institute of Electrical and Electronics Engineers (IEEE), 1998)
    Conference report
    Open Access
    The paper introduces Lazy Transitions Systems (LzTSs). The notion of laziness explicitly distinguishes between the enabling and the firing of an event in a transition system. LzTSs can be effectively used to model the ...
  • Petrify: a tool for manipulating concurrent specifications and synthesis of asynchronous controllers 

    Cortadella, Jordi; Kishinevsky, Michael; Kondratyev, Alex; Lavagno, Luciano; Yakovlev, Alex (Universitat Politècnica de Catalunya (UPC), 1996)
    Conference report
    Open Access
    Petrifyis a tool for (1) manipulating concurrent specifications and (2) synthesis and optimization of asynchronous control circuits. Given a Petri Net (PN), a Signal Transition Graph (STG), or a Transition ...
  • Task generation and compile-time scheduling for mixed data-control embedded software 

    Cortadella, Jordi; Kondratyev, Alex; Lavagno, Luciano; Massot, Marc; Moral Boadas, Sandra; Passerone, Claudio; Watanabe, Yosinori; Sangiovanni-Vincentelli, Alberto (Association for Computing Machinery (ACM), 2000)
    Conference report
    Open Access
    The problem of optimal software synthesis for concurrent processes to be implemented on a single processor is addressed. The approach calls for the representation of the concurrent processes with Petri nets that give a ...
  • Verification of asynchronous circuits by BDD-based model checking of Petri nets 

    Roig Mansilla, Oriol; Cortadella, Jordi; Pastor Llorens, Enric (Springer, 1995)
    Conference report
    Open Access
    This paper presents a methodology for the verification of speed-independent asynchronous circuits against a Petri net specification. The technique is based on symbolic reachability analysis, modeling both the specification ...

View more