PROFESOR I DOKTOR EMINA TORLAK
Porodica Torlak je protjerana iz svog rodnog grada Foče. Otac Aziz, poznat i omiljen ljekar nestao je bez traga. Emina je tad imala samo 12 godina. Iz Foče, sa majkom Edinom, takođe doktoricom, i sestrom Almom u nekoj od izbjegličkih kolona dolazi u Sarajevo gdje preživljava novi pakao, onaj sarajevski 1992/95. godine.
Danas Emina, prva u historiji kompjuterskih nauka ispravlja i otklanja greške u navigacijskim sistemima u zračnom prostoru i riješava problem apsolutne greške.
oprema teksta i naslov:focanskidani
Spotlight: Emina Torlak
UW CSE’s Emina Torlak wins 2016 AITO Dahl-Nygaard Prize
I Am CSE: Zachary Tatlock & Emina Torlak
UW CSE professors Zach Tatlock and Emina Torlak discuss their research in software verification to ensure that programs for the operation of safety-critical systems do not contain potentially life-threatening errors. With the Neutrons Project, our researchers are making the control software for radiotherapy devices safer and more reliable by preventing errors that could lead to an overdose of patients undergoing cancer treatment. Their ongoing research has the potential to improve a variety of safety-critical systems across the country.
Published on Mar 4, 2016
Synthesis and Verification for All – Emina Torlak
Rosette is a programming language for creating new programming tools. It extends Racket with a few constructs that make it easy to build advanced tools for program verification and synthesis. Building these tools usually takes months or years of work, as well as expertise in many fields, from formal methods to programming languages to software engineering. With Rosette, creating such a tool is as easy as defining a new domain-specific language in Racket. Once you define your language, you get the tools for (almost) free. This talk will provide a brief introduction to Rosette, concluding with a whirlwind tour of recent applications to finding bugs in radiotherapy software, generating efficient code for ultra low-power hardware, and creating custom tutors for K-12 algebra.
Emina Torlak is an assistant professor at the University of Washington. She works on computer-aided design, verification, and synthesis of software. Emina is the creator of Rosette, a new Racket-based language that makes it easy to build efficient tools for verifying and synthesizing all kinds of programs, from radiotherapy controllers to automated algebra tutors.
Published on Mar 31, 2017
A Constraint Solver: Finding Models and Cores of Large Relational Specifications
Relational logic is an attractive candidate for a software description language, because both the design and implementation of software often involve reasoning about relational structures, whether in the problem domain (organizational structure, for example), in the high level design (architectural configurations, for example) or in low level code (graphs and linked lists). Until recently, however, frameworks for solving relational constraints (such as Alloy3) have had limited applicability. While powerful enough to analyze relatively small, hand-crafted models of software systems, current frameworks perform poorly on large and automatically generated specifications. In this talk, I will describe Kodkod, an efficient constraint solver for relational logic, with recent applications to design analysis, code checking, test-case generation, and declarative configuration. The Kodkod system includes a finite model finder and a minimal unsatisfiable core extractor, both based on SAT solving technology. I will present the key ideas and contributions behind these analyses, discuss how they compare to existing approaches, and conclude with an overview of future work.
Published on Sep 6, 2016