Verification of an Off-Line Checker for Priority Queues. - Hans de Nivelle; Ruzica Piskac (SEFM, 2005)

Linear Arithmetic with Stars. - Ruzica Piskac; Viktor Kuncak (CAV, 2008)

Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars. - Ruzica Piskac; Viktor Kuncak (CSL, 2008)

Decision Procedures for Multisets with Cardinality Constraints. - Ruzica Piskac; Viktor Kuncak (VMCAI, 2008)

Combining Theories with Shared Set Operations. - Thomas Wies; Ruzica Piskac; Viktor Kuncak (FroCoS, 2009)

MUNCH - Automated Reasoner for Sets and Multisets. - Ruzica Piskac; Viktor Kuncak (IJCAR, 2010)

Comfusy: A Tool for Complete Functional Synthesis. - Viktor Kuncak; Mikaël Mayer; Ruzica Piskac; Philippe Suter (CAV, 2010)

Ordered Sets in the Calculus of Data Structures. - Viktor Kuncak; Ruzica Piskac; Philippe Suter (CSL, 2010)

Complete functional synthesis. - Viktor Kuncak; Mikaël Mayer; Ruzica Piskac; Philippe Suter (PLDI, 2010)

Building a Calculus of Data Structures. - Viktor Kuncak; Ruzica Piskac; Philippe Suter; Thomas Wies (VMCAI, 2010)

Collections, Cardinalities, and Relations. - Kuat Yessenov; Ruzica Piskac; Viktor Kuncak (VMCAI, 2010)

Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. - Ruzica Piskac; Leonardo Mendonça de Moura; Nikolaj S. Bjørner (J. Autom. Reason., 2010)

Interactive Synthesis of Code Snippets. - Tihomir Gvero; Viktor Kuncak; Ruzica Piskac (CAV, 2011)

Decision Procedures for Automating Termination Proofs. - Ruzica Piskac; Thomas Wies (VMCAI, 2011)

Decision Procedures for Program Synthesis and Verification. - Ruzica Piskac (2011)

Software synthesis procedures. - Viktor Kuncak; Mikaël Mayer; Ruzica Piskac; Philippe Suter (Commun. ACM, 2012)

From Search to Computation: Redundancy Criteria and Simplification at Work. - Thomas Hillenbrand; Ruzica Piskac; Uwe Waldmann; Christoph Weidenbach (Programming Logics, 2013)

Incremental, Inductive Coverability. - Johannes Kloos; Rupak Majumdar; Filip Niksic; Ruzica Piskac (CAV, 2013)

Automating Separation Logic Using SMT. - Ruzica Piskac; Thomas Wies; Damien Zufferey (CAV, 2013)

Complete completion using types and weights. - Tihomir Gvero; Viktor Kuncak; Ivan Kuraj; Ruzica Piskac (PLDI, 2013)

Functional synthesis for linear arithmetic and sets. - Viktor Kuncak; Mikaël Mayer; Ruzica Piskac; Philippe Suter (Int. J. Softw. Tools Technol. Transf., 2013)

Automating Separation Logic with Trees and Data. - Ruzica Piskac; Thomas Wies; Damien Zufferey (CAV, 2014)

The FMCAD 2014 graduate student forum. - Ruzica Piskac (FMCAD, 2014)

GRASShopper - Complete Heap Verification with Mixed Specifications. - Ruzica Piskac; Thomas Wies; Damien Zufferey (TACAS, 2014)

A Type-Directed Approach to Program Repair. - Alex Reinking; Ruzica Piskac (CAV (1), 2015)

StriSynth: Synthesis for Live Programming. - Sumit Gulwani; Mikaël Mayer; Filip Niksic; Ruzica Piskac (ICSE (2), 2015)

InSynth: A System for Code Completion using Types and Weights. - Tihomir Gvero; Viktor Kuncak; Ivan Kuraj; Ruzica Piskac (Software Engineering & Management, 2015)

From Decision Procedures to Synthesis Procedures. - Ruzica Piskac (SYNASC, 2015)

Probabilistic Automated Language Learning for Configuration Files. - Mark Santolucito; Ennan Zhai; Ruzica Piskac (CAV (2), 2016)

Vehicle Platooning Simulations with Functional Reactive Programming. - Bernd Finkbeiner; Felix Klein 001; Ruzica Piskac; Mark Santolucito (SCAV@CPSWeek, 2017)

