Simulation-Based Iteration of Tree Transducers. - Parosh Aziz Abdulla; Axel Legay; Julien d'Orso; Ahmed Rezine (TACAS, 2005)

Proving Liveness by Backwards Reachability. - Parosh Aziz Abdulla; Bengt Jonsson 001; Ahmed Rezine; Mayank Saksena (CONCUR, 2006)

Tree regular model checking: A simulation-based approach. - Parosh Aziz Abdulla; Axel Legay; Julien d'Orso; Ahmed Rezine (J. Log. Algebraic Methods Program., 2006)

Parameterized Verification of Infinite-State Processes with Global Conditions. - Parosh Aziz Abdulla; Giorgio Delzanno; Ahmed Rezine (CAV, 2007)

Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems). - Parosh Aziz Abdulla; Giorgio Delzanno; Noomene Ben Henda; Ahmed Rezine (TACAS, 2007)

Monotonic Abstraction for Programs with Dynamic Memory Heaps. - Parosh Aziz Abdulla; Ahmed Bouajjani; Jonathan Cederberg; Frédéric Haziza; Ahmed Rezine (CAV, 2008)

Shape Analysis via Monotonic Abstraction. - Parosh Aziz Abdulla; Ahmed Bouajjani; Jonathan Cederberg; Frédéric Haziza; Ran Ji; Ahmed Rezine (Beyond the Finite: New Challenges in Verification and Semistructured Data, 2008)

Parameterized Tree Systems. - Parosh Aziz Abdulla; Noomene Ben Henda; Giorgio Delzanno; Frédéric Haziza; Ahmed Rezine (FORTE, 2008)

Monotonic Abstraction in Action. - Parosh Aziz Abdulla; Giorgio Delzanno; Ahmed Rezine (ICTAC, 2008)

Handling Parameterized Systems with Non-atomic Global Conditions. - Parosh Aziz Abdulla; Noomene Ben Henda; Giorgio Delzanno; Ahmed Rezine (VMCAI, 2008)

Monotonic Abstraction in Parameterized Verification. - Parosh Aziz Abdulla; Giorgio Delzanno; Ahmed Rezine (RP, 2008)

Parameterized Systems: Generalizing and Simplifying Automatic Verification. - Ahmed Rezine (2008)

Approximated Context-Sensitive Analysis for Parameterized Verification. - Parosh Aziz Abdulla; Giorgio Delzanno; Ahmed Rezine (FMOODS/FORTE, 2009)

Automatic Verification of Directory-Based Consistency Protocols. - Parosh Aziz Abdulla; Giorgio Delzanno; Ahmed Rezine (RP, 2009)

Approximated parameterized verification of infinite-state processes with global conditions. - Parosh Aziz Abdulla; Giorgio Delzanno; Ahmed Rezine (Formal Methods Syst. Des., 2009)

Monotonic Abstraction: on Efficient Verification of Parameterized Systems. - Parosh Aziz Abdulla; Giorgio Delzanno; Noomene Ben Henda; Ahmed Rezine (Int. J. Found. Comput. Sci., 2009)

Invariant Synthesis for Programs Manipulating Lists with Unbounded Data. - Ahmed Bouajjani; Cezara Dragoi; Constantin Enea; Ahmed Rezine; Mihaela Sighireanu (CAV, 2010)

Constrained Monotonic Abstraction: A CEGAR for Parameterized Verification. - Parosh Aziz Abdulla; Yu-Fang Chen 001; Giorgio Delzanno; Frédéric Haziza; Chih-Duo Hong; Ahmed Rezine (CONCUR, 2010)

Automatic Verification of Directory-Based Consistency Protocols with Graph Constraints. - Parosh Aziz Abdulla; Giorgio Delzanno; Ahmed Rezine (Int. J. Found. Comput. Sci., 2011)

Automatic Test Program Generation for Out-of-Order Superscalar Processors. - Ying Zhang 040; Ahmed Rezine; Petru Eles; Zebo Peng (Asian Test Symposium, 2012)

Detecting Key Players in Terrorist Networks. - Ala Berzinji; Lisa Kaati; Ahmed Rezine (EISIC, 2012)

Automatic Fence Insertion in Integer Programs via Predicate Abstraction. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Carl Leonardsson; Ahmed Rezine (SAS, 2012)

Counter-Example Guided Fence Insertion under TSO. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Carl Leonardsson; Ahmed Rezine (TACAS, 2012)

Ordered Counter-Abstraction - Ahmed Rezine (CoRR, 2012)

A lightweight regular model checking approach for parameterized systems. - Giorgio Delzanno; Ahmed Rezine (Int. J. Softw. Tools Technol. Transf., 2012)

Verifying safety and liveness for the FlexTM hybrid transactional memory. - Parosh Aziz Abdulla; Sandhya Dwarkadas; Ahmed Rezine; Arrvindh Shriraman; Yunyun Zhu (DATE, 2013)

Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Carl Leonardsson; Ahmed Rezine (TACAS, 2013)

String Constraints for Verification. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Lukás Holík; Ahmed Rezine; Philipp Rümmer; Jari Stenman (CAV, 2014)

