Ruzica Piskac is an assistant professor (tenure-track) at Yale, Computer Science Department. 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 has received a NSF CAREER award for her proposal, "Synthesis in a Live Programming Environment".
Ruzica received her PhD degree from the École polytechnique fédérale de Lausanne (EPFL) in 2011. She was awarded the Patrick Denantes Memorial Prize for her PhD dissertation. Her advisor was Viktor Kunčak. She holds a Master's degree in Computer Science, obtained from the University of Saarland (supervised by Harald Ganzinger at Max-Planck Institute for Computer Science) in Saarbrücken, Germany, as well as a Master's degree in mathematics from the University of Zagreb, Croatia.
For more information, see her complete CV.
51 Prospect Street, office AKW 212
New Haven, CT 06511
(203) 432 8001
Misconfiguration errors account for the majority of downtime in real-world deployed systems. ConfigC is a machine learning based system to automatically learn specifications for configuration files and check for correctness. It uses an association rule learning approach to build sets of predicates any correct configuration files must satisfy.
G2 is a symbolic execution framework for Haskell that utilizes evaluation and translation of semi-compiled Haskell source. The project is intended for automatic program exploration and input-output example generation, with additional goals to tackle difficult problems such as constraint solving for higher-order functions.
Winston is a type-directed expression synthesis tool that can also generate repairs of ill-typed expressions from their sound subexpressions. It uses a novel search space pruning technique based on graph distance to run interactively.
GRASShopper is an experimental verification tool for programs that manipulate dynamically allocated data structures. GRASShopper programs can be annotated with specifications expressed in a decidable specification logic to check functional correctness properties. The logic supports mixing of separation logic and first-order logic assertions, yielding expressive yet concise specifications.