Boolean SAT/SMT Solvers for Software Engineering - История изменений

Root в 15:00, 9 февраля 2019

2019-02-09T15:00:03Z

PodymovVV в 15:18, 19 февраля 2017

2017-02-19T15:18:21Z

ShupletsovMS: /* Week 2 Lectures */

2016-06-17T17:29:14Z

‎Week 2 Lectures

ShupletsovMS: /* Week 2 Lectures */

2016-06-17T17:28:47Z

‎Week 2 Lectures

ShupletsovMS: /* Расписание занятий */

2016-06-17T17:27:23Z

‎Расписание занятий

ShupletsovMS: /* Course annotation */

2016-06-17T17:26:39Z

‎Course annotation

ShupletsovMS: /* Week 2 Lectures */

2016-06-17T17:21:22Z

‎Week 2 Lectures

ShupletsovMS в 15:18, 10 апреля 2016

2016-04-10T15:18:16Z

ShupletsovMS: /* Course structure */

2016-04-10T15:16:42Z

‎Course structure

ShupletsovMS: /* Week 1 Lectures */

2016-04-08T07:44:54Z

‎Week 1 Lectures

@@ Строка 1: / Строка 1: @@
 Спецкурс на английском языке для студентов магистратуры.
 Лектор курса - профессор университета Ватерлоо (Канада), Виджей Ганеш (Vijay Ganesh).
@@ Строка 44: / Строка 46: @@
 Dr. Vijay Ganesh is an assistant professor at the University of Waterloo, Canada, since September 2012. Prior to that he was a Research Scientist at the Massachusetts Institute of Technology (2007-2012), and received his PhD in computer science from Stanford University in 2007. Vijay's primary area of research is the theory and practice of automated reasoning aimed at software engineering, formal methods and security. In this context he has developed  many SAT/SMT solvers, most notably, STP, HAMPI, and Z3str2. He has also worked on theoretical results in the context of rich string theories. For his research, he recently won an IBM Research Faculty Award in 2015, two Google Research Faculty Awards in 2013 and 2011, and 7 best paper awards/honors at conferences like SAT, CAV, CADE, and DATE. His solver STP has won numerous awards in highly competitive international SMT solver competitions. Recently he was invited to the first Heidelberg Laureate Forum in 2013, a gathering where young researchers from around the world were selected to meet with leading computer scientists and mathematicians.

@@ Строка 3: / Строка 3: @@
 == Расписание занятий ==
-*Занятия первой части курса: 4,5,7 и 8 апреля в аудитории 526б, начало в 18:00.
+*Занятия первой части курса: 4,5,7 и 8 апреля 2016 года в аудитории 526б, начало в 18:00.
-*Занятия второй части курса: 16 b 17 июня в аудитории 526б, начало в 18:00.
+*Занятия второй части курса: 16 b 17 июня 2016 года в аудитории 526б, начало в 18:00.
 == Course annotation ==

@@ Строка 37: / Строка 37: @@
 **[[Media:SAT_SMT_Vijay_Ganesh_lecture_6.pdf| Presentation]]
 * Lecture 7: Counterexample-guided abstraction refinement(CEGAR). CEGAR-based SMT solver.
-**[[Media:SAT_SMT_Vijay_Ganesh_lecture_6.pdf| Presentation]]
+**[[Media:SAT_SMT_Vijay_Ganesh_lecture_5.pdf| Presentation]]
 == Brief Bio of Dr. Vijay Ganesh ==

@@ Строка 37: / Строка 37: @@
 **[[Media:SAT_SMT_Vijay_Ganesh_lecture_6.pdf| Presentation]]
 * Lecture 7: Counterexample-guided abstraction refinement(CEGAR). CEGAR-based SMT solver.
-**[[Media:SAT_SMT_Vijay_Ganesh_lecture_7.pdf| Presentation]]
+**[[Media:SAT_SMT_Vijay_Ganesh_lecture_6.pdf| Presentation]]
 == Brief Bio of Dr. Vijay Ganesh ==

@@ Строка 4: / Строка 4: @@
 == Расписание занятий ==
 *Занятия первой части курса: 4,5,7 и 8 апреля в аудитории 526б, начало в 18:00.