Ordered Counter-Abstraction - Refinable Subword Relations for Parameterized Verification. - Pierre Ganty; Ahmed Rezine (LATA, 2014)

Norn: An SMT Solver for String Constraints. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Lukás Holík; Ahmed Rezine; Philipp Rümmer; Jari Stenman (CAV (1), 2015)

Verification of Cache Coherence Protocols wrt. Trace Filters. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Zeinab Ganjei; Ahmed Rezine; Yunyun Zhu (FMCAD, 2015)

Abstracting and Counting Synchronizing Processes. - Zeinab Ganjei; Ahmed Rezine; Petru Eles; Zebo Peng (VMCAI, 2015)

Lazy Constrained Monotonic Abstraction. - Zeinab Ganjei; Ahmed Rezine; Petru Eles; Zebo Peng (VMCAI, 2016)

Quantifying the Information Leak in Cache Attacks through Symbolic Execution. - Sudipta Chattopadhyay 001; Moritz Beck 002; Ahmed Rezine; Andreas Zeller (CoRR, 2016)

Counting dynamically synchronizing processes. - Zeinab Ganjei; Ahmed Rezine; Petru Eles; Zebo Peng (Int. J. Softw. Tools Technol. Transf., 2016)

Safety verification of phaser programs. - Zeinab Ganjei; Ahmed Rezine; Petru Eles; Zebo Peng (FMCAD, 2017)

Quantifying the information leak in cache attacks via symbolic execution. - Sudipta Chattopadhyay 001; Moritz Beck 002; Ahmed Rezine; Andreas Zeller (MEMOCODE, 2017)

Flatten and conquer: a framework for efficient analysis of string constraints. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Bui Phi Diep; Lukás Holík; Ahmed Rezine; Philipp Rümmer (PLDI, 2017)

An integrated specification and verification technique for highly concurrent data structures. - Parosh Aziz Abdulla; Frédéric Haziza; Lukás Holík; Bengt Jonsson 001; Ahmed Rezine (Int. J. Softw. Tools Technol. Transf., 2017)

Stability-aware integrated routing and scheduling for control applications in Ethernet networks. - Rouhollah Mahfouzi; Amir Aminifar; Soheil Samii; Ahmed Rezine; Petru Eles; Zebo Peng (DATE, 2018)

Trau: SMT solver for string constraints. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Bui Phi Diep; Lukás Holík; Ahmed Rezine; Philipp Rümmer (FMCAD, 2018)

On Reachability in Parameterized Phaser Programs. - Zeinab Ganjei; Ahmed Rezine; Ludovic Henrio; Petru Eles; Zebo Peng (TACAS (1), 2019)

Quantifying the Information Leakage in Cache Attacks via Symbolic Execution. - Sudipta Chattopadhyay 001; Moritz Beck 002; Ahmed Rezine; Andreas Zeller (ACM Trans. Embed. Comput. Syst., 2019)

Verifying Safety of Parameterized Heard-Of Algorithms. - Zeinab Ganjei; Ahmed Rezine; Petru Eles; Zebo Peng (NETYS, 2020)

Software-Based Self-Testing Using Bounded Model Checking for Out-of-Order Superscalar Processors. - Ying Zhang 040; Krishnendu Chakrabarty; Zebo Peng; Ahmed Rezine; Huawei Li 001; Petru Eles; Jianhui Jiang (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020)

Breaking Silos to Guarantee Control Stability with Communication over Ethernet TSN. - Rouhollah Mahfouzi; Amir Aminifar; Soheil Samii; Ahmed Rezine; Petru Eles; Zebo Peng (IEEE Des. Test, 2021)

Correction to: An integrated specification and verification technique for highly concurrent data structures. - Parosh Aziz Abdulla; Frédéric Haziza; Lukás Holík; Bengt Jonsson 001; Ahmed Rezine (Int. J. Softw. Tools Technol. Transf., 2021)

Symbolic identification of shared memory based bank conflicts for GPUs. - Adrian Horga; Ahmed Rezine; Sudipta Chattopadhyay 001; Petru Eles; Zebo Peng (J. Syst. Archit., 2022)

SafeDeep: A Scalable Robustness Verification Framework for Deep Neural Networks. - Anahita Baninajjar; Kamran Hosseini; Ahmed Rezine; Amir Aminifar (ICASSP, 2023)

Verification-Friendly Deep Neural Networks. - Anahita Baninajjar; Ahmed Rezine; Amir Aminifar (CoRR, 2023)

VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees. - Anahita Baninajjar; Ahmed Rezine; Amir Aminifar (ICML, 2024)

Verified Relative Safety Margins for Neural Network Twins. - Anahita Baninajjar; Kamran Hosseini; Ahmed Rezine; Amir Aminifar (CoRR, 2024)

On Modeling and Detecting Trojans in Instruction Sets. - Ying Zhang 040; Aodi He; Jiaying Li; Ahmed Rezine; Zebo Peng; Erik Larsson; Tao Yang; Jianhui Jiang; Huawei Li 001 (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2024)