logo epfl

    Ruzica Piskac

Ecole Polytechnique Fédérale de Lausanne

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 BC343,
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

  1. T. Wies, R. Piskac, V. Kuncak. Combining Theories with Shared Set Operations. To appear in Proceedings of the 7th International symposium on frontiers of combining systems (FroCoS 2009) [extended pdf]
  2. R. Piskac, L. de Moura, N. Bjorner. Deciding Effectively Propositional Logic with Equality, Technical Report, MSR-TR-2008-181, December 2008. [pdf]
  3. L. de Moura, R. Piskac, N. Bjorner. Deciding Effectively Propositional Logic using DPLL and substitution sets, Technical Report, MSR-TR-2008-104, August 2008. [pdf]
  4. R. Piskac, V. Kuncak. Fractional Collections with Cardinality Bounds. Proceedings of 17th Annual Computer Science Logic - CSL 2008, Bertinoro, Italy. Springer, LNCS Volume 5213, p. 124-138. [pdf]
  5. R. Piskac, V. Kuncak. Linear Arithmetic with Stars. Proceedings of 20th International Conference on Computer Aided Verification CAV 2008, Princeton, USA. Springer, LNCS Volume 5123, p. 268-280. [pdf]
  6. R. Piskac, V. Kuncak. Decision Procedures for Multisets with Cardinality Constraints. Proceedings of The Ninth International Conference on Verification, Model Checking and Abstract Interpretation - VMCAI 2008, Springer, LNCS Volume 4905, p. 218-232. [pdf]
  7. H. de Nivelle, R. Piskac. Verification of an Off-Line Checker for Priority Queues. Proceedings of Third IEEE International Conference on Software Engineering and Formal Methods, Koblenz, IEEE computer society press, Washington, 2005, 210-219. [pdf]
  8. R. Piskac. Formal Correctness of Result Checking for Priority Queues. Master Thesis, Universität des Saarlandes, Saarbrücken, Germany, February 2005. [pdf]

Selected Projects

  1. Theorem Proving
  2. Using F# and Z3 for Inferring Congruence Equations
  3. Using Twelf for Mechanized Specification and Proofs for Reasoning about Multisets

Selected Professional Activities