Synthesizing configuration file specifications with association rule learning. - Mark Santolucito; Ennan Zhai; Rahul Dhodapkar; Aaron Shim; Ruzica Piskac (Proc. ACM Program. Lang., 2017)

An auditing language for preventing correlated failures in the cloud. - Ennan Zhai; Ruzica Piskac; Ronghui Gu; Xun Lao; Xi Wang (Proc. ACM Program. Lang., 2017)

Programming-by-example for audio: synthesizing digital signal processing programs. - Mark Santolucito; Kate Rogers; Aedan Lombardo; Ruzica Piskac (FARM@ICFP, 2018)

Programming by Example: Efficient, but Not "Helpful". - Mark Santolucito; Drew Goldman; Allyson Weseley; Ruzica Piskac (PLATEAU@SPLASH, 2018)

New Applications of Software Synthesis: Verification of Configuration Files and Firewall Repair. - Ruzica Piskac (SAS, 2018)

Statically Verifying Continuous Integration Configurations. - Mark Santolucito; Jialu Zhang 002; Ennan Zhai; Ruzica Piskac (CoRR, 2018)

Temporal Stream Logic: Synthesis Beyond the Bools. - Bernd Finkbeiner; Felix Klein 001; Ruzica Piskac; Mark Santolucito (CAV (1), 2019)

Live Programming By Example. - Mark Santolucito; William T. Hallahan; Ruzica Piskac (CHI Extended Abstracts, 2019)

Synthesizing functional reactive programs. - Bernd Finkbeiner; Felix Klein 001; Ruzica Piskac; Mark Santolucito (Haskell@ICFP, 2019)

G2Q: Haskell constraint solving. - William T. Hallahan; Anton Xue; Ruzica Piskac (Haskell@ICFP, 2019)

Lazy counterfactual symbolic execution. - William T. Hallahan; Anton Xue; Maxwell Troy Bland; Ranjit Jhala; Ruzica Piskac (PLDI, 2019)

Identifying Maximal Non-Redundant Integer Cone Generators. - Slobodan Mitrovic; Ruzica Piskac; Viktor Kuncak (CoRR, 2019)

Grammar Filtering for Syntax-Guided Synthesis. - Kairo Morton; William T. Hallahan; Elven Shum; Ruzica Piskac; Mark Santolucito (AAAI, 2020)

Efficient Automated Reasoning About Sets and Multisets with Cardinality Constraints. - Ruzica Piskac (IJCAR (1), 2020)

Check before You Change: Preventing Correlated Failures in Service Updates. - Ennan Zhai; Ang Chen 001; Ruzica Piskac; Mahesh Balakrishnan 001; Bingchuan Tian; Bo Song; Haoliang Zhang (NSDI, 2020)

Towards checkpoint placement for dynamic memory allocation in intermittent computing. - Nicholas Shoemaker; Ruzica Piskac; Mark Santolucito (TAPAS@SPLASH, 2020)

Formal Methods and Computing Identity-based Mentorship for Early Stage Researchers. - Mark Santolucito; Ruzica Piskac (SIGCSE, 2020)

Solving $ mathrm {LIA} ^ star $ Using Approximations. - Maxwell Levatich; Nikolaj S. Bjørner; Ruzica Piskac; Sharon Shoham (VMCAI, 2020)

Privacy Preserving CTL Model Checking through Oblivious Graph Algorithms. - Samuel Judson; Ning Luo; Timos Antonopoulos; Ruzica Piskac (WPES@CCS, 2020)

Succinct Explanations With Cascading Decision Trees. - Jialu Zhang 002; Mark Santolucito; Ruzica Piskac (CoRR, 2020)

Automated repair by example for firewalls. - William T. Hallahan; Ennan Zhai; Ruzica Piskac (Formal Methods Syst. Des., 2020)

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)

Avenir: Managing Data Plane Diversity with Control Plane Synthesis. - Eric Hayden Campbell; William T. Hallahan; Priya Srikumar; Carmelo Cascone; Jed Liu; Vignesh Ramamurthy; Hossein Hojjat; Ruzica Piskac; Robert Soulé; Nate Foster (NSDI, 2021)

Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities. - Julien Lepiller; Ruzica Piskac; Martin Schäf; Mark Santolucito (TACAS (2), 2021)

Can Pre-trained Language Models be Used to Resolve Textual and Semantic Merge Conflicts? - Jialu Zhang 002; Todd Mytkowicz; Mike Kaufman; Ruzica Piskac; Shuvendu K. Lahiri (CoRR, 2021)

