Selected Publications

This list of selected publications is sometimes old. A full list of recent publications may be found at my Google Scholar Profile.

 

Column-Oriented Datalog on the GPU. Yihao Sun, Sidharth Kumar, Thomas Gilray, and Kristopher Micinski. Proceedings of the AAAI Conference on Artificial Intelligence, 2025. Acceptance rate: 23.4%. https://arxiv.org/abs/2501.13051. [ bib ]

 

Bring Your Own Data Structures to Datalog. Arash Sahebolamri, Langston Barrett, Scott Moore, and Kristopher Micinski. Proc. ACM Program. Lang. (PACMPL), 7(OOPSLA Round 2 '23), October 2023. (Acceptance rate: 36%. Distinguished Paper award at OOPSLA '23). [ bib | DOI | http ]

The restricted logic programming language Datalog has become a popular implementation target for deductive-analytic workloads including social-media analytics and program analysis. Modern Datalog engines compile Datalog rules to joins over explicit representations of relations—often B-trees or hash maps. While these modern engines have enabled high scalability in many application domains, they have a crucial weakness: achieving the desired algorithmic complexity may be impossible due to representation-imposed overhead of the engine’s data structures. In this paper, we present the "Bring Your Own Data Structures" (Byods) approach, in the form of a DSL embedded in Rust. Using Byods, an engineer writes logical rules which are implicitly parametric on the concrete data structure representation; our implementation provides an interface to enable "bringing their own" data structures to represent relations, which harmoniously interact with code generated by our compiler (implemented as Rust procedural macros). We formalize the semantics of Byods as an extension of Datalog’s; our formalization captures the key properties demanded of data structures compatible with Byods, including properties required for incrementalized (semi-naïve) evaluation. We detail many applications of the Byods approach, implementing analyses requiring specialized data structures for transitive and equivalence relations to scale, including an optimized version of the Rust borrow checker Polonius; highly-parallel PageRank made possible by lattices; and a large-scale analysis of LLVM utilizing index-sharing to scale. Our results show that Byods offers both improved algorithmic scalability (reduced time and/or space complexity) and runtimes competitive with state-of-the-art parallelizing Datalog solvers.

 

