Ruzica Piskac
Associate Professor of Computer Science (tenured)
Yale University
51 Prospect Street, office AKW 212
New Haven, CT 06511
Email: | |
Phone: | +1-203-432-8001 |
Bio
Ruzica Piskac is an associate professor of computer science at Yale University. Her 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. Ruzica joined Yale in 2013 as an assistant professor and prior to that, she was an independent research group leader at the Max Planck Institute for Software Systems in Germany. In July 2019, she was named the Donna L. Dubinsky Associate Professor of Computer Science, one of the highest recognition that an untenured faculty member at Yale can receive. Ruzica has received various recognitions for research and teaching, including the Patrick Denantes Prize for her PhD thesis, a CACM Research Highlight paper, an NSF CAREER award, the Facebook Communications and Networking award, the Microsoft Research Award for the Software Engineering Innovation Foundation (SEIF), the Amazon Research Award, and the 2019 Ackerman Award for Teaching and Mentoring.
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.
Research projects are described on the group website
Team
Ruzica Piskac is leading the Rigorous Software Engineering (ROSE) group.
Publications
[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] |
[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.