Presentation of course overview (1185844)
Текст из файла
SAT/SMT Solvers for So.ware Engineering and Security Instructor Bio and Course Outline by Vijay Ganesh Assistant Professor, University of Waterloo, Canada. Date: April 4-‐8, 2016 Venue: Moscow State University, Russia.
Brief Bio of Vijay Ganesh • Studied mathematical logic and formal methods at Stanford, USA(PhD in computer science, 2007)• Scientist at the Massachusetts Institute of Technology, USA(2007-2012)• Assistant professor at the University of Waterloo, Canada(2012 – present)• Research focus– Solvers and proof assistants for software engineering, security, and mathematics– Logic and complexity-theoretic questions that arise in software engineering– Foundations of mathematics Key ContribuOons Name Key Concept STP Bit-‐vector & Array Solver1,2 AbstracOon-‐refinement for solving Impact Pubs Concolic TesOng CAV 2007 CCS 2006 TISSEC 2008 HAMPI String Solver1 App-‐driven bounding for solving Analysis of Web Apps ISSTA 20093 TOSEM 2012 CAV 2011 Z3-‐str String and Numeric Solver1 Novel techniques for string + integer combinaOon Analysis of Web Apps FSE 2013 CAV 20153 Maple Series of SAT Solvers, and understanding SAT Branching heurisOcs, and community structure One of the fastest SAT solvers to-‐date AAAI 2016 HVC 2015, SAT 20143 MathCheck Conjecture Verifier CAS+SAT combinaOon Finitely verified math conjectures CADE 20153 Taint-‐based Fuzzing Data flow is cheaper than concolic Scales be`er than concolic ICSE 2009 AutomaNc Input RecNficaNon AutomaOc security envelope New security approach ICSE 2012 Solved open problems HVC 2012 Undecidability results for theories New reducOons over strings 1. 100+ research projects use STP, HAMPI, and Z3str2.
IBM Faculty Award 2015, Google Faculty Research Awards 2011/2013 2. STP won the SMTCOMP 2006/2010 and second in 2011/2014 compeOOons for bit-‐vector solvers 3. Won 7 best paper awards/honors at various conferences including SAT, DATE, SPLC, CAV, and CADE 4. Retargetable Compiler (DATE 1999, 2008). Ten Year Most-‐influenOal paper award at DATE 2008. Current Projects 1. Understanding why conflict-driven clause-learning SAT solvers are so efficient2. Theory and practice of solvers over strings, integers, and bit-vectors3. MathCheck: SAT+CAS combination to verify math conjectures4. Applications of SAT solvers to security5. Formal verification of physics software6. Attack-resistanceSyllabus Lecture Date Contents 1 Apr 4th, 2016 Brief introducOon to logic in sogware engineering and security. IntroducOon to SAT/SMT solvers and their applicaOons, in parOcular, symbolic-‐execuOon based analysis and tesOng 2 Apr 5th, 2016 Internals of SAT Solvers 3 Apr 7th, 2016 Internals of SAT Solvers (conOnued) 4 Apr 8th, 2016 Internals of SAT Solvers (conOnued) 5 TBD IntroducOon to first-‐order theories, and SMT solvers.
DPLL(T) and combinaOon of theories 6 TBD Bit-‐vector and array solvers. Counter-‐example guided abstracOon-‐refinement (CEGAR) 7 TBD Solvers for theories over string equaOons (pracOce) 8 TBD Solvers for theories over string equaOons (theory) Course Requirements • Attendance• Final exam and tests• Projects, if interested• Grading to be determined by MSU faculty.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
