Academic year 2016/17

Razvojem novih detektora, napretkom informacionih i komunikacionih tehnologija, moderna nauka se menja i prelazi iz faze retkih podataka u fazu sa intenzivnim podacima. To podrazumeva i promenu naučne paradigme i načina kako se pristupa i analiziraju podaci. Da bi se tsunami podataka koji nam predstoji uspešno koristio, neophodno je razviti nove metode za analizu (statistika, machine learning, information extraction...)

Large synoptic Survey Telescope je potpuno novi koncept u astronomiji, sa idejom da se celokupni vidljivi deo neba sa vrha planine u Čileu, skenira teleskopom prečnika 8,6 metara približno dva puta nedeljno. To je moguće postići velikim vidnim poljem teleskopa - prečnika sedam vidljivih prečnika Meseca i najveće, ikad napravljene, astronomske kamere od 3,2 gigapixela Projekat će omogućiti kompletno mapiranje Sunčevog sistema, popisa skoro svih zvezda u našoj galaksiji, otkrića i proučavanja promenljivih zvezda i eksplozija u vasioni do karakterizacije tamne materije, tamne energije i kosmologije.

LSST softver će moći da obradi i analizira ogromnu količinu podataka svake noći i da astronomima u realnom vremenu prosledi upozorenja za bilo kakve promene (pozicija, sjaj) koje se dese na nebu. Osim toga planira se godišnje publikovanje kataloga svih objekata (reprocesiranjem svih snimaka od početka projekta). Očekujemo detekciju i karakterizaciju oko 40 milijardi astronomskih objekata (prvi puta ćemo imati zabeleženo više nebeskih objekata nego što ima stanovnika na našoj planeti.)

Izgradnja teleskopa je kompletirana oko 40 odsto. Završetak se očekuje krajem 2019. a posle toga sledi skoro tri godine testiranja i kalibracije instrumenata i završetak kamere. Pravi početak prikupljanja astronomskih podataka će biti krajem 2022. godine, a radna faza će trajati barem deset godina - dakle do 2032-2033. godine

Srpski deo tima čine kolege sa Astronomske opservatorije, Matematičkog fakulteta, FON-a i PMF-a u kragujevcu. Interes našeg tima je u razvoju softvera za LSST (trenutno razvijamo simulator alerata), razvoju metoda i softvera za analizu big data u astronomiji, razvoju potpuno nove discipline proučavanja tamne energije, vangalaktička astronomija. Postoji mogućnost uključivanja u naše projekte, a njih će biti sve više i biće raznorodniji, kako se približavamo početku aktivnog sakupljanja podataka.

Proizvodnja softvera je disciplina koja počiva na matematičkoj logici, a podrazumeva posedovanje jos mnogo matematičkih i informatičkih oblasti znanja. Međutim, iako u korenu ima vekovima razvijanu, po mnogima savršenu teoriju, često se događa da rezultat bude daleko od savršenog. Šta to muči današnje informatičare? Kako se što više približiti savršenom ili očekivanom rezultatu?

Ova prezentacija će mladim kolegama prikazati kakva je uloga ITja u kompanijama koje brzo napreduju i rastu, kao što je Generali Osiguranje Srbija. Kroz primere iz naše prakse pokušaćemo da prikažemo koliko različitih matematičkih ali i društvenih teorija je potrebno savladati da bi proces proizvodnje softvera dao dobar retutat. Predavanje će obuhvatati tri ključne oblasti: organizaciju podataka, projektovanje i implementacija korisničkog zahteva i sisteme izveštavanja. Kako su ovo najčešći procesi koje IT prati i unapređuje, tu imamo i najviše znanja i iskustva koje možemo da podelimo sa mladim kolegama.

Prezentacija se odnosi na sledeće teme: Šta implementacija novih poslovnih rešenja donosi kao promene u celokupnoj organizaciji, Opasnosti i rizici koje vrebaju pri implementaciji, Potrebni nivoi upravljanja, Ključni principi pre početka implementacije, Kontrola kvaliteta tokom implementacije.

PlanetLab (www.planet-lab.org) is a global research network with the main purpose to support experimental research in the Internet. PlanetLab consists of about 1000 Linux servers at 700 geographically different sites. The servers are accessible by remote login and the users can run their own experimental software on them.

Biography: Dan Komosný is an associate professor at the Department of Telecommunications, Brno University of Technology, the Czech Republic. He received his Ph.D. degree in Teleinformatics in 2003. His research is focused on cyber geography and cyber security. He leads courses dealing with IP networks and network operating systems.

U predavanju će biti predstavljena analiza problema i razvoj novih tehnika za rešavanje uobičajenih problema koji nastaju prilikom implementacije asinhronih softverskih sistema, poput eksplicitne sinhronizacije konkurentnih procesa preko muteksa i transakcione memorije, razbijanja programa na delove koji nisu logičke pod-celine zbog izvrtanja kontrole izvršavanja (IoC -- Inversion of Control) koju je neophodno koristiti prilikom implementacije asinhronih sistema, kao i životnog veka korišćenih podataka u konkurentnim procesima.