ppSAT: Towards Two-Party Private SAT Solving. - Ning Luo; Samuel Judson; Timos Antonopoulos; Ruzica Piskac; Xiao Wang 012 (IACR Cryptol. ePrint Arch., 2021)

Static detection of silent misconfigurations with deep interaction analysis. - Jialu Zhang 002; Ruzica Piskac; Ennan Zhai; Tianyin Xu (Proc. ACM Program. Lang., 2021)

Using pre-trained language models to resolve textual and semantic merge conflicts (experience paper). - Jialu Zhang 002; Todd Mytkowicz; Mike Kaufman; Ruzica Piskac; Shuvendu K. Lahiri (ISSTA, 2022)

Automated Feedback Generation for Competition-Level Code. - Jialu Zhang 002; De Li; John Charles Kolesar; Hanyuan Shi; Ruzica Piskac (ASE, 2022)

Can reactive synthesis and syntax-guided synthesis be friends? - Wonhyuk Choi; Bernd Finkbeiner; Ruzica Piskac; Mark Santolucito (PLDI, 2022)

Learning CI Configuration Correctness for Early Build Feedback. - Mark Santolucito; Jialu Zhang 002; Ennan Zhai; Jürgen Cito; Ruzica Piskac (SANER, 2022)

IVeri: Privacy-Preserving Interdomain Verification. - Ning Luo; Qiao Xiang; Timos Antonopoulos; Ruzica Piskac; Y. Richard Yang; Franck Le (CoRR, 2022)

Repairing Bugs in Python Assignments Using Large Language Models. - Jialu Zhang 002; José Cambronero; Sumit Gulwani; Vu Le 002; Ruzica Piskac; Gustavo Soares; Gust Verbruggen (CoRR, 2022)

Proving UNSAT in Zero Knowledge. - Ning Luo; Timos Antonopoulos; William R. Harris; Ruzica Piskac; Eran Tromer; Xiao Wang 012 (IACR Cryptol. ePrint Arch., 2022)

Checking equivalence in a non-strict language. - John C. Kolesar; Ruzica Piskac; William T. Hallahan (Proc. ACM Program. Lang., 2022)

Towards Automated Detection of Single-Trace Side-Channel Vulnerabilities in Constant-Time Cryptographic Code. - Ferhat Erata; Ruzica Piskac; Víctor Mateu; Jakub Szefer (EuroS&P, 2023)

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)

Formal XAI via Syntax-Guided Synthesis. - Katrine Bjørner; Samuel Judson; Filip Cano 001; Drew Goldman; Nicholas Shoemaker; Ruzica Piskac; Bettina Könighofer (AISoLA, 2023)

Accountable Software Systems (Dagstuhl Seminar 23411). - Bettina Könighofer; Joshua A. Kroll; Ruzica Piskac; Michael Veale; Filip Cano Córdoba (Dagstuhl Reports, 2023)

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 012; Ning Luo (IACR Cryptol. ePrint Arch., 2023)

Privacy-Preserving Regular Expression Matching using Nondeterministic Finite Automata. - Ning Luo; Chenkai Weng; Jaspal Singh; Gefei Tan; Ruzica Piskac; Mariana Raykova 001 (IACR Cryptol. ePrint Arch., 2023)

Ou: Automating the Parallelization of Zero-Knowledge Protocols. - Yuyang Sang; Ning Luo; Samuel Judson; Ben Chaimberg; Timos Antonopoulos; Xiao Wang 012; Ruzica Piskac; Zhong Shao 001 (IACR Cryptol. ePrint Arch., 2023)

Resilient Software Configuration and Infrastructure Code Analysis (Dagstuhl Seminar 23082). - Jürgen Cito; Ruzica Piskac; Mark Santolucito; Andy Zaidman; Daniel Sokolowski (Dagstuhl Reports, 2023)

ETAP: Energy-aware Timing Analysis of Intermittent Programs. - Ferhat Erata; Eren Yildiz; Arda Goknil; Kasim Sinan Yildirim; Jakub Szefer; Ruzica Piskac; Gökçin Sezgin (ACM Trans. Embed. Comput. Syst., 2023)

Proving Query Equivalence Using Linear Integer Arithmetic. - Haoran Ding; Zhaoguo Wang; Yicun Yang; Dexin Zhang; Zhenglin Xu; Haibo Chen 001; Ruzica Piskac; Jinyang Li 001 (Proc. ACM Manag. Data, 2023)

