Ruzica Piskac

Max Planck Institute for Software Systems (MPI-SWS)
Email:

[ About | Publications | Professional Activities | Teaching | Students | Research Opportunities | Contact ]


About

I am tenure-track faculty at the Max Planck Institute for Software Systems (MPI-SWS).

Prior to joining MPI-SWS, I was a graduate student at the EPFL (2007-2011), where I worked under the supervision of Viktor Kuncak.

My research interests span the areas of software verification, automated reasoning, code synthesis and program termination. A common thread in my research is improving software reliability and trustworthiness using formal techniques.

Curriculum Vitae

Publications

  1. Incremental, Inductive Coverability, with J. Kloos, R. Majumdar, F. Niksic.
    To appear in the Proceedings of 25th International Conference on Computer Aided Verification (CAV 2013).
  2. Automating Separation Logic using SMT, with T. Wies, D. Zufferey.
    Proceedings of 25th International Conference on Computer Aided Verification - CAV 2013, Saint Petersburg, Russia, p. 773-789.
    An extended version of this paper is available as NYU Technical Report TR2013-954, March, 2013.
  3. Complete Completion using Types and Weights, with T. Gvaro, I. Kuraj, V. Kuncak.
    To appear in the Proceedings of 34th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI 2013).
  4. Software Synthesis Procedures, with V. Kuncak, M. Mayer, P. Suter.
    Communications of the ACM, Volume 55, Number 2, p. 103-111, DOI: 10.1145/2076450.2076472 February 2012.
  5. Interactive Synthesis of Code Snippets , with T. Gvero, V. Kuncak.
    Proceedings of the 23rd International Conference on Computer Aided Verification - CAV 2011, Snowbird, UT, USA. Springer, LNCS Volume 6806, p. 418-423. USA.
  6. Decision Procedures for Automating Termination Proofs , with T. Wies.
    Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation - VMCAI 2011, Austin, TX, USA. Springer, LNCS Volume 6538, p. 371-386.
  7. Ordered Sets in the Calculus of Data Structures , with V. Kuncak, P. Suter.
    Proceedings of the 19th Annual Computer Science Logic - CSL 2010, Brno, Czech Republic. Springer, LNCS Volume 6247, p. 34-48.
  8. MUNCH - Automated Reasoner for Sets and Multisets , with V.Kuncak.
    Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), Edinburgh, UK. LNAI 6173, pp. 149-155.
  9. Comfusy: A Tool for Complete Functional Synthesis , with V. Kuncak, M. Mayer, P. Suter.
    Proceedings of the 22nd International Conference on Computer Aided Verification (CAV 2010), Edinburgh, UK. LNCS 6174, pp. 430-433.
  10. Complete Functional Synthesis , with V. Kuncak, M. Mayer, P. Suter.
    Proceedings of the ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation - PLDI 2010, Toronto, Canada, p. 316-329.
  11. Building a Calculus of Data Structures, with V. Kuncak, P. Suter, T. Wies.
    Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation - VMCAI 2010, Madrid, Spain. LNCS Volume 5944, p. 26-44.
  12. Collections, Cardinalities, and Relations, with K. Yessenov, V. Kuncak.
    Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation - VMCAI 2010, Madrid, Spain. LNCS Volume 5944, p. 380-395.
  13. Deciding Effectively Propositional Logic using DPLL and substitution sets, with L. de Moura, N. Bjorner.
    Journal of Automated Reasoning, DOI: 10.1007/s10817-009-9161-6, Volume 44, Number 4, p. 401-424, April 2010.
    this is an extended version of the Technical Report, MSR-TR-2008-104, August 2008.
  14. Combining Theories with Shared Set Operations (extended version), with T. Wies, V. Kuncak.
    Proceedings of the 7th International Symposium on Frontiers of Combining Systems - FroCoS 2009, Trento, Italy. Springer, LNCS Volume 5749, p. 366-382.
  15. Deciding Effectively Propositional Logic with Equality, with L. de Moura, N. Bjorner.
    Technical Report, MSR-TR-2008-181, December 2008.
  16. Fractional Collections with Cardinality Bounds, with V. Kuncak.
    Proceedings of the 17th Annual Computer Science Logic - CSL 2008, Bertinoro, Italy. Springer, LNCS Volume 5213, p. 124-138.
  17. Linear Arithmetic with Stars, with V. Kuncak.
    Proceedings of 20th International Conference on Computer Aided Verification CAV 2008, Princeton, USA. Springer, LNCS Volume 5123, p. 268-280.
  18. Decision Procedures for Multisets with Cardinality Constraints, with V. Kuncak.
    Proceedings of the 9th International Conference on Verification, Model Checking and Abstract Interpretation - VMCAI 2008, Springer, LNCS Volume 4905, p. 218-232.
  19. Verification of an Off-Line Checker for Priority Queues, with H. de Nivelle
    Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods, Koblenz, IEEE computer society press, Washington, 2005, 210-219.