Biće predstavljen metod rešavanja problema izvrtanja kontrole zasnovan na apstrakciji monade nastavka. Ovaj metod bi trebalo da nam omogući da implementiramo logiku sistema bez osvrtanja na potrebu da se delovi izvršavaju asinhrono i, samim tim, bez potrebe za razbijanjem programa na delove koji nisu logičke pod-celine. Na ovaj način bi se izvrtanje kontrole u potpunosti sakrilo i programeru bi se omogućilo da piše uobičajen (sinhroni) funkcionalan ili imperativan kod, dok se sve asinhrone operacije izvršavaju "iza scene".

Takođe, u planu je da se pokaže da ovaj pristup, uz korektan dizajn softverskog sistema, u potpunosti eliminiše potrebu za eksplicitnom upotrebom sinhronizacionih primitiva poput muteksa i transakcione memorije, kao i da je staranje o životnom veku promenljivih korišćenih prilikom implementacije sistema trivijalno implementirati bez potrebe za eksplicitnim oslobađanjem (što je uobičajeno za programske jezike C i C++), ali i bez potrebe za naprednim sakupljačima otpadaka (što je uobičajeno za većinu funkcionalnih programskih jezika, i jezika koji se izvršavaju na virtuelnim mašinama poput jezika Java i C#).

Razvoj računara je došao do nivoa da su računari sveprisutni. Većina stanovnika razvijenog sveta poseduje lični računar, ali i pametni telefon, tablet, možda i laptop. Ono što izmiče velikoj većini je da su računari ušli u skoro sve uređaje oko nas: avione, brodove, automobile, kućne aparate, liftove, fabrike, elektrane, itd. Upravo je oblast embeded razvoja jedna od najaktivnijih i najbogatijih u pogledu dostupnog hardvera, operativnih sistema, komunikacionih protokola i primene.

Više nego u bilo kojoj drugoj oblasti računarskog razvoja, istovremeno se sukobljavaju zahtevi za brzinom, vremenskom predvidljivošću, uštedom energije, malim dimenzijama i jeftinim komponentama. S druge strane, od savremenog embeded programera se očekuje da odlično poznaje Linuks, kako sa korisničke, tako i sa kernelske strane,te C, C++ i Bash, mrežne protokole, da bude u stanju da rekonstruiše kernel i fajl sistem, i još mnogo toga.

Predavanje je usredsređeno na kratak uvod u izazove u embeded razvoju, kako iz ugla samog hardvera, tako i iz ugla dostupnog softvera i različitih ograničenja. Osvrnućemo se i na ulogu Linuksa u embeded razvoju, te i na trendove koji prate razvoj Linuks kernela u poslednjih nekoliko godina. Posebnu pažnju ćemo posvetiti primerima iz iskustva, koji pobliže opisuju mogućnosti Linuksa i opravdavaju njegov izbor kao dominantog operativnog sistema u embeded svetu.

Rad na projektu često zahteva saradnju vise osoba, što nameće pitanje organizacije. Svaki put kada pravimo odredjenu organizacionu strukturu, donosimo odluke. Ova radionica ima za cilj da objasni potrebu za tim odlukama kao i razloge zbog kojih odluke treba da vode ka nekoj od vec postavljenih i isprobanih struktura.

Dva modela rada koja su ovde obrađena su Tim i Radna Grupa. Tim je prirodno okruženje u sredinama u kojima ljudi imaju svest o samoorganizaciji, i naklonjeniji su redovnoj saradnji, karakteriše ga visok stepen komunikacije i kolektivno vlasništvo nad projektom, kao i pojedinačnim zadacima. Potreba za vođstvom postoji u timu, ali to vođstvo ima implicitni autoritet.

Radna grupa predstavlja skup ljudi sa istim ciljem. Pored glavnog cilja pojedinci mogu imati i lične ciljeve. Podela zadataka unutar projekta je strožija i ponekad je potrebno jasno i čvrsto vođstvo. Kultura predaje štafete, integracije, i kontrole je svojstvena za radne grupe. Svako ima svoje zone odgovornosti, ili jasnu listu zadataka i rokova. Postavljamo pitanje kako se biraju ljudi za tim, a kako za radnu grupu. Na šta je bitno obratiti pažnju, i kako u praksi funkcionišu all star timovi?

Na kraju pričamo o unapređenja procesa u oba modela. Načinu praćenja i sinhronizacije ili davanja izveštaja unutar izabranog modela. Takođe posmatramo i dinamiku izgradnje, vreme koje je potrebno dok se postignu performanse unutar modela i dugoročnost jedne i druge strukture.

Sve veći izazovi u poslovanju s kojima se susreću kompanije u oblasti Finansija i Upravljanja rizicima diktiraju konstantne inovacije u IT industriji i potrebu za softverskim rešenjima koja:

• Imaju mogućnost da podrže veliku količinu podataka obrađenu u realnom vremenu;
• Mogu da generišu pravovremene finansijske rezultate za donošenje strateških odluka;
• Imaju utvrđene kontrole i pravila za različite računovodstvene principe izveštavanja i regulativu solventnosti.

SAP kompanija je lider u inovacijama, kada je u pitanju poslovni softver, koja nudi integrisana i moderna softverska rešenja kombinujući znanja i veštine iz oblasti informacionih tehnologija sa finansijama, upravljanjem rizicima i investicijama. Rešenja koja SAP nudi zasnovana su na SAP HANA platformi koja omogućava transakciono, analitičko i kombinovano procesiranje sa visokim performansama.

Tokom ovog izlaganja biće prikazane prednosti SAP softverskih rešenja na HANA platformi, kao i izazovi sa kojima se kompanije u osiguravajućoj i bankarskoj industriji suočavaju. Neke od njih su računovodstvene regulative, regulative solventnosti, integrisanje aktuarskih proračuna, praćenje i predviđanje prihoda i troškova, kao i kompleksni poslovni procesi. Takođe, biće prikazana dva inovativna SAP-ova rešenja: Insurance Analyzer i Cost and Revenue Allocation for Financial Services. Ova rešenja su inovacije u industriji osiguranja i bankarstva, ali mogu biti lako primenjiva i u ostalim industrijama. Cilj prezentacije bi bio da prikažemo prednosti inovacija u današnjem poslovanju osvrćući se na primere iz prakse, stečene tokom implementacije ovih rešenja.

Insurance Analyzer je softversko rešenje koje omogućava osiguravajućim kućama i bankama da poštuju različite računovodstvene principe i principe solventnosti u svom poslovanju; kao što su IFRS 17, US GAAP, US Statutory Accounting Principles, Solvency II, Risk Based Capital i drugi.

SAP-ovo rešenje Cost and Revenue Allocation služi za izvršavanje različitih kalkulacija kao što su predračuni, alokacije ili raspoređivanje prihoda i troškova, valuacije vrednosti novca, stohastičke kalkulacije i integracija sa R programskim jezikom. Predviđanje budućih prihoda i troškova su jedna od najbitnijih stavki radi održavanja i unapređenja poslovnih procesa jednog preduzeća, podržana različitim simulacijama, “what if” analizama i stress testiranjem.

Oba SAP-ova rešenja omogućavaju transparentnost podataka na svim nivoima poslovanja jedne kompanije, počevši od najvišeg do najnižeg nivoa. Razvijena su kao nezavisna rešenja, ali se mogu integrisati sa drugim bazama podataka, sa postojećim SAP-ovim modulima kao i sa rešenjima drugih kompanija. Podržavaju kako kvantitativnu tako i kvalitativnu proveru podataka sistema prilikom učitavanja u jedno od ova dva rešenja.

Predavanje je koncipirano tako da studentima pruži priliku da razumeju brojne izazove na tržištu sa kojima se kompanije u industriji Finansija i Upravljanja Rizicima susreću, kao i priliku da se upoznaju sa SAP aplikacijama koja odgovaraju na ove potrebe tržišta osvrćući se na tehničke mogućnosti i primere iz prakse.

In this talk we will give an overview of the GeoCoq library developed by our team in Strasbourg (http://geocoq.github.io/GeoCoq/). GeoCoq library contains a systematic development of geometry from Tarski’s or Hilbert’s axioms. From these axiom systems, we formalized the culminating results of both Tarski, Schwabhäuser, Szmielew, Metamathematische Methoden in der Geometrie and Hilbert, Foundations of Geometry, namely the arithmetization of geometry. This connection between synthetic geometry and algebra, allows us to use algebraic methods for automated deduction in geometry in a synthetic setting. We have also studied the formal proof of the equivalence between 34 versions of the parallel postulates. We work in neutral geometry in an intuitionistic setting and study the impact of different continuity properties on the equivalence proofs. This result in four groups of postulates, which are all equivalent assuming Archimedes’ axiom but distinct, in constructive logic without Archimedes’ axiom.

Finally, I will report our ongoing work toward the formalization of Euclid’s Elements proposition in Coq.

Fazi logika predstavlja matematički aparat koji omogućava rad sa raznovrsnim informacijama koje ne mogu precizno da se izraze uz pomoć klasične logike i teorije klasičnih skupova. Podobnost fazi logike za predstavljanje neizvesnih, nepreciznih i nesigurnih informacija, doprinosi njenoj sve široj primeni.

Matematička optimizacija je oblast u preseku računarstva i matematike sa širokim spektrom primene. Klasa problema rutiranja vozila (engl. Vehicle Routing Problems– VRPs), koja predstavlja uopštenje problema trgovačkog putnika, jedna je od poznatijih klasa problema kombinatorne optimizacije. Posebno značajno mesto među često proučavanim problemima matematičke optimizacije imaju lokacijski problemi. Predmet izlaganja biće analiza i rešavanje tri NP-teška problema: problem rutiranja vozila sa ograničenim rizikom (engl. Risk-constrained Cash-in-Transit Vehicle Routing Problem - RCTVRP), problem ravnomernog opterećenja (engl. Load Balancing Problem - LOBA) i problem maksimizacije minimalnog rastojanja (engl. Max-Min Diversity Problem - MMDP).

Metaheuristike predstavljaju generalizovane strategije računarske inteligencije koje se često koriste za rešavanje NP-teških optimizacionih problema. U okviru izlaganja biće prikazana metoda GRASP (engl. Greedy Randomized Adaptive Search Procedure), kao i metoda ponovnog povezivanja puta (engl. Path relinking - PR) za rešavanje problema RCTVRP, LOBA i MMDP. GRASP je metaheuristička metoda koja se sastoji od višestrukog pokretanja lokalne pretrage nad početnim rešenjima dobijenim primenom neke pohlepne heuristike. PR predstavlja način pretraživanja trajektorija (putanja) između dobrih rešenja. Glavna ideja ove metode je pretpostavka da dobra rešenja imaju neke zajedničke karakteristike, tako da se kretanjem po trajektoriji između dva dobra rešenja prolazi kroz rešenja koja su potencijalno bolja.

Fazi logika će biti primenjena u dva različita aspekta: prilikom modeliranja problema i prilikom rešavanja problema metaheuristikama. S obzirom da mnogi problemi iz realnog sveta sadrže različite vrste nepouzdanosti, potreban je matematički, formalan način koji će omogućiti da se precizno kreiraju matematički modeli koji će odgovarati tim problemima. U toku izlaganja biće predloženi novi modeli razmatranih problema koji uz pomoć korišćenja fazi logike bolje opisuju realne situacije. Pored toga, biće predstavljene neke mogućnosti upotrebe fazi logike za poboljšanje performansi predloženih metaheurističkih metoda za rešavanje razmatranih problema.

Diskretna matematika je oblast matematike koja se bavi proučavanjem matematičkih objekata koji su diskretni, odnosno objekata koji se sastoje od različitih ili nepovezanih elemenata. Za razliku od realnih brojeva objektima diskretne matematike mogu se dodeliti zasebne celobrojne vrednosti. Diskretna matematika se koristi kad god se broje objekti, kada se proučavaju odnosi između konačnih skupova, kao i kada postupak podrazumeva konačan broj koraka za analizu. Glavni razlog porasta značaja diskretne matematike, počev od sredine dvadesetog veka je ta što se često podaci diskretne matematike mogu skladištiti i njima rukovati pomoću računara. Pojmovi i obeležavanje iz diskretne matematike su značajni za proučavanje i opis objekata i problema iz raznih oblasti računarskih nauka, poput kompjuterskih algoritama, programskih jezika, razvoja softvera, kriptografije i automatskog dokazivanja teorema. Među najviše korišćenim matematičkim objektima koji potpadaju pod diskretnu matematiku nalaze se celi brojevi, skupovi, grafovi i matrice. Diskretna matematika se pojavila na univerzitetskim programima početkom 80-ih godina prošlog veka, kao kurs u okviru programa računarskih nauka. Od tada je popularnost ove oblasti znatno porasla, tako da se diskretna matematika, pored mnogih univerziteta, proučava i u određenom broju srednjih škola.

Konstruktivni pristup je veoma čest u rešavanju problema iz diskretne matematike. Među poznatijim primerima je svakako rešenje problema ćetiri boje (Four Color Problem). Ovaj problem, postavljen 1852. godine, tvrdi da je dovoljno četiri ili manje boja da bi se izvelo bojenje regiona bilo koje mape, tako da svaka dva regiona koji dele zajedničku granicu budu obojena različitom bojom. Dokaz koji su Apel (Appel) i Haken (Haken) izveli 1976. godine sastoji se od konstrukcije neizbežnog skupa od 1936 svodljivih konfiguracija. Kao posledica izvodi se zaključak da ne postoji minimalni protivprimer grafa za čije bojenje je potrebno više od četiri boje. U izvođenju dokaza da graf neizbežno sadrži neku od svodljivih kofiguracija neophodna je pomoć raqunara, što dokaz problema četiri boje čini jednim od prvih dokaza potpomognutih računarom (computer-aided proof).

Nešto drugačija veza konstruktivnog pristupa i računara je mogućnost programske implementacije jasno definisanih konstruktivnih algoritama. Na ovaj način se, pored dokaza zadovolivosti određenog svojstva, može efektivno dobiti primer objekta sa traženim svojstvima.

Proučavanje raznih tipova bojenja grafova, poput bojenja čvorova, bojenja grana, totalnog bojenja, i raznih varijacija bojenja grafova. Među njima su valjana bojenja, indukovana bojenja, čvor-razlikujuća, kao i sused-razlikujuća bojenja. Pored hromatske teorije grafova, obrađuju se problemi iz Bulove teorije matrica, kao i Franklova hipoteza iz teorije skupova.

Metode za dobijanje poboljšanja u odnosu na poznate rezultate obuhvataju:

1. Konstrukcije grafova sa odgovarajućim karakteristikama.
2. Opis kako rekurzivnih tako i nerekurzivnih algoritama koji obezbe]uju bojenje grafa uz korišćenje minimalnog broja različitih boja.
3. Dokazivanje ispravnosti algoritama, ;esto korišćenjem matematičke indukcije. Dokazivanje nepostojanja minimalnog protivprimera sa određenim karakteristikama.
4. Dokazivanje teorema iscrpljivanjem mogućnosti ili analizom slučajeva, bilo uz pomoć računara ili klasičnim pristupom.

Terminologija, kao sistem naziva, odnosno termina u nekoj naučnoj oblasti ima podjednako važno mesto kako kod lingvista, tako i kod stručnjaka različitih specijalizovanih oblasti. U okviru izlaganja biće predstavljen proces razvoja terminoloških resursa koji se bazira na domenski specifičnim korpusima: od prikupljanja građe za izradu korpusa preko primene leksičkih resursa i ručne evaluacije do željene dopune morfoloških rečnika. Biće predstavljena i koncepcija terminološke baze, funkcije softverskog rešenja, trenutni sadržaj, mogućnosti razmene podataka i veza sa digitalnim bibliotekama. Praćenje verzija i razvojni tok terminološke odrednice će biti komentarisan iz teorijskog i praktičnog aspekta. Uz konkretan prikaz procesa razvoja, daće se osvrt i na pojedine standarde iz grupe ISO TC37 koji se odnose na terminologiju.

Drugi deo prezentacije se odnosi na rešavanje problema usvajanja podesnih prevoda stranih termina, što je, opet, samo po sebi, jezički osetljiv i izazovan zadatak. U okviru kursa Programiranje za veb na master studijama modula Informatika razvijena je aplikacija koja ima za cilj sumiranje internih dogovora, jezičkih smernica i pravila, kao i olakšanu diskusiju po pitanju usvajanja preferiranih termina. Zamisao je da rezultujuća baza termina bude javno dostupna i pretraživa po oblastima i da posluži kao podrška u procesu pisanja, prevođenja ili pretraživanja informacija.

U ovoj disertaciji razmatrana su tri NP-teška problema diskretne optimizacije sa funkcijom cilja tipa min-max: višeperiodni lokacijski problem za rasporedivanje jedinica za reagovanje u hitnim slučajevima, dinamički lokacijski problem maksimalnog pokrivanja sa više poluprečnika, i problem p-hab centra neograničenih kapaciteta sa višestrukim alokacijama. Kako u situacijama u praksi ulazni podaci (zahtevi korisnika, cena ili vreme transporta) često variraju po nepoznatim raspodelama, u razmatrane determinističke varijante problema je uključena nepouzdanost ulaznih podataka koristeći pristup robusne optimizacije. Razvijeni su matematički modeli za odgovarajuće determinističke i robusne varijante problema, osim u slučaju determinističke varijante problema p-hab centra neograničenih kapaciteta sa višestrukim alokacijama, koja je već razmatrana u literaturi. Dodatno, za lokacijski problem rasporedivanja jedinica za reagovanje u hitnim slučajevima, prvi put u literaturi je dokazano da je NP-težak.

Razmatrani problemi i njihove robusne varijante imaju veliki praktični značaj, imajući u vidu brojne oblasti primene, kao i da razmatrana nepouzdanost ulaznih parametara odgovara čestim situacijama u praksi. Višeperiodni lokacijski problem za rasporedivanje jedinica za reagovanje u hitnim slučajevima nalazi primenu u optimalnom rasporedivanju stanica hitne pomoći, policijskih i vatrogasnih jedinica ili drugih jedinica hitnih službi u okviru odredene oblasti. Dinamički lokacijski problem maksimalnog pokrivanja sa više poluprečnika pomaže pri optimalnom odabiru lokacija za izgradnju resursa (fabrika, uslužnih centara, službi hitne pomoći, i sl.), koji bi maksimalno zadovoljili potrebe stanovništva neke oblasti, pri čemu udaljenost resursa do korisnika (odabrani poluprečnik pokrivanja) direktno utiče na efikasnost snabdevanja. Problem p-hab centra neograničenih kapaciteta sa višestrukim alokacijama ima značajne primene pri optimizaciji telekomunikacionih sistema, sistema isporuke poštanskih i drugih pošiljaka, hitnih službi, sistema snabdevanja, itd.

Kako egzaktne metode mogu rešiti samo instance problema manjih dimenzija, razvijeni su hibridni algoritmi za rešavanje determinističkih i robusnih varijanti razmatranih problema. Predloženi algoritmi su dobijeni kombinovanjem optimizacije rojem čestica i dva algoritma zasnovana na lokalnom pretraživanju – klasične lokalne pretrage i metode promenljivih okolina. Za problem dinamičkog lokacijskog problema maksimalnog pokrivanja sa više poluprečnika, izvršena je hibridizacija metaheuristike sa egzaktnom metodom zasnovanom na linearnom programiranju. Svi elementi predloženih hibridnih algoritama su prilagodeni osobinama razmatranih problema. Pri- menjene su razne strategije za ubrzanje predloženih algoritama, posebno pri računanju funkcije cilja i heuristika lokalnog pretraživanja. Detaljno je analiziran uticaj različitih vrednosti parametara hibridnih algoritama na kvalitet dobijenih rešenja. Adekvatne vrednosti značajnih paramatara su odredene analizom varijanse.

Za svaki od razmatranih problema (za determinističku i robusnu varijantu), izvršena su testiranja predloženih hibridnih algoritama na odgovarajućim instancama i eksperimentalna poredenja sa postojećim algoritmima iz literature ili egzaktnim metodama koje su ugradene u rešavač CPLEX. Dobijeni eksperimentalni rezultati ukazuju na efikasnost predloženih algoritama pri dobijanju visoko kvalitetnih rešenja. Na osnovu rezultata poredenja sa postojećim metodama za rešavanje razmatranih problema, mogu se uočiti prednosti predloženih hibridnih algoritama u smislu kvaliteta rešenja i/ili brzine izvršavanja, što se posebno ogleda u slučaju instanci problema većih dimenzija. Rezultati prikazani u ovoj disertaciji predstavljaju doprinos oblastima diskretne optimizacije, robusne optimizacije i metaheurističkih metoda.

Bioinformatika je mlada i izuzetno dinamična oblast koja stoji na preseku statistike, informatike i biologije. Uključuje analizu i modeliranje velikih podataka, kao i razvoj novih algoritama. Cilj predavanja je predstavljanje ključnih pojmova oblasti, aktuelnih problema i mnogobrojnih izazova bioinformatike. Kroz par primera objasnićemo biološku i inženjersku složenost oblasti, kao i primenu bioinformatike u savremenoj nauci. Prikazaćemo jednu od ključnih primena iz oblasti personalizovane medicine, gde izučavanje genoma i promena u njemu utiče na efikasnije lečenje. Osvrnućemo se na značajan izazov intenzivnog rasta količine bioinformatičkih podataka i zahteva za razvoj efikasnih rešenja za analizu, prenos i čuvanje istih.

Kompanija Seven Bridges okuplja najveći bioinformatički tim u regionu i zajedno sa kolegama iz drugih kancelarija radi na velikim internacionalnim projektima koji imaju za cilj da identifikuju uzročnike raka, genetskih oboljenja i da razviju lekove koji bi preciznije i uspešnije tretirali te bolesti.

Korisni linkovi:
Ako želite da se više informišete o ovoj oblasti i pročitate iskustva bioinformatičara, pogledajte ovaj članak: Saveti bioinformatičara kako i zašto ući u ovu oblast, Startit članak. Takođe slikovit opis, kako bioinformatika može da promeni kurs medicine, pogledajte ovde: Kako bioinformatika može da promeni kurs medicine, NewYorker.com

Više o kompaniji:
Seven Bridges, kompanija koja je 2016. imenovana za jednu od najpametnijih svetskih kompanija od strane MIT Technology Review-a, bavi se analizom biomedicinskih podataka, pospešujući proboje u istraživanju raka, genetskih oboljenja, razvoja lekova i personalizovane medicine. Naš proizvod, skalabilna Seven Bridges Cloud platforma omogućava brzu, zajedničku analizu genoma paralelno sa ostalim formama biomedicinskih podataka. Istraživači u državnim, biotehnološkim, farmaceutskim i akademskim laboratorijama širom sveta koriste usluge Seven Bridges-a, uključujući i tri značajne inicijative iz oblasti genomike: Cancer Genomics Cloud Pilot (U.S. National Cancer Institute), Million Veteran Program (The Veterans Affairs Office of Research and Development) i 100,000 Genomes Project (Genomics England). Seven Bridges ima kancelarije u Beogradu, Bostonu, Londonu, Istanbulu, Ankari i San Francisku.

Problem zadovoljivosti u odnosu na teoriju (eng. Satisfiability Modulo Theory (SMT)) je problem ispitivanja da li postoji model neke unapred zadate teorije prvog reda u kome je data formula tačna. Softverski alati koji implementiraju procedure za rešavanje SMT problema zovu se SMT rešavači. Ovi alati se danas dominantno koriste u verifikaciji softvera. Zbog toga su tipične teorije koje se razmatraju u SMT-u prilagodjene upravo toj vrsti primene (teorija jednakosti sa neinterpretiranim funkcijskim simbolima, linearna aritmetika, teorija bitvektora, teorija nizova, itd.). U okviru ove teze razmatrani su pristupi za unapređivanje SMT rešavača. Jedan pravac unapređivanja SMT rešavača je definisanje novih SMT teorija. Ugradnja procedura odlučivanja za nove teorije u postojeće SMT rešavače omogućila bi širu primenjivost SMT tehnologija u rešavanju problema iz drugih oblasti. Jedna takva primena je rešavanje problema zadovoljavanja ograničenja (eng. Constraint Satisfaction Problem (CSP)). Postojeće SMT teorije nisu prilagođene rešavanju ovakvih problema, jer su CSP problemi po pravilu definisani nad konačnim domenima, dok tipične SMT teorije podrazumevaju beskonačne domene. Takođe, standardne SMT teorije nemaju mogućnost korišćenja globalnih ograničenja u formulaciji CSP problema, kao ni mogućnost rezonovanja o globalnim ograničenjima. Zbog toga je u okviru ove teze formulisana nova SMT teorija koja definiše sintaksu i semantiku nekih najčešćih globalnih ograničenja (pre svih ograničenja uzajamne različitosti, engl. alldifferent), a zatim je za takvu teoriju razvijena procedura odlučivanja koja je ugrađenja u DPLL(T) zasnovan SMT rešavač. Ova procedura je zasnovana na postojećim CSP tehnikama, pri čemu su te tehnike prilagođene SMT kontekstu i po potrebi proširene i unapređene. Na ovaj način smo u okviru SMT-a objedinili dobre strane SAT rešavača (efikasnost pretrage) i CSP rešavača (algoritmi prilagođeni globalnim ograničenjima). Za alldifferent ograničenje osmišljen je novi algoritam za generisanje objašnjenja konflikata i propagacija. Za linearno ograničenje osmišljen je novi poboljšani algoritam filtriranja koji koristi informacije o postojećim alldifferent ograničenjima u datom problemu za postizanje jačeg nivoa konzistentnosti. Za sve predložene algoritme i tehnike u okviru ovog dela teze data je i opsežna eksperimentalna evaluacija. Drugi skup tehnika kojima se SMT rešavači mogu unapređivati su tehnike paralelizacije, pre svega zahvaljujući ubrzanom razvoju višejezgarnih procesora koji su danas već uveliko dostupni. Tipični pristup u paralelizaciji SMT rešavača je tzv. paralelni portfolio, gde se više različito podešenih instanci rešavača pokreću istovremeno nad istom instancom problema, dok neka od njih ne pronađe rešenje. Alternativni pristup je paralelizacija vremenski zahtevnih algoritama u okviru procedura odlučivanja ugrađenih u SMT rešavače. U okviru ove teze implementiran je paralelni portfolio, a urađena je i paralelizacija simpleks procedure koja se u SMT-u koristi za ispitivanje zadovoljivosti u teoriji linearne aritmetike. Ova procedura je jedna od vremenski najzahtevnijih procedura u SMT-u, zbog čega je bilo očekivano da će njenom paralelizacijom doći do značajnog ubrzanja rada rešavača. Urađena je i opsežna eksperimentalna evaluacija navedenih pristupa paralelizaciji na velikom skupu, kako slučajno generisanih, tako i industrijskih instanci. Rezultati evaluacije prikazani u tezi govore u prilog paralelnom portfoliju, ali takođe pokazuju i značajne rezultate kada je u pitanju paralelizacija simpleksa. Takođe je evaluiran i hibridni pristup koji je takođe u nekim slučajevima dao dobre rezultate.

Preciznost prediktivnih alata može biti iskorišćena kao komparativna prednost i kao tajno oruđe za donošenje ispravnih poslovnih odluka. Integracijom korisničkih podataka sa različitih sistema omogućava se kreiranje personalizovanih ponuda i predviđaju buduće potrebe korisnika korišćenjem prediktivne analitike, čime se ostvaruju ključni benefiti digitalne transformacije za naše klijente:

• Optimzacija marketinških i prodajnih aktivnosti
• Optimizacija logistike i nabavke
• Povećanje podaje
• Poboljšanje odnosa sa kupcima: povećanje lojalnosti brendu i smanjenje churn-a
• Razvijanje poslovanja: proširenje na nova tržišta i oblasti poslovanja
• Smanjenje operativnih troškova

IMPOQO: Impoqo predstavlja personalizovano, tailor made, smart eCommerce rešenje prilagođeno potrebama klijenata u okviru različitih grana industrije. Pažljivo kreirano eCommerce iskustvo doprinosi boljem korisničkom iskustvu, povećava korisničko zadovoljstvo, poverenje u brend, a samim tim i utiče na povećanje prodaje naših klijenata. Za Impoqo, personalizacija se ogleda u individualanom pristupu- mogućnosti da se u realnom vremenu isporuče relevantna, kontekstualna digitalana iskustva u svakom trenutku zavisno od potreba korisnika.

GEOTELEMARK: Geotelemark je softversko rešenje za poslovnu, georeferenciranu analitiku. Osnovni zadatak Geotelemarka je da prikupi, objedini, analizira i, kao rezultat, prikaže na mapi veliku količinu raznorodnih, georeferenciranih, podataka (podaci o različitim tipovima infrastrukture‚ komercijalne i demografske podatke iz više različitih izvora: Inventory, CRM, različita istraživanja tržišta, zavod za statistiku, geodetski zavod, hidrometeorološki zavod i dr.) Intuitivnost u radu sa georeferenciranim podacima, u kombinaciji sa snažnom analitikom omogućavaju uočavanje veza koje nije moguće zapaziti kada su podaci prikazani u tabelarnoj formi. Ova osobina Geotelemarka odvaja ga od standardnih BI rešenja. Detaljnije podatke o svemu možete videti na našem sajtu www.geotelemark.com.
Geotelemark i Impoqo omogućavaju prediktivne uvide kako bi se korisnici bolje razumeli i maksimizovala CLV (customer lifetime value).

На предавању ће студенти сазнати како изгледа свакодневни посао софтверског инжењера у великој компанији Google. На крају предавања биће речи о Google-овом програму студентских пракси, процесу интервјуисања и запошљавања итд. Google поседује широк спектар пракси и послова и презентација је прилагођена свима, те су добродошли сви студенти. Поред предавача, на предавању ће учествовати и Никола Јовановић (студент МатФ-а који је ове године био на пракси у Google-у).

Mnogi realni problemi se danas mogu predstaviti u obliku problema zadovoljenja ograničenja (CSP) i zatim rešiti nekom od mnogobrojnih tehnika za rešavanje ovog problema. Jedna od tehnika podrazumeva svođenje na problem SAT, tj. problem iskazne zadovoljivosti. Promenljive i ograničenja problema CSP se prevode (kodiraju) u SAT instancu, ona se potom rešava pomoću modernih SAT rešavača i rešenje se, ako postoji, prevodi u rešenje problema CSP. Glavni cilj ove teze je unapređenje rešavanja problema CSP svođenjem na SAT. Razvijena su dva nova hibridna kodiranja (prevođenja u SAT formulu) koja kombinuju dobre strane postojećih kodiranja. Dat je dokaz korektnosti jednog od kodiranja koji do sada nije postojao u literaturi. Razvijen je sistem meSAT koji omogućava svođenje problema CSP na SAT pomoću četiri osnovna i dva hibridna kodiranja, kao i rešavanje problema CSP svođenjem na dva problema srodna problemu SAT, SMT i PB. Razvijen je portfolio za automatski odabir kodiranja/rešavača za ulaznu instancu koju je potrebno rešiti i pokazano je da je razvijeni portfolio uporediv sa najefikasnijim savremenim pristupima. Prikazan je novi pristup zasnovan na kratkim vremenskim ograničenjima sa ciljem da se značajno smanji vreme pripreme portfolija. Pokazano je da se ovim pristupom dobijaju rezultati konkurentni onima koji se dobijaju korišćenjem standardnog vremena za pripremu. Izvršeno je poređenje nekoliko tehnika mašinskog učenja, sa ciljem da se ustanovi koja od njih je pogodnija za pristup sa kratkim treniranjem. Prikazan je jedan realan problem, problem raspoređivanja kontrolora leta, kao i tri njegova modela. Veliki broj metoda rešavanja i raznovrsnih rešavača je upotrebljeno za rešavanje ovog problema. Razvijeno je više optimizacionih tehnika koje imaju za cilj pronalaženje optimalnih rešenja problema. Pokazuje se da je najefikasnija hibridna tehnika koja kombinuje svođenje na SAT i lokalnu pretragu. Razmotren je i problem sudoku, kao i postojeće tehnike rešavanja sudoku zagonetki većih dimenzija od 9 × 9. Pokazuje se da je u rešavanju ovih zagonetki najefikasnije već postojeće svođenje na SAT. Unapređen je postojeći algoritam za generisanje velikih sudoku zagonetki. Pokazano je da jednostavna pravila preprocesiranja dodatno unapređuju brzinu generisanja sudokua.