Timos Antonopoulos
Research Scientist and Lecturer, Department of Computer Science, Yale University
Member of the Rigorous Software Engineering (ROSE) group led by Ruzica Piskac
Logic, Verification, Formal Languages and Security
Publications
- soid: A Tool for Legal Accountability for Automated Decision Making
Samuel Judson, Matthew Elacqua, Filip Cano, Timos Antonopoulos, Bettina Könighofer, Scott J. Shapiro, Ruzica Piskac
CAV 2024
PDF - ZKSMT: A VM for Proving SMT Theorems in Zero Knowledge
Daniel Luick, John C. Kolesar, Timos Antonopoulos, William R. Harris, James Parker, Ruzica Piskac, Eran Tromer, Xiao Wang, Ning Luo
USENIX Security 2024
PDF - 'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions
Samuel Judson, Matthew Elacqua, Filip Cano, Timos Antonopoulos, Bettina Könighofer, Scott J. Shapiro, Ruzica Piskac
CSLAW 2024
PDF - Analyzing Intentional Behavior in Autonomous Agents Under Uncertainty
Filip Cano Córdoba, Samuel Judson, Timos Antonopoulos, Katrine Bjørner, Nicholas Shoemaker, Scott J. Shapiro, Ruzica Piskac, Bettina Könighofer
IJCAI 2023
PDF - Ou: Automating the Parallelization of Zero-Knowledge Protocols
Yuyang Sang, Ning Luo, Samuel Judson, Ben Chaimberg, Timos Antonopoulos, Xiao Wang, Ruzica Piskac, Zhong Shao
CCS 2023
PDF - An Algebra of Alignment for Relational Verification
Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, Minh Ngo
POPL 2023
PDF - Proving UNSAT in Zero Knowledge
Ning Luo, Timos Antonopoulos, William R. Harris, Ruzica Piskac, Eran Tromer, Xiao Wang
CCS 2022
PDF - Representing Regular Languages of Infinite Words Using Mod 2 Multiplicity Automata
Dana Angluin, Timos Antonopoulos, Dana Fisman, Nevin George
FoSSaCS 2022
PDF - ppSAT: Towards Two-Party Private SAT Solving
Ning Luo, Samuel Judson, Timos Antonopoulos, Ruzica Piskac, Xiao Wang
USENIX Security 2022
PDF - Looking for the Maximum Independent Set: A New Perspective on the Stable Path Problem
Yichao Cheng, Ning Luo, Jingxuan Zhang, Timos Antonopoulos, Ruzica Piskac, Qiao Xiang
INFOCOM 2021
PDF - Bucketing and Information Flow Analysis for Provable Timing Attack Mitigation
Tachio Terauchi, Timos Antonopoulos
JCS 28(6), 607--634 (2020)
PDF -
DynamiTe: Dynamic Termination and Non-termination Proofs
Ton Chanh Le, Timos Antonopoulos, Parisa Fathololumi, Eric Koskinen, ThanhVu Nguyen
OOPSLA 2020
PDF -
Using Dynamically Inferred Invariants to Analyze Program Runtime Complexity
ThanhVu Nguyen, Didier Ishimwe, Alexey Malyshev, Timos Antonopoulos, Quoc-Sang Phan
SEAD 2020
PDF -
Privacy Preserving CTL Model Checking through Oblivious Graph Algorithms
Samuel Judson, Ning Luo, Timos Antonopoulos, Ruzica Piskac
WPES 2020
PDF - Strongly Unambiguous Büchi Automata Are Polynomially Predictable with Membership Queries
Dana Angluin, Timos Antonopoulos, Dana Fisman
CSL 2020
PDF - Specification and Inference of Trace Refinement Relations
Timos Antonopoulos, Eric Koskinen, Ton Chanh Le
OOPSLA 2019
PDF - Query Learning of Derived ω-Tree Languages in Polynomial Time
Dana Angluin, Timos Antonopoulos, Dana Fisman
LMCS 15(3), 21:1--21:29 (2019)
PDF - Games for Security under Adaptive Adversaries
Timos Antonopoulos, Tachio Terauchi
CSF 2019
PDF - A Formal Analysis of Timing Channel Security via Bucketing
Tachio Terauchi, Timos Antonopoulos
POST 2019
PDF - Counterexample-guided Approach to Finding Numerical Invariants
ThanhVu Nguyen, Timos Antonopoulos, Andrew Ruef, Michael Hicks
FSE 2017
PDF - Query Learning of Derived ω-Tree Languages in Polynomial Time
Dana Angluin, Timos Antonopoulos, Dana Fisman
CSL 2017
PDF - Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels
Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, Shiyi Wei
PLDI 2017
PDF - Three Variables are Enough for Real-Time Specification
Timos Antonopoulos, Paul Hunter, Shahab Raza, James Worrell
FoSSaCS 2015
PDF - Deciding Twig-definability of Node Selecting Tree Automata
Timos Antonopoulos, Dag Hovland, Wim Martens, Frank Neven
Theory Comput. Syst. 57(4): 967--1007 (2015)
PDF - Reachability Problems for Markov Chains
S. Akshay, Timos Antonopoulos, Joël Ouaknine, James Worrell
Inf. Process. Lett. 115(2): 155--158 (2015)
PDF - Foundations for Decision Problems in Separation Logic with General Inductive Predicates
Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max Kanovich, Joël Ouaknine
FoSSaCS 2014
PDF - Generating, Sampling and Counting Subclasses of Regular Tree Languages
Timos Antonopoulos, Floris Geerts, Wim Martens, Frank Neven
Theory Comput. Syst. 52(3):542--585 (2013)
PDF - Definability Problems for Graph Query Languages
Timos Antonopoulos, Frank Neven, Frédéric Servais
ICDT 2013
PDF - Deciding Twig-definability of Node Selecting Tree Automata
Timos Antonopoulos, Dag Hovland, Wim Martens, Frank Neven
ICDT 2012
PDF - The Complexity of Text-preserving XML Transformations
Timos Antonopoulos, Wim Martens, Frank Neven
PODS 2011
PDF - Generating, Sampling and Counting Subclasses of Regular Tree Languages
Timos Antonopoulos, Floris Geerts, Wim Martens, Frank Neven
ICDT 2011
PDF - Separating Graph Logic from MSO
Timos Antonopoulos and Anuj Dawar
FoSSaCS 2009
PDF
Thesis
- Expressive power of graph languages
Timos Antonopoulos
University of Cambridge, UK, 2009
Supervisor: Anuj Dawar
PDF