397 citations · 492 across the 15 of their papers we have counts for
18 papers
Practical Formal Verification for MLIR Programs
Emily Tucker, Louis-Noël Pouchet, Erika Hunhoff +2
Optimizing compilers have become a cornerstone for high-performance program generation in research and industry. Optimizations, including those implemented manually by a user and t…
Holistic Optimization Framework for FPGA Accelerators
Stéphane Pouget, Michael Lo, Louis-Noël Pouchet +1
Customized accelerators have revolutionized modern computing by delivering substantial gains in energy efficiency and performance through hardware specialization. Field-Programmabl…
Automatic Hardware Pragma Insertion in High-Level Synthesis: A Non-Linear Programming Approach
Stéphane Pouget, Louis-Noël Pouchet, Jason Cong
High-Level Synthesis enables the rapid prototyping of hardware accelerators, by combining a high-level description of the functional behavior of a kernel with a set of micro-archit…
A Unified Framework for Automated Code Transformation and Pragma Insertion
Stéphane Pouget, Louis-Noël Pouchet, Jason Cong
High-level synthesis, source-to-source compilers, and various Design Space Exploration techniques for pragma insertion have significantly improved the Quality of Results of generat…
Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules
Steve Kommrusch, Martin Monperrus, Louis-Noël Pouchet
We target the problem of automatically synthesizing proofs of semantic equivalence between two programs made of sequences of statements. We represent programs using abstract syntax…
Proving Equivalence Between Complex Expressions Using Graph-to-Sequence Neural Models
Steve Kommrusch, Théo Barollet, Louis-Noël Pouchet
We target the problem of provably computing the equivalence between two complex expression trees. To this end, we formalize the problem of equivalence between two such programs as…