Path Directed Symbolic Execution in the K Framework. - Irina Mariuca Asavoae; Mihail Asavoae; Dorel Lucanu (SYNASC, 2010)

Collecting Semantics under Predicate Abstraction in the K Framework. - Irina Mariuca Asavoae; Mihail Asavoae (WRLA, 2010)

On Abstractions for Timing Analysis in the $ mathbb{K}$ Framework. - Mihail Asavoae; Irina Mariuca Asavoae; Dorel Lucanu (FOPARA, 2011)

Using the Executable Semantics for CFG Extraction and Unfolding. - Mihail Asavoae; Irina Mariuca Asavoae (SYNASC, 2011)

K Semantics for Assembly Languages: A Case Study. - Mihail Asavoae (K, 2011)

A Generic Program Slicing Technique Based on Language Definitions. - Adrián Riesco 001; Irina Mariuca Asavoae; Mihail Asavoae (WADT, 2012)

On the Modular Integration of Abstract Semantics for WCET Analysis. - Mihail Asavoae; Irina Mariuca Asavoae (FOPARA, 2013)

Program Semantics in Model-Based WCET Analysis: A State of the Art Perspective. - Mihail Asavoae; Claire Maiza; Pascal Raymond (WCET, 2013)

Towards a Formal Semantics-Based Technique for Interprocedural Slicing. - Irina Mariuca Asavoae; Mihail Asavoae; Adrián Riesco 001 (IFM, 2014)

How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics. - Julien Henry; Mihail Asavoae; David Monniaux; Claire Maiza (LCTES, 2014)

Memory Policy Analysis for Semantics Specifications in Maude. - Adrián Riesco 001; Irina Mariuca Asavoae; Mihail Asavoae (LOPSTR, 2015)

Timing analysis enhancement for synchronous program. - Pascal Raymond; Claire Maiza; Catherine Parent-Vigouroux; Fabienne Carrier; Mihail Asavoae (Real Time Syst., 2015)

Slicing from Formal Semantics: Chisel. - Adrián Riesco 001; Irina Mariuca Asavoae; Mihail Asavoae (FASE, 2017)

Reproducibility and representativity: mandatory properties for the compositionality of measurement-based WCET estimation approaches. - Cristian Maxim; Adriana Gogonel; Irina Mariuca Asavoae; Mihail Asavoae; Liliana Cucu-Grosjean (SIGBED Rev., 2017)

Context-Updates Analysis and Refinement in Chisel. - Irina Mariuca Asavoae; Mihail Asavoae; Adrián Riesco 001 (SPIN, 2018)

Formal Executable Models for Automatic Detection of Timing Anomalies. - Mihail Asavoae; Belgacem Ben Hedia; Mathieu Jan (WCET, 2018)

Slicing from formal semantics: Chisel - a tool for generic program slicing. - Irina Mariuca Asavoae; Mihail Asavoae; Adrián Riesco 001 (Int. J. Softw. Tools Technol. Transf., 2018)

Towards Formal Co-validation of Hardware and Software Timing Models of CPSs. - Mihail Asavoae; Imane Haur; Mathieu Jan; Belgacem Ben Hedia; Martin Schoeberl (CyPhy/WESE, 2019)

Improving WCET Evaluation using Linear Relation Analysis. - Pascal Raymond; Claire Maiza; Catherine Parent-Vigouroux; Erwan Jahier; Nicolas Halbwachs; Fabienne Carrier; Mihail Asavoae; Rémy Boutonnet (Leibniz Trans. Embed. Syst., 2019)

Formal Semantics of Predictable Pipelines: a Comparative Study. - Mathieu Jan; Mihail Asavoae; Martin Schoeberl; Edward A. Lee (ASP-DAC, 2020)

Scalable Detection of Amplification Timing Anomalies for the Superscalar TriCore Architecture. - Benjamin Binder 001; Mihail Asavoae; Florian Brandner; Belgacem Ben Hedia; Mathieu Jan (FMICS, 2020)

Is This Still Normal? Putting Definitions of Timing Anomalies to the Test. - Benjamin Binder 001; Mihail Asavoae; Belgacem Ben Hedia; Florian Brandner; Mathieu Jan (RTCSA, 2021)

Exploration of Fault Effects on Formal RISC-V Microarchitecture Models. - Simon Tollec; Mihail Asavoae; Damien Couroussé; Karine Heydemann; Mathieu Jan (FDTC, 2022)

A memory interference analysis using a formal timing analyzer (WIP). - Mihail Asavoae; Oumaima Matoussi; Asmae Bouachtala; Hai-Dang Vu; Mathieu Jan (LCTES, 2022)

Deriving Pipeline Models for Timing Analysis from High-Level HDL Processor Designs. - Samira Ait Bensaid; Mihail Asavoae; Farhat Thabet; Mathieu Jan (MEMOCODE, 2022)

Work in Progress: Automatic Construction of Pipeline Datapaths from High-Level HDL Code. - Samira Ait Bensaid; Mihail Asavoae; Farhat Thabet; Mathieu Jan (RTAS, 2022)

The Role of Causality in a Formal Definition of Timing Anomalies. - Benjamin Binder 001; Mihail Asavoae; Florian Brandner; Belgacem Ben Hedia; Mathieu Jan (RTCSA, 2022)

A Coq Framework for More Trustworthy DRAM Controllers. - Felipe Lisboa Malaquias; Mihail Asavoae; Florian Brandner (RTNS, 2022)

Formal modeling and verification for amplification timing anomalies in the superscalar TriCore architecture. - Benjamin Binder 001; Mihail Asavoae; Florian Brandner; Belgacem Ben Hedia; Mathieu Jan (Int. J. Softw. Tools Technol. Transf., 2022)

μARCHIFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections. - Simon Tollec; Mihail Asavoae; Damien Couroussé; Karine Heydemann; Mathieu Jan (FMCAD, 2023)

From the Standards to Silicon: Formally Proved Memory Controllers. - Felipe Lisboa Malaquias; Mihail Asavoae; Florian Brandner (NFM, 2023)

A formal framework to design and prove trustworthy memory controllers. - Felipe Lisboa Malaquias; Mihail Asavoae; Florian Brandner (Real Time Syst., 2023)

Leveraging Reusable Code and Proofs to Design Complex DRAM Controllers - A Case Study. - Felipe Lisboa Malaquias; Mihail Asavoae; Florian Brandner (DSD, 2024)

Fault-Resistant Partitioning of Secure CPUs for System Co-Verification against Faults. - Simon Tollec; Vedad Hadzic; Pascal Nasahl; Mihail Asavoae; Roderick Bloem; Damien Couroussé; Karine Heydemann; Mathieu Jan; Stefan Mangard (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2024)

Revisiting Timing Anomalies in Predictable In-Order Pipelines. - Lilia Rouizi; Mihail Asavoae; Benjamin Binder 001; Lionel Rieg; Florian Brandner (ECRTS, 2025)