Bilateral research project

The Faculty of Mathematics, within the group for Automated Reasoning (http://argo.matf.bg.ac.rs), implemented a bilateral research project "Decision Procedures: from Formalization to Applications", funded (under the label IZ73Z0_1 27 979) Foundation SNSF SCOPES within the program. The holder of the project is prof. Victor Kuncak (EPFL, Lausanne, Switzerland, http://lara.epfl.ch/~kuncak/), and coordinator for a partner from Serbia is Associate. prof. Predrag Janicic (Faculty of mathematics, Belgrade, http//www.matf.bg.ac.rs/~janicic). The project runs from 11/01/2009. to 31.10.2012.

The focus of the project is decision-making procedures - algorithms for a formula that certain theories can examine whether or not the theorem. Decision-making procedures have many applications in software and hardware verification in VLSI design, relational databases and so on. The project is improving existing and develop new procedures for deciding SAT (propositional satisfiability problem), SMT (satisfiability in relation to the theory) and fragments of Euclidean geometry and working on their applications.

Swiss National Science Foundation (The Swiss National Science Foundation - SNSF, http://www.snf.ch), established 1952. is the most important Swiss Agency for the Advancement of Science. It helps all scientific disciplines with the support of the Swiss federal government.

SCOPES Program, funded by the SNSF (together with the Swiss Agency for Development and Cooperation (Swiss Agency for Development and Cooperation - SDC) supports the collaboration between research groups in Switzerland and Eastern Europe. In the period 2009-2012. by means of the program  16 projects are funded with groups of participants from Serbia.

http://www.snf.ch/E/international/europe/scopes/Pages/currentprojects.aspx