Agnishom · August 4, 2018 17:35
diff --git a/smt.txt b/smt.txt
 Symbolic Analysis Using SMT Solvers (SASS)
 Instructor: M.K. SrivasFirst
 Meeting: Aug 8 (Wed) 3:30PM, Lec Hall 801

 Satisfiability-Modulo Theory (SMT) solver is a sound algorithmic framework for combining automatic decision procedures for first-order (i.e., quantifier-free) theories of data types, such as propositional logic, un-interpreted functions, bit-vectors, arithmetic, arrays, pointers, etc.,  that commonly occur in modern programming languages.  Advances in SMT solving technology in the recent past have enabled development of tools - interactive theorem provers, model checkers, guided-synthesizers - for practical formal verification and synthesis of sequential and concurrent SW systems. This course covers the theory and practice of SMT solvers providing hands-on exposure to the use of SMT solvers.  The topics of the course will be distributed over two not necessarily contiguous parts.  The first part will cover the basic principles and theory behind construction of SMT solvers, describing in detail decision procedures for some of the theories commonly supported in popular SMT solvers.   The second part will cover applications of SMT solvers in the following areas: interactive theorem proving, model checking, and program synthesis.  The course will be graded based on the following requirements:
 1. A set of written assignments and tests covering Part-1.
 2. A final project based on the use of a state-of-art SMT solver to implement a verification or synthesis task or a case-study using an interactive theorem prover.

 Desired Background:
 Mathematical Logic
 Basic Programming

 PS

 If you can't attend the first meeting but are still interested in the course, please send me an email (mksrivas@hotmail.com)
	Symbolic Analysis Using SMT Solvers (SASS)
	Instructor: M.K. SrivasFirst
	Meeting: Aug 8 (Wed) 3:30PM, Lec Hall 801

	Satisfiability-Modulo Theory (SMT) solver is a sound algorithmic framework for combining automatic decision procedures for first-order (i.e., quantifier-free) theories of data types, such as propositional logic, un-interpreted functions, bit-vectors, arithmetic, arrays, pointers, etc., that commonly occur in modern programming languages. Advances in SMT solving technology in the recent past have enabled development of tools - interactive theorem provers, model checkers, guided-synthesizers - for practical formal verification and synthesis of sequential and concurrent SW systems. This course covers the theory and practice of SMT solvers providing hands-on exposure to the use of SMT solvers. The topics of the course will be distributed over two not necessarily contiguous parts. The first part will cover the basic principles and theory behind construction of SMT solvers, describing in detail decision procedures for some of the theories commonly supported in popular SMT solvers. The second part will cover applications of SMT solvers in the following areas: interactive theorem proving, model checking, and program synthesis. The course will be graded based on the following requirements:
	1. A set of written assignments and tests covering Part-1.
	2. A final project based on the use of a state-of-art SMT solver to implement a verification or synthesis task or a case-study using an interactive theorem prover.

	Desired Background:
	Mathematical Logic
	Basic Programming

	PS

	If you can't attend the first meeting but are still interested in the course, please send me an email (mksrivas@hotmail.com)
No results found