-*Занятия второй части курса: будут объявлены позже.
+*Занятия второй части курса: 16 b 17 июня в аудитории 526б, начало в 18:00.
 == Course annotation ==

@@ Строка 7: / Строка 7: @@
 == Course annotation ==
-Computer-aided reasoning tools, such as SAT/SMT solvers, have had a dramatic impact on software engineering and security in recent years. So much so that a large number of software engineering tools these days are designed primarily using a SAT or SMT solver as a backend. The primary reason for this recent adoption of solvers in software engineering is the continued improvement in their performance and expressive power. For example, over the last 15 years we have seen a 1000x improvement in the performance of conflict-driven clause-learning SAT solvers. Given their foundational importance and impact, it is important for any student wanting to do research in software engineering, security, or mathematics to have a thorough understanding of SAT/SMT solvers and proof assistants. In this course, we will cover the theory and practice of automated reasoning tools such as conflict-driven clause learning SAT solvers, SMT solvers, and their applications. Below find a brief summary of the topics that we will cover in the course. The course consists of 8 lectures of 3 hour each.
+Computer-aided reasoning tools, such as SAT/SMT solvers, have had a dramatic impact on software engineering and security in recent years. So much so that a large number of software engineering tools these days are designed primarily using a SAT or SMT solver as a backend. The primary reason for this recent adoption of solvers in software engineering is the continued improvement in their performance and expressive power. For example, over the last 15 years we have seen a 1000x improvement in the performance of conflict-driven clause-learning SAT solvers. Given their foundational importance and impact, it is important for any student wanting to do research in software engineering, security, or mathematics to have a thorough understanding of SAT/SMT solvers and proof assistants. In this course, we will cover the theory and practice of automated reasoning tools such as conflict-driven clause learning SAT solvers, SMT solvers, and their applications. Below find a brief summary of the topics that we will cover in the course. The course consists of 7 lectures of 3 hour each.
 == Course projects ==

@@ Строка 32: / Строка 32: @@
 === Week 2 Lectures ===
-* Lecture 5: First-order logic, first-order theories and related SAT problems
+* Lecture 5: Motivation for SMT solvers, and combination of decision procedures.
-* Lecture 6: SMT solvers, DPLL(T), combination of theories
+**[[Media:SAT_SMT_Vijay_Ganesh_lecture_5.pdf| Presentation]]
-* Lecture 7: Solvers for theories over bit-vectors and arrays
+* Lecture 6: Combination of decision procedures.
-* Lecture 8: Solvers for theories over strings
+**[[Media:SAT_SMT_Vijay_Ganesh_lecture_6.pdf| Presentation]]
 == Brief Bio of Dr. Vijay Ganesh ==

@@ Строка 9: / Строка 9: @@
 Computer-aided reasoning tools, such as SAT/SMT solvers, have had a dramatic impact on software engineering and security in recent years. So much so that a large number of software engineering tools these days are designed primarily using a SAT or SMT solver as a backend. The primary reason for this recent adoption of solvers in software engineering is the continued improvement in their performance and expressive power. For example, over the last 15 years we have seen a 1000x improvement in the performance of conflict-driven clause-learning SAT solvers. Given their foundational importance and impact, it is important for any student wanting to do research in software engineering, security, or mathematics to have a thorough understanding of SAT/SMT solvers and proof assistants. In this course, we will cover the theory and practice of automated reasoning tools such as conflict-driven clause learning SAT solvers, SMT solvers, and their applications. Below find a brief summary of the topics that we will cover in the course. The course consists of 8 lectures of 3 hour each.
 == Course structure ==
 [[Media:SAT_SMT_Vijay_Ganesh_intro.pdf| Presentation of course overview]]

@@ Строка 26: / Строка 26: @@
 *# [[Media:SAT_SMT_Vijay_Ganesh_ICCAd96.pdf| GRASP—A New Search Algorithm for Satisfiability]]
 *# [[Media:SAT_SMT_Vijay_Ganesh_vg2014.pdf| Impact of Community Structure on SAT Solver Performance]]
 * Lecture 4: Application of SAT solvers to symbolic-execution based testing