| 2026 | ESOP | Rely-Guarantee Is Coinductive - - A Proof-Centered Investigation of Inductively Approximated Coinduction -. | John Derrick, Chelsea Edmonds, Andrei Popescu, Jamie Wright |
| 2026 | ITP | Certified Infinite Descent Criteria in Isabelle/HOL. | Jamie Wright, Liron Cohen, Reuben N. S. Rowe, Andrei Popescu |
| 2025 | ITP | Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL. | Jan van Brgge, Andrei Popescu, Dmitriy Traytel |
| 2025 | JELIA | Completing Structured Arguments in Assumption-Based Argumentation. | Andrei Popescu, Johannes P. Wallner |
| 2025 | LICS | Completing Gordon's Higher-Order Logic. | Andrei Popescu |
| 2025 | SAC | Dynamic Programming Algorithms for Probabilistic Bipolar Argumentation Frameworks. | Andrei Popescu, Johannes P. Wallner |
| 2024 | IFM | Isomorphic Transfer Infrastructure for Nested Types in Isabelle/HOL (Work in Progress). | Gergely Buday, Andrei Popescu |
| 2024 | KR | Advancing Algorithmic Approaches to Probabilistic Argumentation under the Constellation Approach. | Andrei Popescu, Johannes P. Wallner |
| 2023 | IFM | A Framework for Verifying the Collision Freeness of Collaborative Robots (Work in Progress). | Artur Graczyk, Marialena Hadjikosti, Andrei Popescu |
| 2023 | JELIA | Reasoning in Assumption-Based Argumentation Using Tree-Decompositions. | Andrei Popescu, Johannes P. Wallner |
| 2022 | CADE | Rensets and Renaming-Based Recursion for Syntax with Bindings. | Andrei Popescu |
| 2021 | ITP | Bounded-Deducibility Security (Invited Paper). | Andrei Popescu, Thomas Bauereiss, Peter Lammich |
| 2021 | RecSys | Do Users Appreciate Explanations of Recommendations? An Analysis in the Movie Domain. | Thi Ngoc Trang Tran, Viet Man Le, Muesluem Atas, Alexander Felfernig, Martin Stettinger, Andrei Popescu |
| 2021 | SPLC | Evaluating recommender systems in feature model configuration. | Mathias Uta, Alexander Felfernig, Viet Man Le, Andrei Popescu, Thi Ngoc Trang Tran, Denis Helic |
| 2019 | CADE | A Formally Verified Abstract Account of Gdel's Incompleteness Theorems. | Andrei Popescu, Dmitriy Traytel |
| 2017 | ESOP | Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. | Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel |
| 2017 | ESOP | Comprehending Isabelle/HOL's Consistency. | Ondrej Kuncar, Andrei Popescu |
| 2017 | ITP | A Formalized General Theory of Syntax with Bindings. | Lorenzo Gheri, Andrei Popescu |
| 2017 | LICS | Foundational nonuniform (Co)datatypes for higher-order logic. | Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel |
| 2017 | SP | CoSMeDis: A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees. | Thomas Bauerei, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi |
| 2016 | ITP | CoSMed: A Confidentiality-Verified Social Media Platform. | Thomas Bauerei, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi |
| 2016 | ITP | From Types to Sets by Local Type Definitions in Higher-Order Logic. | Ondrej Kuncar, Andrei Popescu |
| 2015 | ESOP | Witnessing (Co)datatypes. | Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel |
| 2015 | ICFP | Foundational extensible corecursion: a proof assistant perspective. | Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel |
| 2015 | ITP | A Consistent Foundation for Isabelle/HOL. | Ondrej Kuncar, Andrei Popescu |
| 2014 | CADE | Unified Classical Logic Completeness - A Coinductive Pearl. | Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel |
| 2014 | CAV | A Conference Management System with Verified Document Confidentiality. | Sudeep Kanav, Peter Lammich, Andrei Popescu |
| 2014 | ITP | Cardinals in Isabelle/HOL. | Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel |
| 2014 | ITP | Truly Modular (Co)datatypes for Isabelle/HOL. | Jasmin Christian Blanchette, Johannes Hlzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel |
| 2013 | CALCO | Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference. | Andrei Popescu, Johannes Hlzl, Tobias Nipkow |
| 2013 | CPP | Formalizing Probabilistic Noninterference. | Andrei Popescu, Johannes Hlzl, Tobias Nipkow |
| 2013 | CPP | Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory. | Andreas Schropp, Andrei Popescu |
| 2013 | TACAS | Encoding Monomorphic and Polymorphic Types. | Jasmin Christian Blanchette, Sascha Bhme, Andrei Popescu, Nicholas Smallbone |
| 2012 | CPP | Proving Concurrent Noninterference. | Andrei Popescu, Johannes Hlzl, Tobias Nipkow |
| 2012 | ITP | More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. | Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach |
| 2012 | LICS | Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving. | Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette |
| 2011 | ICFP | Recursion principles for syntax with bindings and substitution. | Andrei Popescu, Elsa L. Gunter |
| 2010 | FOSSACS | Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization. | Andrei Popescu, Elsa L. Gunter |
| 2010 | LICS | Strong Normalization for System F by HOAS on Top of FOAS. | Andrei Popescu, Elsa L. Gunter, Christopher J. Osborn |
| 2009 | CALCO | Weak Bisimilarity Coalgebraically. | Andrei Popescu |
| 2006 | CHI | Minimap: a web page visualization method for mobile phones. | Virpi Roto, Andrei Popescu, Antti Koivisto, Elina Vartiainen |
| 2006 | FOSSACS | A Semantic Approach to Interpolation. | Andrei Popescu, Traian Serbanuta, Grigore Rosu |
| 2005 | CALCO | Behavioral Extensions of Institutions. | Andrei Popescu, Grigore Rosu |
| 1995 | ICASSP | CELP coding using trellis-coded vector quantization of the excitation. | Andrei Popescu, Nicolas Moreau, Claude Lamblin |
| 1995 | Interspeech | Subband analysis-by-synthesis coding. | Andrei Popescu, Nicolas Moreau |
| 1995 | Interspeech | A differential encoding method for the LTP delay in CELP coders. | Andrei Popescu, Nicolas Moreau, Claude Lamblin |