soid: A Tool for Legal Accountability for Automated Decision Making. - Samuel Judson; Matthew Elacqua; Filip Cano 001; Timos Antonopoulos; Bettina Könighofer; Scott J. Shapiro; Ruzica Piskac (CAV (2), 2024)

'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions. - Samuel Judson; Matthew Elacqua; Filip Cano 001; Timos Antonopoulos; Bettina Könighofer; Scott J. Shapiro; Ruzica Piskac (CSLAW, 2024)

Privacy-Preserving Regular Expression Matching Using TNFA. - Ning Luo; Chenkai Weng; Jaspal Singh; Gefei Tan; Mariana Raykova 001; Ruzica Piskac (ESORICS (2), 2024)

Systematic Use of Random Self-Reducibility in Cryptographic Code against Physical Attacks. - Ferhat Erata; Tinghung Chiu; Anthony Etim; Srilalith Nampally; Tejas Raju; Rajashree Ramu; Ruzica Piskac; Timos Antonopoulos; Wenjie Xiong 001; Jakub Szefer (ICCAD, 2024)

Testing Learning-Enabled Cyber-Physical Systems with Large-Language Models: A Formal Approach. - Xi Zheng 001; Aloysius K. Mok; Ruzica Piskac; Yong Jae Lee; Bhaskar Krishnamachari; Dakai Zhu 001; Oleg Sokolsky; Insup Lee 001 (SIGSOFT FSE Companion, 2024)

Systematic Use of Random Self-Reducibility against Physical Attacks. - Ferhat Erata; Tinghung Chiu; Anthony Etim; Srilalith Nampally; Tejas Raju; Rajashree Ramu; Ruzica Piskac; Timos Antonopoulos; Wenjie Xiong 001; Jakub Szefer (CoRR, 2024)

Scheherazade: Evaluating Chain-of-Thought Math Reasoning in LLMs with Chain-of-Problems. - Stephen Miner; Yoshiki Takashima; Simeng Han; Ferhat Erata; Timos Antonopoulos; Ruzica Piskac; Scott J. Shapiro (CoRR, 2024)

Learning Randomized Reductions and Program Properties. - Ferhat Erata; Orr Paradise; Timos Antonopoulos; ThanhVu Nguyen; Shafi Goldwasser; Ruzica Piskac (CoRR, 2024)

Automated Synthesis: Functional, Reactive and Beyond (Dagstuhl Seminar 24171). - S. Akshay 001; Bernd Finkbeiner; Kuldeep S. Meel; Ruzica Piskac; Arijit Shaw (Dagstuhl Reports, 2024)

PyDex: Repairing Bugs in Introductory Python Assignments using LLMs. - Jialu Zhang 002; José Pablo Cambronero; Sumit Gulwani; Vu Le 002; Ruzica Piskac; Gustavo Soares; Gust Verbruggen (Proc. ACM Program. Lang., 2024)

Quantum Circuit Reconstruction from Power Side-Channel Attacks on Quantum Computer Controllers. - Ferhat Erata; Chuanqi Xu; Ruzica Piskac; Jakub Szefer (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2024)

Privacy-Preserving SAT Solving (Invited Talk). - Ruzica Piskac (SAT, 2025)

NeuroStrata: Harnessing Neuro-Symbolic Paradigms for Improved Testability and Verifiability of Autonomous CPS. - Xi Zheng 001; Ziyang Li; Ivan Ruchkin; Ruzica Piskac; Miroslav Pajic (SIGSOFT FSE Companion, 2025)

Counterexample-Guided Inference of Modular Specifications. - William T. Hallahan; Ranjit Jhala; Ruzica Piskac (Proc. ACM Program. Lang., 2025)

NeuroStrata: Harnessing Neurosymbolic Paradigms for Improved Design, Testability, and Verifiability of Autonomous CPS. - Xi Zheng 001; Ziyang Li; Ivan Ruchkin; Ruzica Piskac; Miroslav Pajic (CoRR, 2025)

Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge. - John C. Kolesar; Shan Ali; Timos Antonopoulos; Ruzica Piskac (CoRR, 2025)

Automated Validating and Fixing of Text-to-SQL Translation with Execution Consistency. - Yicun Yang; Zhaoguo Wang; Yu Xia; Zhuoran Wei; Haoran Ding; Ruzica Piskac; Haibo Chen 001; Jinyang Li 001 (Proc. ACM Manag. Data, 2025)