-
Brijesh Dongol, Matt Griffin, Andrei Popescu and Jamie Wright
Relative Security: Formally Modeling and (Dis)Proving
Resilience Against Semantic Optimization Vulnerabilities
37th IEEE Computer Security Foundations Symposium (CSF 2024)
Accepted.
-
Andrei Popescu
Nominal Recursors as Epi-Recursors
51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024)
To appear.
-
Liron Cohen, Adham Jabarin, Andrei Popescu, Reuben N. S. Rowe
On the Complex(ity) Landscape of Checking Infinite Descent
51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024)
To appear.
-
Artur Graczyk, Marialena Hadjikosti, Andrei Popescu
A Framework for Verifying the Collision Freeness
of Collaborative Robots (Work in Progress)
In P. Herber and A. Wijs: (eds.),
18th International Conference (iFM 2023)
LNCS 14300, 391–397, Springer
-
Andrei Popescu, Dmitriy Traytel
Admissible Types-to-PERs Relativization in Higher-Order Logic
50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023)
Proc. ACM Program. Lang. 7(POPL): 1214-1245 (2023)
-
Andrei Popescu
Rensets and Renaming-Based
Recursion for Syntax with Bindings
Automated Reasoning: 11th International Joint Conference (2022)
-
Andrei Popescu, Dmitriy Traytel
Distilling the Requirements of Gödel's Incompleteness Theorems with a Proof Assistant
Journal of Automated Reasoning 65: 1027–1070 (2021)
-
Andrei Popescu, Peter Lammich, Ping Hou
CoCon: A Conference Management System with Verified Document Confidentiality
Journal of Automated Reasoning 65(2): 321-356 (2021)
-
Lorenzo Gheri, Andrei Popescu
A Formalized General Theory of Syntax With Bindings: Extended Version
Journal of Automated Reasoning 64, 641–675 (2020)
-
Andrei Popescu, Dmitriy Traytel
A Formally Verified Abstract Account of Gödel's Incompleteness Theorems
In P. Fontaine (ed.),
27th International Conference on Automated Deduction (CADE) 2019
LNCS 11716,
7442-461, Springer
-
Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel
Bindings As Bounded Natural Functors
Proc. ACM Program. Lang. 3, Principles of Programming Languages (POPL) 2019
Article No. 22, 1-22, ACM
-
Ondrej Kuncar, Andrei Popescu
From Types to Sets by Local Type Definition in Higher-Order Logic
(extended version)
Journal of Automated Reasoning 62(2): 237-260 (2019)
(Special issue dedicated to
ITP 2016)
-
Ondrej Kuncar, Andrei Popescu
A Consistent Foundation for Isabelle/HOL (extended version, including detailed proofs)
Journal of Automated Reasoning 62(4): 531-555 (2019)
(Special issue dedicated to
ITP 2015)
-
Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi
CoSMed: A Confidentiality-Verified Social Media Platform (extended version)
Journal of Automated Reasoning 61(1-4): 113-139 (2018)
(Special issue on Milestones in Interactive Thoerem Proving, dedicated to Tobias Nipkow's 60th birthday)
-
Ondřej Kunčar, Andrei Popescu
Safety and conservativity of definitions in HOL and Isabelle/HOL
Proc.
ACM Program. Lang. 2, Principles of Programming Languages (POPL) 2018,
Article No. 24, 1-24, ACM
-
Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel
Foundational nonuniform (co)datatypes for higher-order logic
In 32nd Annual ACM/IEEE Symposium on Logic in Computer
Science (LICS) 2017,
1-12, ACM / IEEE
-
Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi
CoSMeDis: A Distributed Social Media Platform
with Formally Verified Confidentiality Guarantees
In
38th IEEE Symposium
on Security and Privacy (S&P) 2017
729-748, IEEE
-
Ondřej Kunčar, Andrei Popescu
Comprehending Isabelle/HOL's consistency
In H. Yang (ed.),
26th
European Symposium on Programming (ESOP) 2017,
LNCS 10201, 724-749, Springer
Here are the slides
of my two end-to-end ESOP 2017 talks.
-
Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, and Dmitriy Traytel
Friends with benefits: Implementing corecursion in foundational proof assistants
In H. Yang (ed.),
26th
European Symposium on Programming (ESOP) 2017,
LNCS 10201, 111-140, Springer
-
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Soundness and completeness proofs by coinductive methods
Journal of Automated Reasoning 58(1): 149-179 (2017)
(Special issue dedicated to
IJCAR 2014)
-
Lorenzo Gheri, Andrei Popescu
A Formalized General Theory of Syntax With Bindings
In M. Ayala-
Rincón and C. A. Muñoz (eds.),
8th International Conference on Interactive Theorem Proving (ITP) 2017
LNCS 10499, 241-261, Springer
-
Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone
Encoding monomorphic and polymorphic types
Logical Methods in Computer Science 12(4), 2016
(Special issue dedicated to TACAS 2013)
-
Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi
CoSMed: A Confidentiality-Verified Social Media Platform
In J. C. Blanchette and S. Merz (eds.),
7th International Conference on Interactive Theorem Proving (ITP)
2016,
LNCS 9807, 87-106, Springer
-
Ondřej Kunčar, Andrei Popescu
From Types to Sets by Local Type Definitions in Higher-Order Logic
In J. C. Blanchette and S. Merz (eds.),
7th International Conference on Interactive Theorem Proving (ITP)
2016,
LNCS 9807, 200-218, Springer
-
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Foundational Extensible Corecursion: A Proof Assistant Perspective
In K. Fisher and J. H. Reppy (eds.),
20th ACM SIGPLAN International
Conference on Functional Programming (ICFP) 2015,
192-204, ACM
-
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Witnessing (Co)datatypes
In J. Vitek
(ed.),
24th European Symposium on Programming (ESOP) 2015
LNCS 9032, 359-382, Springer
-
Andrei Popescu, Grigore Roșu
Term-Generic Logic
Theoretical Computer Science 577: 1–24 (2015)
-
Ondřej Kunčar, Andrei Popescu
A Consistent Foundation for Isabelle/HOL
In C. Urban and X. Zhang
(eds.),
6th International Conference on Interactive Theorem Proving (ITP) 2015,
LNCS 9236, 234-252, Springer
-
Sudeep Kanav, Peter Lammich, Andrei Popescu
A Conference Management System with Verified Document Confidentiality
In A. Biere and R. Bloem (eds.),
26th International Conference on Computer
Aided Verification (CAV) 2014,
LNCS 8559, 167-183, Springer
-
Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel
Truly Modular (Co)datatypes for Isabelle/HOL
In G. Klein
and R. Gamboa (eds.),
5th International Conference on Interactive Theorem Proving (ITP) 2014,
LNCS 8558, 93-110, Springer
-
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Cardinals in Isabelle/HOL
In G. Klein
and R. Gamboa (eds.),
5th International Conference on Interactive Theorem Proving (ITP) 2014,
LNCS 8558, 111-127, Springer
-
Tobias Nipkow, Andrei Popescu
Making Security Type Systems Less Ad Hoc
it - Information Technology 56(6): 267-272 (2014)
-
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Unified Classical Logic Completeness: A Coinductive Pearl
In S. Demri, D. Kapur and C. Weidenbach (eds.),
7th International Joint
Conference on Automated Reasoning (IJCAR) 2014
LNCS 8562, 46-60, Springer
-
Andreas Schropp, Andrei Popescu
Nonfree Datatypes in Isabelle/HOL: Animating a Many-Sorted Metatheory
In
G. Gonthier and M. Norrish (eds.),
3rd International Conference on Certified Programs and Proofs (CPP)
2013,
LNCS 8307, 114-130, Springer
-
Andrei Popescu, Johannes Hölzl, Tobias Nipkow
Formalizing Probabilistic Noninterference
In
G. Gonthier and M. Norrish (eds.),
3rd International Conference on Certified Programs and Proofs (CPP)
2013,
LNCS 8307, 259-275, Springer
-
Andrei Popescu, Johannes Hölzl, Tobias Nipkow
Formal Verification of Language-Based Concurrent Noninterference
Journal of Formalized Reasoning 6(1), 2013
-
Jasmin Christian Blanchette, Andrei Popescu
Mechanizing the metatheory of Sledgehammer
In
P. Fontaine, C. Ringeissen and R. A. Schmidt (eds.),
9th International Symposium on Frontiers of Combining
Systems (FroCoS) 2013
LNCS 8152, 245-260, Springer
-
Andrei Popescu, Johannes Hölzl, Tobias Nipkow
Noninterfering Schedulers: When Possibilistic Noninterference Implies Probabilistic Noninterference
In In R. Heckel and S. Milius (eds.),
5th International
Conference on Algebra and Coalgebra in Computer Science (CALCO) 2013,
LNCS 8089, 236-252, Springer
-
Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone
Encoding Monomorphic and Polymorphic Types
In N. Piterman and S. A. Smolka (eds.),
19th International Conference on
Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2013
LNCS 7795, 493-507, Springer
-
Andrei Popescu, Johannes Hölzl, Tobias Nipkow
Proving Concurrent Noninterference
In C. Hawblitzel
and D. Miller (eds.),
2nd International Conference on Certified Programs and Proofs (CPP) 2012
LNCS 7795, 109-125, Springer
Receiver of the
RS3
best paper award for 2012-2013
-
Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach
More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification
In L. Beringer
and A. P. Felty (eds.),
3rd Conference on Interactive Theorem Proving (ITP) 2012
LNCS 7406, 345-360, Springer
-
Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette
Foundational, Compositional (Co)datatypes for Higher-Order Logic:
Category Theory Applied to Theorem Proving
LICS 2012
596-605, IEEE
-
Andrei Popescu, Elsa L. Gunter
Recursion principles for syntax with bindings and substitution
In M. M. T. Chakravarty,
Z. Hu and
O. Danvy (eds.),
16th ACM SIGPLAN International Conference on
Functional Programming (ICFP) 2011
346-358, ACM
-
Andrei Popescu, Elsa L. Gunter, Christopher J. Osborn
Strong Normalization for System F by HOAS on Top of FOAS
LICS 2010
31-40, IEEE
-
Andrei Popescu, Elsa L. Gunter
Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization
In C.-H. L. Ong (ed.),
13th International Conference on Foundations of Software and
Computational Structures (FoSSaCS) 2010
LNCS 6014, 109-127, Springer
-
Andrei Popescu, Traian Florin Șerbănuță, Grigore Roșu
A semantic approach to interpolation
Theoretical Computer Science 410(12-13): 1109-1128 (2009)
-
Andrei Popescu
Weak Bisimilarity Coalgebraically
In A. Kurz, M. Lenisa and A. Tarlecki (eds.),
3rd
International Conference on Algebra and Coalgebra in Computer Science (CALCO) 2009
LNCS 5728, 157-172, Springer
-
Elsa L. Gunter, Christopher J. Osborn, Andrei Popescu
Theory support for weak higher order abstract syntax in Isabelle/HOL
In J. Cheney and A. P. Felty (eds.),
4th International Workshop on Logical Frameworks and Meta-
Languages: Theory and Practice, 2009
12-20, ACM
-
Andrei Popescu, Grigore Roșu
Term-Generic Logic.
In A. Corradini and U. Montanari (eds.),
19th
International Workshop on Algebraic Development Techniques (WADT) 2008
LNCS 5486, 290-307, Springer
-
Daniel Găină, Andrei Popescu
An Institution-Independent Proof of the Robinson Consistency Theorem
Studia Logica 85(1): 41-73 (2007)
-
Daniel Găină, Andrei Popescu
An Institution-independent Generalization of Tarski's Elementary Chain Theorem
Journal of Logic and Computation 16(6): 713-735 (2006)
-
Andrei Popescu, Traian Florin Șerbănuță, Grigore Roșu
A Semantic Approach to Interpolation
In L. Aceto
and A. Ingólfsdóttir (eds.),
9th International Conference on Foundations of Software Science and Computation
Structure (FoSSaCS) 2006
LNCS 3921, 307-321, Springer
-
Andrei Popescu, Grigore Roșu
Behavioral Extensions of Institutions
In J. L. Fiadeiro, N. Harman,
M. Roggenbach and J. J. M. M. Rutten (eds.),
1st International Conference on Algebra and Coalgebra in
Computer Science (CALCO) 2005
LNCS 3629, 331-347, Springer
-
Andrei Popescu
Languages Generated Using an Abstract Catenation
Grammars 7: 31-40 (2004)