| 2010 | Compilation of imperative synchronous programs with refined clocks. | Mike Gemunde, Jens Brandt, Klaus Schneider |
| 2010 | A design flow based on modular refinement. | Nirav Dave, Man Cheuk Ng, Michael Pellauer, Arvind |
| 2010 | Understanding loops: The influence of the decomposition of Karp, Miller, and Winograd. | Alain Darte |
| 2010 | Elastic systems. | Jordi Cortadella, Marc Galceran Oms, Michael Kishinevsky |
| 2010 | Modular verification of synchronization with reentrant locks. | Tevfik Bultan, Fang Yu, Aysu Betin-Can |
| 2010 | A flexible schema for generating explanations in lazy theory propagation. | Roberto Bruttomesso, Edgar Pek, Natasha Sharygina |
| 2010 | ATLAS: Automatic Term-level abstraction of RTL designs. | Bryan A. Brady, Randal E. Bryant, Sanjit A. Seshia, John W. O'Leary |
| 2010 | Feldspar: A domain specific language for digital signal processing algorithms. | Emil Axelsson, Koen Claessen, Gergely Dvai, Zoltn Horvth, Karin Keijzer, Bo Lyckegrd, Anders Persson, Mary Sheeran, Josef Svenningsson, Andrs Vajda |
| 2010 | Predictable multithreading of embedded applications using PRET-C. | Sidharta Andalam, Partha S. Roop, Alain Girault |
| 2009 | Refining schizophrenia via graph reachability in Esterel. | Jeong-Han Yun, Chul-Joo Kim, Sunae Seo, Taisook Han, Kwang-Moo Choe |
| 2009 | A cross-layer approach to heterogeneity and reliability. | Daniel W. Williams, Aprotim Sanyal, Dan Upton, Jason Mars, Sudeep Ghosh, Kim M. Hazelwood |
| 2009 | Bounded Dataflow Networks and Latency-Insensitive circuits. | Muralidaran Vijayaraghavan, Arvind |
| 2009 | Buffer sharing in CSP-like programs. | Nalini Vasudevan, Stephen A. Edwards |
| 2009 | High-level optimization of integer multipliers over a finite bit-width with verification capabilities. | Omid Sarbishei, Mahmoud Tabandeh, Bijan Alizadeh, Masahiro Fujita |
| 2009 | A design case study: CPU vs. GPGPU vs. FPGA. | Daniel L. Rosenband, Till Rosenband |
| 2009 | Survival strategies for synthesized hardware systems. | Martin C. Rinard |
| 2009 | An introduction to implementation attacks and countermeasures. | Thomas Popp |
| 2009 | Synthesis of programs from temporal property specifications. | Amir Pnueli, Uri Klein |
| 2009 | Multicore power management: Ensuring robustness via early-stage formal verification. | Anita Lungu, Pradip Bose, Daniel J. Sorin, Steven German, Geert Janssen |
| 2009 | Can we computerize an elephant? | David Harel |
| 2009 | The role of mutation analysis for property qualification. | Luigi Di Guglielmo, Franco Fummi, Graziano Pravadelli |
| 2009 | Verification of an industrial SystemC/TLM model using LOTOS and CADP. | Hubert Garavel, Claude Helmstetter, Olivier Ponsini, Wendelin Serwe |
| 2009 | Bang for the buck: Improvising and scheduling verification engines for effective resource utilization. | Malay K. Ganai, Weihong Li |
| 2009 | Performance estimation for task graphs combining sequential path profiling and control dependence regions. | Fabrizio Ferrandi, Marco Lattuada, Christian Pilato, Antonino Tumeo |
| 2009 | Implementing a high-performance multithreaded microprocessor: A case study in high-level design and validation. | Eric S. Chung, James C. Hoe |