Ruzica Piskac

Professor of Computer Science

Yale University

51 Prospect Street, office AKW 212

New Haven, CT 06511

Email:
Phone:	+1-203-432-8001

Bio

Short Bio

Ruzica Piskac is a Professor of Computer Science at Yale University, where she leads the Rigorous Software Engineering (ROSE) group. Her research interests span the areas of software verification, security and applied cryptography, automated reasoning, and code synthesis. Much of her research has focused on using formal techniques to improve software reliability and trustworthiness. Piskac joined Yale’s Department of Computer Science in 2013. She was previously an Independent Research Group Leader at the Max Planck Institute for Software Systems in Germany. Her research has received a range of professional honors, including multiple Amazon Research Awards, Yale University’s Ackerman Award for Teaching and Mentoring, the Facebook Communications and Networking Award, and the Microsoft Research Award for the Software Engineering Innovation Foundation (SEIF). In 2019, Yale named Piskac the Donna L. Dubinsky Associate Professor of Computer Science. Piskac holds a Ph.D. from the Swiss Federal Institute of Technology (EPFL), where her dissertation won the Patrick Denantes Prize. Her current and recent professional activities include service as Program Chair of the 37th International Conference on Computer Aided Verification and the Steering Committee of the Formal Methods in Computer-Aided Design conference. Piskac has graduated five PhD students, four of them are currently holding a position of an assistant professor of computer science.

Education and Previous Affiliations

Max Planck Institute for Software Systems, Germany

Leading an independent research group on synthesis, analysis and automated reasoning (2012 - 2013)

EPFL, Switzerland

PhD in Computer Science (2011)
Thesis title: Decision Procedures for Program Synthesis and Verification
Advisor: Viktor Kuncak

Research

Ruzica Piskac's research interests span the areas of programming languages, software verification, automated reasoning, and code synthesis. A common thread in Ruzica's research is improving software reliability and trustworthiness using formal techniques.

On-going Projects

Research projects are described on the group website

Funding sponsors

Team

Ruzica Piskac is leading the Rigorous Software Engineering (ROSE) group.

Publications

Conference / Journal Papers

