| 2014 | Refinement-based synthesis of correct contract model decompositions. | Thi Thieu Hoa Le, Roberto Passerone |
| 2014 | A framework for high-assurance quasi-synchronous systems. | Robin Larrieu, Natarajan Shankar |
| 2014 | Tutorial I: Efficient symbolic execution for software testing. | Johannes Kinder |
| 2014 | A new synthesis procedure for atomic rules containing multi-cycle function blocks. | Michal Karczmarek, Arvind, Muralidaran Vijayaraghavan |
| 2014 | Probabilistic model checking based DAL analysis to optimize a combined TMR-blind-scrubbing mitigation technique for FPGA-based aerospace applications. | Khaza Anuarul Hoque, Otmane At Mohamed, Yvon Savaria, Claude Thibeault |
| 2014 | Unified dataflow model for the analysis of data and pipeline parallelism, and buffer sizing. | Joost P. H. M. Hausmans, Stefan J. Geuns, Maarten Wiggers, Marco Jan Gerrit Bekooij |
| 2014 | From visual to logical formalisms for SoC validation. | Ranan Fraer, Doron Keren, Zurab Khasidashvili, Alexander Novakovsky, Avi Puder, Eli Singerman, Eran Talmor, Moshe Y. Vardi, Jin Yang |
| 2014 | Performance analysis of the Disrupted Static Priority scheduling for AFDX. | Rubn Trillo Flores, Marc Boyer |
| 2014 | A fast emulator for ARM-based embedded systems. | Nariman Eskandari, Hatef Madani, Armin Ahmadzadeh, Mohsen Mahmoudi Aznaveh, Saeid Gorgin |
| 2014 | MEMOCODE 2014 software design contest: Space Invaders emulator. | Stephen A. Edwards, Hiren D. Patel |
| 2014 | Assertion-based flow monitoring of SystemC models. | Sonali Dutta, Moshe Y. Vardi |
| 2014 | A multi-core version of FreeRTOS verified for datarace and deadlock freedom. | Prakash Chandrasekaran, Kavum Muriyil Balachandran Shibu Kumar, Remish L. Minz, Deepak D'Souza, Lomesh Meshram |
| 2014 | Keynote talk I: Security and privacy in implantable medical devices: An ongoing concern. | Wayne P. Burleson |
| 2014 | TESL: A language for reconciling heterogeneous execution traces. | Frdric Boulanger, Christophe Jacquet, Ccile Hardebolle, Iuliana Prodan |
| 2014 | An abstraction-refinement framework for priority-driven scheduling of static dataflow graphs. | Adnan Bouakaz, Thierry Gautier |
| 2014 | From clock-driven to data-driven models. | Yu Bai, Klaus Schneider, Nikita Bhardwaj, Badarinath Katti, Tania Shazadi |
| 2014 | Cost-efficient implementation of k-NN algorithm on multi-core processors. | Armin Ahmadzadeh, Reza Mirzaei, Hatef Madani, Mohammad Shobeiri, Mahsa Sadeghi, Mohsen Gavahi, Kianoush Jafari, Mohsen Mahmoudi Aznaveh, Saeid Gorgin |
| 2014 | Formal property verification in a conformance testing framework. | Houssam Abbas, Hans D. Mittelmann, Georgios Fainekos |
| 2013 | Equivalence checking for synchronous elastic circuits. | Vidura Wijaysekara, Sudarshan K. Srinivasan |
| 2013 | An equivalence checker for hardware-dependent embedded system software. | Carlos Villarraga, Bernard Schmidt, Jrg Bormann, Christian Bartsch, Dominik Stoffel, Wolfgang Kunz |
| 2013 | Modular compilation of guarded atomic actions. | Muralidaran Vijayaraghavan, Nirav Dave, Arvind |
| 2013 | Symbolic software model validation. | Cynthia Sturton, Rohit Sinha, Thurston H. Y. Dang, Sakshi Jain, Michael McCoyd, Wei Yang Tan, Petros Maniatis, Sanjit A. Seshia, David A. Wagner |
| 2013 | Automated extraction of scenario sequences from disciplined dataflow networks. | Firew Siyoum, Marc Geilen, Johan Eker, Carl von Platen, Henk Corporaal |
| 2013 | Ranking structure in communication fabrics. | Sayak Ray, Robert K. Brayton |
| 2013 | Keynote talk I: Building a high-assurance unpiloted air vehicle. | Lee Pike |