Ruzica Piskac

PhD Student School of Computer and Communication Sciences

email: ruzica.piskac@epfl.ch phone: +41 21 69 31221 fax: +41 21 69 36660 mailing address: Swiss Federal Institute of Technology (EPFL), School of Computer & Communications Sciences, Building BC358, Station 14, CH-1015 Lausanne, Switzerland   I am a PhD student working in the Laboratory for Automated Reasoning and Analysis under the supervision of Professor Viktor Kuncak. Curriculum Vitae Selected Publications 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. Deciding Effectively Propositional Logic with Equality, with L. de Moura, N. Bjorner. Technical Report, MSR-TR-2008-181, December 2008. 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. 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. 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. 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. Formal Correctness of Result Checking for Priority Queues Master Thesis, Universität des Saarlandes, Saarbrücken, Germany, February 2005. Selected Projects MUNCH - Automated Reasoner for Collections COMFUSY - COMplete FUnctional SYnthesis isynth - Interactive Synthesis of Code Snippets Using F# and Z3 for Inferring Congruence Equations Using Twelf for Mechanized Specification and Proofs for Reasoning about Multisets Selected Professional Activities Proceedings editor Ruzica Piskac, Elena Simperl: Proceedings of the Doctoral Consortium of the 3rd Future Internet Symposium 2010 Berlin, Germany, September 23-24, 2010. 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. 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 Organizer of ARea2008, NeFors07 Education co-chair of the 3rd Future Internet Symposium 2010 PC member of ASWC2009, ASWC2008, NeFors08 Managing editor of the CEUR-WS.org publishing service