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

I'm a tenure-track faculty at the Max Planck Institute for Software Systems (MPI-SWS) and head of the Synthesis, Analysis and Automated Reasoning Group.

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

1. 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.
2. 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.
3. 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.
4. 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.
5. 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.
6. 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.
7. 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.
8. 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.
9. 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.
10. 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.
11. Deciding Effectively Propositional Logic with Equality, with L. de Moura, N. Bjorner.
    Technical Report, MSR-TR-2008-181, December 2008.
12. 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.
13. 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.
14. 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.
15. 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.

Program Committees

1. The 14th International Workshop on Verification of Infinite-State Systems (INFINITY 2012)
2. The 3rd Workshop on Practical Aspects of Automated Reasoning (PAAR-2012)
3. The 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18)
4. The 4th Annual Asian Semantic Web Conference (ASWC2009)
5. The 3rd Annual Asian Semantic Web Conference (ASWC2008)
6. 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

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

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.

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