Markus Püschel


Last Name

Püschel

First Name

Markus

ORCID

0000-0001-8834-8551

Organisational unit

03893 - Püschel, Markus / Püschel, Markus

Filters

2011 - 2019622020 - 202632
Reset filters

Search Results

Publications 1 - 10 of 94
  • Memory-efficient fast fourier transform on streaming data by fusing permutations
    Item type: Conference Paper
    Serre, François; Püschel, Markus (2018)
    Proceedings of the 2018 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays (FPGA)
  • Fast polyhedra abstract domain
    Item type: Conference Paper
    Singh, Gagandeep; Püschel, Markus; Vechev, Martin (2017)
    Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL'17
  • Improving Fixed-Point Accuracy of FFT Cores in O-OFDM Systems
    Item type: Other Conference Item
    Koutsoyannis, Robert; Milder, Peter; Berger, Christian R.; et al. (2012)
    IEEE International Conference on Acoustics, Speech and Signal Processing
  • ADMM For Consensus On Colored Networks
    Item type: Conference Paper
    Mota, João; Xavier, João; Aguiar, Pedro Q.; et al. (2012)
  • Accelerating Automated Program Verifiers by Automatic Proof Localization
    Item type: Conference Paper
    Gopinathan, Kiran; Spiliopoulos, Dionysios; Goyal, Vikram; et al. (2025)
    Lecture Notes in Computer Science ~ Computer Aided Verification
    Automated program verifiers such as Dafny, F, Verus, and Viper are now routinely used to verify real-world software. Unfortunately, the performance of the SMT solvers employed by these tools is not always able to keep up with the increasing size and complexity of verification problems, resulting in long verification times and verification failures due to time-outs. This performance degradation occurs because large SMT queries increase the search space for the SMT solver, in particular, the number of possible quantifier instantiations. Most existing attempts to mitigate this problem require substantial manual effort to reduce the size of the search space, for instance, by decomposing proofs. In this paper, we present an automatic technique to significantly improve the performance of SMT-based program proofs by drastically reducing the proof search space for each assertion, in particular, the performed quantifier instantiations. Starting from a successful verification, we automatically extract for each assertion the quantified axioms used by the SMT solver to show that the assertion is valid. Crucially, these include lurking axioms, which are logically irrelevant, but needed to trigger the instantiation of other, relevant axioms. We describe a novel proof localization algorithm that implements a semantics-preserving source-to-source translation of a program such that re-verifying an assertion in the optimized program uses only the axioms in its proof essence. This rewriting greatly reduces the possible quantifier instantiations and, thereby, the search space for the SMT solver, such that all future runs of the verifier, for instance as part of continuous integration, are substantially faster. We implemented our algorithm for the Boogie verifier and demonstrated its effectiveness on examples from Dafny and Viper. Specifically, for files with verification times over a minute, we show significant speedups of up to 100–1000 times and no slowdowns. We also provide some evidence that these improvements persist as projects evolve.
  • Distributed Basis Pursuit
    Item type: Journal Article
    Mota, Joao F.C.; Xavier, Joao M.F.; Aguiar, Pedro M.Q.; et al. (2012)
    IEEE Transactions on Signal Processing
  • Go Meta! A Case for Generative Programming and DSLs in Performance Critical Systems
    Item type: Conference Paper
    Rompf, Tiark; Brown, Kevin J.; Lee, HyoukJoong; et al. (2015)
    Leibniz International Proceedings in Informatics (LIPIcs) ~ 1st Summit on Advances in Programming Languages (SNAPL 2015)
    Most performance critical software is developed using very low-level techniques. We argue that this needs to change, and that generative programming is an effective avenue to enable the use of high-level languages and programming techniques in many such circumstances.
  • Learning Signals and Graphs from Time-Series Graph Data with Few Causes
    Item type: Conference Paper
    Misiakos, Panagiotis; Mihal, Vedran; Püschel, Markus (2024)
    ICASSP 2024 - 2024 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)
    In this paper we port assumptions and techniques from DAG (directed acyclic graph) learning and causal inference to time-series graph data. In particular, we view such data as indexed by a DAG obtained by unrolling the graph in time and generated by a causal linear structural equation model (SEM) from only few causes. For this situation we solve two problems: (1) learning the time series from samples, and (2) learning the graph from time-series data by first learning the entire DAG and then extracting the result. We empirically evaluate our approach targeting the few-causes assumption on both synthetic and real-world data and show significant improvements over prior methods.
  • Optimal circuits for streamed linear permutations using RAM
    Item type: Conference Paper
    Serre, François; Holenstein, Thomas; Püschel, Markus (2016)
    Proceedings of the 2016 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays (FPGA 2016)
  • Distributed ADMM for model predictive control and congestion control
    Item type: Conference Paper
    Mota, João; Xavier, João; Aguiar, Pedro Q.; et al. (2012)
Publications 1 - 10 of 94