Datalog with First-Class Facts. Thomas Gilray, Arash Sahebolamri, Yihao Sun, Sowmith Kunapaneni, Sidharth Kumar, and Kristopher Micinski. Proc. VLDB Endow. (VLDB '25), 18(3):651–665, April 2025. Acceptance rate not announced yet. [ bib | DOI | http ]

 

Distributed Cooperative Caching in Social Wireless Networks. Mahmoud Taghizadeh, Kristopher Micinski, Subir Biswas, Charles Ofria, and Eric Torng. IEEE Transactions on Mobile Computing, 12(6):1037--1053, 2013. [ bib | DOI ]

 

Is Function Similarity Over-Engineered? Building a Benchmark. Rebecca Saul, Chang Liu, Noah Fleischmann, Richard Zak, Kristopher Micinski, Edward Raff, and James Holt. Thirty-Eighth Annual Conference on Neural Information Processing Systems (NeurIPS '24 datasets and benchmarks track), 2024. [ bib ]

 

Incremental Evaluation of Dynamic Datalog Programs as a Higher-order DBSP Program. Bruno Rucy Carneiro Alves de Lima, Merlin Kramer, Kalmer Apinis, and Kristopher Micinski. the 5th International Workshop on the Resurgence of Datalog in Academia and Industry (Datalog 2.0 '24), 2024. [ bib ]

 

Assemblage: Automatic Binary Dataset Construction for Machine Learning. Chang Liu, Rebecca Saul, Yihao Sun, Edward Raff, Maya Fuchs, Townsend Southard Pantano, James Holt, and Kristopher Micinski. Thirty-Eighth Annual Conference on Neural Information Processing Systems (NeurIPS '24 datasets and benchmarks track), 2024. [ bib ]

 

Optimizing Datalog on the GPU. Yihao Sun, Ahmedur Rahman Shovon, Thomas Gilray, Sidharth Kumar, and Kristopher Micinski. ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS '25), March 2025. Acceptance rate: 20.5%, (105 out of 510). [ bib ]

 

Towards Iterative Relational Algebra on the GPU. Ahmedur Rahman Shovon, Thomas Gilray, Kristopher Micinski, and Sidharth Kumar. In 2023 USENIX Annual Technical Conference (USENIX ATC '23), pages 1009--1016, Boston, MA, July 2023. USENIX Association. (Acceptance rate: 18%). [ bib | http ]

 

Communication-Avoiding Recursive Aggregation. Yihao Sun, Thomas Gilray, Sidharth Kumar, and Kristopher Micinski. Proceedings of the IEEE Conference on Cluster Computing (IEEE Cluster '23), (Cluster), Oct 2023. (Acceptance rate: 24%). [ bib ]

 

Security Policies and Security Models. J. A. Goguen and J. Meseguer. In 1982 IEEE Symposium on Security and Privacy, pages 11--11, 1982. [ bib | DOI ]

 

Bounded Model Checking for Hyperproperties. Tzu-Han Hsu, César Sánchez, and Borzoo Bonakdarpour. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 94--112, Cham, 2021. Springer International Publishing. [ bib ]

This paper introduces a bounded model checking (BMC) algorithm for hyperproperties expressed in HyperLTL, which --- to the best of our knowledge --- is the first such algorithm. Just as the classic BMC technique for LTL primarily aims at finding bugs, our approach also targets identifying counterexamples. BMC for LTL is reduced to SAT solving, because LTL describes a property via inspecting individual traces. Our BMC approach naturally reduces to QBF solving, as HyperLTL allows explicit and simultaneous quantification over multiple traces. We report on successful and efficient model checking, implemented in our tool called HyperQube, of a rich set of experiments on a variety of case studies, including security, concurrent data structures, path planning for robots, and mutation testing.

 

HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties. Erika Ábrahám and Borzoo Bonakdarpour. In Annabelle McIver and Andras Horvath, editors, Quantitative Evaluation of Systems, pages 20--35, Cham, 2018. Springer International Publishing. [ bib ]

In this paper, we propose a new temporal logic for expressing and reasoning about probabilistic hyperproperties. Hyperproperties characterize the relation between different independent executions of a system. Probabilistic hyperproperties express quantitative dependencies between such executions. The standard temporal logics for probabilistic systems, i.e., PCTL and PCTL $$^*$$can refer only to a single path at a time and, hence, cannot express many probabilistic hyperproperties of interest. The logic proposed in this paper, HyperPCTL, adds explicit and simultaneous quantification over multiple traces to PCTL. Such quantification allows expressing probabilistic hyperproperties. A model checking algorithm for the proposed logic is also introduced for discrete-time Markov chains.

 

Asynchronous Extensions of HyperLTL. Laura Bozzelli, Adriano Peron, and César Sánchez. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1--13, 2021. [ bib | DOI ]

 

So You Want to Analyze Scheme Programs With Datalog? Davis Ross Silverman, Yihao Sun, Kristopher K. Micinski, and Thomas Gilray. CoRR, abs/2107.12909, 2021. (Acceptance rate: 80%). [ bib | arXiv | http ]

 

User Comfort with Android Background Resource Accesses in Different Contexts. Daniel Votipka, Seth M. Rabin, Kristopher Micinski, Thomas Gilray, Michelle L. Mazurek, and Jeffrey S. Foster. In Fourteenth Symposium on Usable Privacy and Security (SOUPS '18), pages 235--250, Baltimore, MD, August 2018. USENIX Association. [ bib | http ]

 

Optimizing the Bruck Algorithm for Non-Uniform All-to-All Communication. Ke Fan, Thomas Gilray, Valerio Pascucci, Xuan Huang, Kristopher Micinski, and Sidharth Kumar. In Proceedings of the 31st International Symposium on High-Performance Parallel and Distributed Computing (HPDC '22), HPDC '22, page 172–184, New York, NY, USA, 2022. Association for Computing Machinery. (Acceptance rate: 19%). [ bib | DOI | http ]

 

Exploring MPI Collective I/O and File-per-process I/O for Checkpointing a Logical Inference Task. Ke Fan, Kristopher Micinski, Thomas Gilray, and Sidharth Kumar. In 2021 IEEE International Parallel and Distributed Processing Symposium Workshops (IPDPSW '21), pages 965--972, 2021. [ bib | DOI ]

 

Seamless Deductive Inference via Macros. Arash Sahebolamri, Thomas Gilray, and Kristopher Micinski. In Proceedings of the 31st ACM SIGPLAN International Conference on Compiler Construction (CC '22), page 77–88, New York, NY, USA, 2022. Association for Computing Machinery. (Acceptance rate: 32%). [ bib | DOI | http ]

 

Declarative Demand-Driven Reverse Engineering. Yihao Sun, Jeffrey Ching, and Kristopher Micinski. In Workshop on Binary Analysis Research (textbfBAR '21) at NDSS 2021, February 2021. (Acceptance rate: 60%). [ bib | .pdf ]

 

Compiling Data-Parallel Datalog. Thomas Gilray, Sidharth Kumar, and Kristopher Micinski. In Proceedings of the 30th ACM SIGPLAN International Conference on Compiler Construction (CC '21), page 23–35, New York, NY, USA, 2021. Association for Computing Machinery. (Acceptance rate: 37%). [ bib | DOI | http ]

Datalog allows intuitive declarative specification of logical inference tasks while enjoying efficient implementation via state-of-the-art engines such as LogicBlox and Soufflé. These engines enable high-performance implementation of complex logical tasks including graph mining, program analysis, and business analytics. However, all efficient modern Datalog solvers make use of shared memory, and present inherent challenges scalability. In this paper, we leverage recent insights in parallel relational algebra and present a methodology for constructing data-parallel deductive databases. Our approach leverages recent developments in parallelizing relational algebra to create an efficient data-parallel semantics for Datalog. Based on our methodology, we have implemented the first MPI-based data-parallel Datalog solver. Our experiments demonstrate comparable performance and improved single-node scalability versus Soufflé, a state-of-art solver.

 

Abstracting Faceted Execution. Kristopher Micinski, David Darais, and Thomas Gilray. In 2020 IEEE 33rd Computer Security Foundations Symposium (CSF '20), pages 184--198, 2020. (Acceptance rate: 25%). [ bib | DOI ]

 

An observational investigation of reverse engineers' processes. Daniel Votipka, Seth M. Rabin, Kristopher Micinski, Jeffrey S. Foster, and Michelle M. Mazurek. In Proceedings of the 29th USENIX Security Symposium (USENIX '20), Proceedings of the 29th USENIX Security Symposium, pages 1875--1892. USENIX Association, 2020. (Acceptance rate: 16.1%). [ bib ]

Reverse engineering is a complex process essential to software-security tasks such as vulnerability discovery and malware analysis. Significant research and engineering effort has gone into developing tools to support reverse engineers. However, little work has been done to understand the way reverse engineers think when analyzing programs, leaving tool developers to make interface design decisions based only on intuition. This paper takes a first step toward a better understanding of reverse engineers' processes, with the goal of producing insights for improving interaction design for reverse engineering tools. We present the results of a semi-structured, observational interview study of reverse engineers (N=16). Each observation investigated the questions reverse engineers ask as they probe a program, how they answer these questions, and the decisions they make throughout the reverse engineering process. From the interview responses, we distill a model of the reverse engineering process, divided into three phases: overview, sub-component scanning, and focused experimentation. Each analysis phase's results feed the next as reverse engineers' mental representations become more concrete. We find that reverse engineers typically use static methods in the first two phases, but dynamic methods in the final phase, with experience playing large, but varying, roles in each phase. Based on these results, we provide five interaction design guidelines for reverse engineering tools.

 

Symbolic Path Tracing to Find Android Permission-Use Triggers, Kristopher Micinski, Thomas Gilray, Daniel Votipka, Jeffrey S. Foster, and Michelle L. Mazurek. February 2019. [ bib | .pdf ]

 

Racets: Faceted Execution in Racket. Kristopher K. Micinski, Zhanpeng Wang, and Thomas Gilray. In Scheme Workshop at ICFP 2018 (Scheme '18), 2018. [ bib | http ]

 

User Interactions and Permission Use on Android. Kristopher Micinski, Daniel Votipka, Rock Stevens, Nikolaos Kofinas, Jeffrey S. Foster, and Michelle L. Mazurek. In Conference on Human Factors in Computing Systems (CHI '17), 2017. [ bib | .pdf ]

 

Checking Interaction-Based Declassification Policies for Android Using Symbolic Execution. Kristopher Micinski, Jonathan Fetter-Degges, Jinseong Jeon, Jeffrey S. Foster, and Michael R. Clarkson. In European Symposium on Research in Computer Security (ESORICS '15), volume 9327 of Lecture Notes in Computer Science, pages 520--538, Vienna, Austria, September 2015. [ bib | .pdf ]

 

An Empirical Study of Location Truncation on Android. Kristopher Micinski, Philip Phelps, and Jeffrey S. Foster. In Mobile Security Technologies (MoST '13), San Francisco, CA, May 2013. [ bib | .pdf ]

 

Dr. Android and Mr. Hide: Fine-grained Permissions in Android Applications. Jinseong Jeon, Kristopher Micinski, Jeffrey A. Vaughan, Ari Fogel, Nikhilesh Reddy, Jeffrey S. Foster, and Todd Millstein. In ACM CCS Workshop on Security and Privacy in Smartphones and Mobile Devices (SPSM '12), pages 3--14, Raleigh, NC, USA, October 2012. [ bib | .pdf ]

 

Temporal Logics for Hyperproperties. Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher Micinski, Markus N. Rabe, and César Sánchez. In Martín Abadi and Steve Kremer, editors, Principles of Security and Trust (POST '14), volume 8414 of Lecture Notes in Computer Science, pages 265--284. Springer Berlin Heidelberg, 2014. [ bib | .pdf ]

 

SymDroid: Symbolic Execution for Dalvik Bytecode. Jinseong Jeon, Kristopher Micinski, and Jeffrey S. Foster. Technical Report CS-TR-5022, Department of Computer Science, University of Maryland, College Park, July 2012. [ bib | .pdf ]

 

Multi-Node Multi-GPU Datalog. Ahmedur Rahman Shovon, Yihao Sun, Kristopher Micinski, Thomas Gilray, and Sidharth Kumar. In Proceedings of the 39th ACM International Conference on Supercomputing, ICS '25, page 822–836, New York, NY, USA, 2025. Association for Computing Machinery. Acceptance rate: 23.4%. [ bib | DOI | http ]

Datalog, a declarative logic programming language that operates bottom-up, has experienced increasing popularity due to its natural handling of recursive queries. Its applications span diverse fields, including graph mining, program analysis, deductive databases, and neuro-symbolic reasoning. While Datalog shares similarities with SQL in using relational algebra kernels, it uniquely employs iterative execution until reaching a fixed point to support recursion. Current Datalog engines like SLOG, LogicBlox and Soufflé work well with multi-core and multi-threaded systems, but none have yet tackled multi-node, multi-GPU architectures. Our research addresses this gap by developing the first multi-GPU, multi-node Datalog engine. This advancement is particularly for high-performance computing (HPC) systems, which typically feature multiple GPUs per node. Our implementation combines MPI for inter-node communication with CUDA for GPU parallelization, enabling the processing of massive datasets in real time. We have created novel data-parallel implementations of core relational algebra operations (join), while also optimizing deduplication and tuple materialization. To handle iterative execution, we have developed two novel GPU-accelerated methods for non-uniform all-to-all data exchange. Evaluating on Argonne National Lab’s Polaris supercomputer demonstrated our engine’s effectiveness, achieving performance improvements of up to 32 against state-of-the-art multi-node Datalog engine.

 

Checking Interaction-Based Declassification Policies for Android Using Symbolic Execution. Kristopher K. Micinski, Jonathan Fetter-Degges, Jinseong Jeon, Jeffrey S. Foster, and Michael R. Clarkson. CoRR, abs/1504.03711, 2015. [ bib | http ]

 

Dr. Android and Mr. Hide: Fine-grained security policies on unmodified Android. Jinseong Jeon, Kristopher K. Micinski, Jeffrey A. Vaughan, Nikhilesh Reddy, Yixin Zhu, Jeffrey S. Foster, and Todd Millstein. Technical Report CS-TR-5006, Department of Computer Science, University of Maryland, College Park, December 2011. [ bib ]

 

A Temporal Logic of Security. Masoud Koleini, Michael R. Clarkson, and Kristopher K. Micinski. CoRR, abs/1306.5678, 2013. [ bib | http ]