Theses

  1. Decision Procedures for Program Synthesis and Verification
    PhD Thesis, École Polytechnique Fédérale de Lausanne, Lausanne, Switzerland, December 2011.
  2. Formal Correctness of Result Checking for Priority Queues
    Master Thesis, Universität des Saarlandes, Saarbrücken, Germany, February 2005.

Proceedings

  1. Ruzica Piskac, Elena Simperl: Proceedings of the Doctoral Consortium of the 3rd Future Internet Symposium 2010, Berlin, Germany, September 23-24, 2010.
  2. Frank van Harmelen, Andreas Herzig, Pascal Hitzler, Zuoquan Lin, Ruzica Piskac, Guilin Qi: Proceedings of the Workshop on "Advancing Reasoning on the Web: Scalability and Commonsense (ARea-2008)", Tenerife, Spain, June 2, 2008.
  3. Ruzica Piskac, Frank van Harmelen, and Ning Zhong: Proceedings of the First International Workshop Workshop "New forms of reasoning for the Semantic Web: scalable, tolerant and dynamic", co-located with ISWC 2007 and ASWC 2007.

Professional Activities

Program Committees

  1. 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2014)
  2. The 13th conference on Formal Methods in Computer-Aided Design (FMCAD 2013)
  3. The ESEC/FSE 2013 Tool Demonstrations Track
  4. The 22nd EACSL Annual Conference on Computer Science Logic (CSL'13)
  5. The 14th International Workshop on Verification of Infinite-State Systems (INFINITY 2012)
  6. The 3rd Workshop on Practical Aspects of Automated Reasoning (PAAR-2012)
  7. The 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18)
  8. The 4th Annual Asian Semantic Web Conference (ASWC2009)
  9. The 3rd Annual Asian Semantic Web Conference (ASWC2008)
  10. Workshop on New forms of reasoning for the Semantic Web: scalable, tolerant and dynamic (NeFors08)

Organizational Activities

  1. Education co-chair of the 3rd Future Internet Symposium 2010
  2. Organizer of ESWC-08 Workshop on Advancing Reasoning on the Web: Scalability and Commonsense (ARea2008)
  3. Organizer of the workshop on New forms of reasoning for the Semantic Web: scalable, tolerant and dynamic (NeFors07)

Managing editor of the CEUR-WS.org publishing service

Teaching

  1. lecturer for the Seminar on Decision Procedures, Winter Semester 2012, Saarland University
  2. course "Kann der Computer selbst programmieren? - Die logischen und spieltheoretischen Grundlagen der automatischen Programmsynthese", given at Frühjahrsakademie Papenburg, 2012, together with Bernd Finkbeiner
  3. lecturer at the First International SAT/SMT Solver Summer School 2011,MIT, June 2011.
  4. co-lecturer for the Seminar on Automated Reasoning, EPFL, 2010.

Students

  1. Jose A. Lopes
  2. Filip Niksic

Research Opportunities

The Synthesis, Analysis and Automated Reasoning Group has research opportunities for post-docs, PhD students, and research interns. For post-doc applications please contact me directly, and for the remaining applications please visit the Institute's career opportunities page.

Contact

Mailing address:

MPI-SWS
Campus E 1 4
D-66123 Saarbrücken
Germany

phone: +49 681 9303 8901

Email:

I am also a visiting academic in the Department of Computer Science at New York University. While there, you can find me in:
Warren Weaver Hall, room 402
Courant Institute of Mathematical Sciences
251 Mercer St.
New York, NY 10012