[OOPSLA'24]	Jialu Zhang, José Cambronero, Sumit Gulwani, Vu Le, Ruzica Piskac, Gustavo Soares, Gust Verbruggen: PyDex: Repairing Bugs in Introductory Python Assignments Using Large Language Models, in Proceedings of the ACM on Programming Languages, Volume 8, Issue OOPSLA1, Article No.: 133, pp.1100-1124. [url]
[USENIX'24]	Daniel Luick, John C. Kolesar, Timos Antonopoulos, William R. Harris, James Parker, Ruzica Piskac, Eran Tromer, Xiao Wang, Ning Luo: ZKSMT: A VM for Proving SMT Theorems in Zero Knowledge, in the 33rd USENIX Security Symposium, to appear. [url]
[CAV'24]	Samuel Judson, Matthew Elacqua, Filip Cano, Timos Antonopoulos, Bettina Könighofer, Scott J. Shapiro, Ruzica Piskac: soid: A Tool for Legal Accountability for Automated Decision Making, in the 36th International Conference on Computer Aided Verification (CAV 2024), pp.233-246. [url]
[SIGMOD'24]	Haoran Ding, Zhaoguo Wang, Yicun Yang, Dexin Zhang, Zhenglin Xu, Haibo Chen, Ruzica Piskac, Jinyang Li: Proving Query Equivalence Using Linear Integer Arithmetic, in Proceedings of the ACM on Management of Data, Volume 1, Issue 4, Article No.: 227, pp.1-26. [url]
[TCHES]	Ferhat Erata, Chuanqi Xu, Ruzica Piskac, Jakub Szefer: Quantum Circuit Reconstruction from Power Side-Channel Attacks on Quantum Computer Controllers, in IACR Transactions on Cryptographic Hardware and Embedded Systems, TCHES 2024 Issue 2, pp. 735-768. [url]
[CSLAW'24]	Samuel Judson, Matthew Elacqua, Filip Cano, Timos Antonopoulos, Bettina Könighofer, Scott J. Shapiro, Ruzica Piskac: 'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions, in the 3rd ACM Symposium on Computer Science and Law (CS & Law 2024), pp.73-85. [url]
[FSE'24]	Xi Zheng, Aloysius K. Mok, Ruzica Piskac, Yong Jae Lee, Bhaskar Krishnamachari, Dakai Zhu, Oleg Sokolsky, Insup Lee: Testing Learning-Enabled Cyber-Physical Systems with Large-Language Models: A Formal Approach, in Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering (FSE 2024), pp.467-471. [url]
[AISOLA'23]	Katrine Bjørner, Samuel Judson, Filip Cano Córdoba, Drew Goldman, Nicholas Shoemaker, Ruzica Piskac, Bettina Könighofer: Formal XAI via Syntax-Guided Synthesis, in the 1st International Conference on Bridging the Gap Between AI and Reality (AISoLA 2023), pp.119-137. [url]
[CCS'23]	Yuyang Sang, Ning Luo, Samuel Judson, Ben Chaimberg, Timos Antonopoulos, Ruzica Piskac, Xiao Wang, Zhong Shao: Ou: Automating the Parallelization of Zero-Knowledge Protocols, in the 29th ACM SIGSAC Conference on Computer and Communications Security (CCS 2023), pp.534-548. [url]
[IJCAI'23]	Filip Cano Córdoba, Samuel Judson, Timos Antonopoulos, Katrine Bjørner, Nicholas Shoemaker, Scott J. Shapiro, Ruzica Piskac, Bettina Könighofer: Analyzing intentional behavior in autonomous agents under uncertainty, in the 32nd International Joint Conference on Artificial Intelligence, (IJCAI 2023), pp.372-381. [url]
[EuroS&P'23]	Ferhat Erata, Ruzica Piskac, Víctor Mateu, Jakub Szefer: Towards Automated Detection of Single-Trace Side-Channel Vulnerabilities in Constant-Time Cryptographic Code, in the 8th IEEE European Symposium on Security and Privacy, (EuroS&P 2023), pp.687-706. [url]
[TECS]	Ferhat Erata, Eren Yildiz, Arda Goknil, Kasim Sinan Yildirim, Jakub Szefer, Ruzica Piskac, Gokcin Sezgin: ETAP: Energy-aware timing analysis of intermittent programs, in ACM Transactions on Embedded Computing Systems, Volume 22, Issue 2, Article No.: 23, pp. 1-31. [url]
[OOPSLA'22]	John C. Kolesar, Ruzica Piskac, William T. Hallahan: Checking equivalence in a non-strict language, in Proceedings of the ACM on Programming Languages, Volume 6, Issue OOPSLA2, pp.1469-1496. [url]
[CCS'22]	Ning Luo, Timos Antonopoulos, William R. Harris, Ruzica Piskac, Eran Tromer, Xiao Wang: Proving UNSAT in Zero Knowledge, in the 28th ACM SIGSAC Conference on Computer and Communications Security (CCS 2022), pp.2203-2217. [url] [Distinguished Paper Award]
[ISSTA'22]	Jialu Zhang, Todd Mytkowicz, Mike Kaufman, Ruzica Piskac, Shuvendu K. Lahiri: Using pre-trained language models to resolve textual and semantic merge conflicts (experience paper), in the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2022), pp.77-88. [url]
[ASE'22]	Jialu Zhang, De Li, John Charles Kolesar, Hanyuan Shi, Ruzica Piskac: Automated Feedback Generation for Competition-Level Code, in the 37th IEEE/ACM International Conference on Automated Software Engineering (ASE 2022), pp.13:1-13:13. [url]
[PLDI'22]	Wonhyuk Choi, Bernd Finkbeiner, Ruzica Piskac, Mark Santolucito: Can reactive synthesis and syntax-guided synthesis be friends?, in the 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2022), pp.229-243. [url]
[SANER'22]	Mark Santolucito, Jialu Zhang, Ennan Zhai, Jürgen Cito, Ruzica Piskac: Learning CI Configuration Correctness for Early Build Feedback, in the 29th IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER 2022), pp.1006-1017. [url]
[USENIX'22]	Ning Luo, Samuel Judson, Timos Antonopoulos, Ruzica Piskac, Xiao Wang: ppSAT: Towards Two-Party Private SAT Solving, in the 31st USENIX Security Symposium, pp.2983-3000. [url]
[OOPSLA'21]	Jialu Zhang, Ruzica Piskac, Ennan Zhai, Tianyin Xu: Static detection of silent misconfigurations with deep interaction analysis, in the 36th ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'21), pp.1-30. [url]
[TACAS'21]	Julien Lepiller, Ruzica Piskac, Martin Schaef, Mark Santolucito: Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities, in the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021), pp. 105-123. [url] [Extended version]
[NSDI'21]	Eric Campbell, William Hallahan, Priya Srikumar, Carmelo Cascone, Jed Liu, Vignesh Ramamurthy, Hossein Hojjat, Ruzica Piskac, Robert Soulé, Nate Foster: Avenir: Managing Data Plane Diversity with Control Plane Synthesis, in the 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2021), pp. 133-153. [url]
[INFOCOM'21]	Yichao Cheng, Ning Luo, Jingxuan Zhang, Timos Antonopoulos, Ruzica Piskac, Qiao Xiang: Looking for the Maximum Independent Set: A New Perspective on the Stable Path Problem, in the 16th IEEE International Conference on Computer Communications (INFOCOM 2021), pp. 1-10. [url]
[FMSD]	William T. Hallahan, Ennan Zhai, Ruzica Piskac: Automated Repair by Example for Firewalls, in the International Journal on Formal Methods in System Design (FMSD), volume 56, pp. 127-153. [url]
[TAPAS'20]	Nicholas Shoemaker, Ruzica Piskac, Mark Santolucito: Towards Checkpoint Placement for Dynamic Memory Allocation in Intermittent Computing, in the 11th Workshop on Tools for Automatic Program Analysis (TAPAS 2020), pp. 20-22. [url]
[WPES'20]	Samuel Judson, Ning Luo, Timos Antonopoulos, Ruzica Piskac: Privacy Preserving CTL Model Checking through Oblivious Graph Algorithms, in the 19th Workshop on Privacy in the Electronic Society (WPES 2020), pp. 101-115. [url]
[IJCAR'20]	Ruzica Piskac: Efficient Automated Reasoning About Sets and Multisets with Cardinality Constraints, in the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), pp. 3-10. [url]
[NSDI'20]	Ennan Zhai, Ang Chen, Ruzica Piskac, Mahesh Balakrishnan, Bingchuan Tian, Bo Song, Haoliang Zhang: Check before You Change: Preventing Correlated Failures in Service Updates, in the 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2020), pp. 575-589. [url]
[AAAI'20]	Kairo Morton, William Hallahan, Elven Shum, Ruzica Piskac, Mark Santolucito: Grammar Filtering for Syntax Guided Synthesis, in the 34th AAAI Conference on Artificial Intelligence (AAAI 2020), pp. 1611-1618. [url]
[SIGCSE'20]	Mark Santolucito, Ruzica Piskac: Formal Methods and Computing Identity-based Mentorship for Early Stage Researchers, in the 51st ACM Technical Symposium on Computer Science Education (SIGCSE 2020), pp. 135-141. [url]
[VMCAI'20]	Maxwell Levatich, Nikolaj Bjøner, Ruzica Piskac, Sharon Shohan: Solving LIA* Using Approximations, in the 21st International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2020), pp. 360-378. [url]
[Haskell'19]	William T. Hallahan, Anton Xue, Ruzica Piskac: G2Q: Haskell Constraint Solving, in the 12th ACM SIGPLAN International Symposium on Haskell (Haskell@ICFP 2019), pp. 44–57. [url]
[Haskell'19]	Bernd Finkbeiner, Felix Klein, Ruzica Piskac, Mark Santolucito: Synthesizing functional reactive programs, in the 12th ACM SIGPLAN International Symposium on Haskell (Haskell@ICFP 2019), pp. 162-175. [url]
[CAV'19]	Bernd Finkbeiner, Felix Klein, Ruzica Piskac, Mark Santolucito: Temporal Stream Logic: Synthesis Beyond the Bools, in the 31st International Conference on Computer Aided Verification (CAV 2019), pp. 609-629. [url]
[PLDI'19]	William T. Hallahan, Anton Xue, Maxwell Troy Bland, Ranjit Jhala, Ruzica Piskac: Lazy counterfactual symbolic execution, in the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019), pp. 411-424. [url]
[CHI'19]	Mark Santolucito, William T. Hallahan, Ruzica Piskac: Live Programming By Example, in Extended Abstracts of the 2019 CHI Conference on Human Factors in Computing Systems (CHI 2019) [url]
[PLATEAU'18]	Mark Santolucito, Drew Goldman, Allyson Weseley, Ruzica Piskac: Programming by Example: Efficient, but Not "Helpful", in the 9th Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU@SPLASH 2018), pp. 3:1-3:10. [url]
[FARM'18]	Mark Santolucito, Kate Rogers, Aedan Lombardo, Ruzica Piskac: Programming-by-example for audio: synthesizing digital signal processing programs, in the 6th ACM SIGPLAN International Workshop on Functional Art, Music, Modeling, and Design (FARM@ICFP 2018), pp. 18-25. [url]
[SAS'18]	Ruzica Piskac: New Applications of Software Synthesis: Verification of Configuration Files and Firewall Repair, in the 25th International Symposium (SAS 2018), pp. 71-76. [url]
[OOPSLA'17]	Ennan Zhai, Ruzica Piskac, Ronghui Gu, Xun Lao, Xi Wang: An auditing language for preventing correlated failures in the cloud, in the 32th ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'17), pp.97:1-97:28. [url]
[OOPSLA'17]	Mark Santolucito, Ennan Zhai, Rahul Dhodapkar, Aaron Shim, Ruzica Piskac: Synthesizing configuration file specifications with association rule learning, in the 32th ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'17), pp. 64:1-64:20. [url]
[FMCAD'17]	William T. Hallahan, Ennan Zhai, Ruzica Piskac: Automated repair by example for firewalls, in the 17th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2017), pp. 220-229. [url]
[SCAV'17]	Bernd Finkbeiner, Felix Klein, Ruzica Piskac, Mark Santolucito: Vehicle Platooning Simulations with Functional Reactive Programming, in the 1st International Workshop on Safe Control of Connected and Autonomous Vehicles (SCAV@CPSWeek 2017), pp. 43-47. [url]
[CAV'16]	Mark Santolucito, Ennan Zhai, Ruzica Piskac: Probabilistic Automated Language Learning for Configuration Files, in the 28th International Conference on Computer Aided Verification (CAV 2016), pp. 80-87. [url]
[CAV'15]	Alex Reinking, Ruzica Piskac: A Type-Directed Approach to Program Repair, in the 27th International Conference on Computer Aided Verification (CAV 2015), pp. 511-517. [url]
[ICSE'15]	Sumit Gulwani, Mikaël Mayer, Filip Niksic, Ruzica Piskac: StriSynth: Synthesis for Live Programming, in the 37th IEEE/ACM International Conference on Software Engineering (ICSE 2015), pp. 701-704. [url]
[SWM'15]	Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, Ruzica Piskac: InSynth: A System for Code Completion using Types and Weights, in the Software Engineering & Management 2015, pp. 39-40.
[SYNASC'15]	Ruzica Piskac: From Decision Procedures to Synthesis Procedures, in the 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2015), pp. 3-10. [url]
[CAV'14]	Ruzica Piskac, Thomas Wies, Damien Zufferey: Automating Separation Logic with Trees and Data, in the 26th International Conference on Computer Aided Verification (CAV 2014), pp. 711-728. [url]
[TACAS'14]	Ruzica Piskac, Thomas Wies, Damien Zufferey: GRASShopper: Complete Heap Verification with Mixed Specifications, in the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014), pp. 124-139. [url]
[CAV'13]	Johannes Kloos, Rupak Majumdar, Filip Niksic, Ruzica Piskac: Incremental, Inductive Coverability, in the 25th International Conference on Computer Aided Verification (CAV 2013), pp. 158-173. [url]
[CAV'13]	Ruzica Piskac, Thomas Wies, Damien Zufferey: Automating Separation Logic Using SMT, in the 25th International Conference on Computer Aided Verification (CAV 2013), pp. 773-789. [url]
[BOOK]	Thomas Hillenbrand, Ruzica Piskac, Uwe Waldmann, Christoph Weidenbach: From Search to Computation: Redundancy Criteria and Simplification at Work, in the Programming Logics - Essays in Memory of Harald Ganzinger, pp. 169-193. [url]
[STTT]	Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter: Functional synthesis for linear arithmetic and sets, in the International Journal on Software Tools for Technology Transfer (STTT) 15(5-6), pp. 455-474. [url]
[PLDI'13]	Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, Ruzica Piskac: Complete Completion using Types and Weights, in the ACM SIGPLAN 2013 Conference on Programming Language Design and Implementation (PLDI 2013), pp. 27-38. [url]
[CACM]	Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter: Software Synthesis Procedures, in the Communications of the ACM (55), Volume 55, Number 2, pp. 103-111. [Research Highlight] [url]
[CAV'11]	Tihomir Gvero, Viktor Kuncak, Ruzica Piskac: Interactive Synthesis of Code Snippets, in the 23rd International Conference on Computer Aided Verification (CAV 2011), pp. 418-423. [url]
[VMCAI'11]	Ruzica Piskac, Thomas Wies: Decision Procedures for Automating Termination Proofs, in the 12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2011), pp. 371-386. [url]
[CSL'10]	Viktor Kuncak, Ruzica Piskac, Philippe Suter: Ordered Sets in the Calculus of Data Structures, in the 19th Annual Computer Science Logic (CSL 2010), pp. 34-48. [url]
[JAR]	Ruzica Piskac, Leonardo de Moura, Nikolaj Bjørner: Deciding Effectively Propositional Logic Using DPLL and Substitution Sets, in Journal of Automated Reasoning, Volume 44, Number 4, pp. 401-424. [url]
[IJCAR'10]	Ruzica Piskac, Viktor Kuncak: MUNCH - Automated Reasoner for Sets and Multisets, in the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), pp. 149-155. [url]
[CAV'10]	Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter: Comfusy: A Tool for Complete Functional Synthesis, in the 22nd International Conference on Computer Aided Verification (CAV 2010), pp. 430-433. [url]
[PLDI'10]	Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter: Complete functional synthesis, in the ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation (PLDI 2010), pp. 316-329. [url]
[VMCAI'10]	Viktor Kuncak, Ruzica Piskac, Philippe Suter, Thomas Wies: Building a Calculus of Data Structures, in the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2010), pp. 26-44. [url]
[VMCAI'10]	Kuat Yessenov, Ruzica Piskac, Viktor Kuncak: Collections, Cardinalities, and Relations, in the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2010), pp. 380-395. [url]
[FroCoS'09]	Thomas Wies, Ruzica Piskac, Viktor Kuncak: Combining Theories with Shared Set Operations, in the 7th International Symposium on Frontiers of Combining Systems (FroCoS 2009), pp. 366-382. [url]
[CSL'08]	Ruzica Piskac, Viktor Kuncak: Fractional Collections with Cardinality Bounds, in the 17th Annual Computer Science Logic Conference (CSL 2008), pp. 124-138. [url]
[CAV'08]	Ruzica Piskac, Viktor Kuncak: Linear Arithmetic with Stars, in the 20th International Conference on Computer Aided Verification (CAV 2008), pp. 268-280. [url]
[VMCAI'08]	Ruzica Piskac, Viktor Kuncak: Decision Procedures for Multisets with Cardinality Constraints, in the 9th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2008), pp. 218-232. [url]
[SEFM'05]	Hans de Nivelle, Ruzica Piskac: Verification of an Off-Line Checker for Priority Queues, in the 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), pp. 210-219. [url]

Proceedings Editorial

[LPAR'23]	Ruzica Piskac, Andrei Voronkov: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2023), EPiC Series in Computing 94, EasyChair 2023.
[FMCAD'21]	Ruzica Piskac, Michael Whalen: Proceedings of the 21th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2021), IEEE 2021, ISBN 978-3-85448-046-4.
[VMCAI'19]	Constantin Enea, Ruzica Piskac: Proceedings of the 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2019), Lecture Notes in Computer Science 11388, Springer 2019, ISBN 978-3-030-11244-8.
[VSTTE'18]	Ruzica Piskac, Philipp Rümmer: Proceedings of the 10th International Conference on Verified Software, Theories, Tools, and Experiments (VSTTE 2018), Lecture Notes in Computer Science 11294, Springer 2018, ISBN 978-3-030-03591-4.
[FMCAD'16]	Ruzica Piskac, Muralidhar Talupur: Proceedings of the 16th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2016), IEEE 2016, ISBN 978-0-9835678-6-8.
[SMT'16]	Tim King, Ruzica Piskac: Proceedings of the 14th International Workshop on Satisfiability Modulo Theories (SMT 2016), CEUR Workshop Proceedings 1617.
[SYNT'16]	Rayna Dimitrova, Ruzica Piskac: Proceedings of the 5th International Workshop on Synthesis (SYNT 2016), Electronic Proceedings in Theoretical Computer Science 229.

Theses

[PhD'11]	Ruzica Piskac: Decision Procedures for Program Synthesis and Verification, PhD thesis, The Ecole polytechnique fédérale de Lausanne (EPFL), 2011 [Patrick Denantes Prize].
[MSc'05]	Ruzica Piskac: Formal Correctness of Result Checking for Priority Queues, Master's thesis, Saarland University, 2005.

Teaching

Listed in the CV.

Service

Listed in the CV.