http://flolac.iis.sinica.edu.tw/flolac11/ 2011-09-27T09:47:25+08:00 http://flolac.iis.sinica.edu.tw/flolac11/ http://flolac.iis.sinica.edu.tw/flolac11/lib/images/favicon.ico text/html 2011-08-10T03:55:47+08:00 tsay http://flolac.iis.sinica.edu.tw/flolac11/doku.php?id=zh-tw:start&rev=1312919747&do=diff * [2011/8/10] [FLOLAC 2011 成績報告] * [2011/6/25] 所有課程投影片將於第一天報到時發放；主辦單位免費供應上課期間每日之午餐。 * [2011/6/25] 全體學員請於二十七日(星期一)8:30-9:00報到；9:00進行始業式；9:10開始上課。 text/html 2011-07-07T06:49:23+08:00 mht208 http://flolac.iis.sinica.edu.tw/flolac11/doku.php?id=en:lecture:automata&rev=1309992563&do=diff Lecturer: 蔡益坤 Yih-Kuen Tsay * Lecture 1: Automata-Based Model Checking (3 hours) * Büchi automata, generalized Büchi automata, model checking using automata, intersection and emptiness test, parallel compositions, on-the-fly state exploration, fairness, the SPIN model checker text/html 2011-07-07T05:00:46+08:00 mht208 http://flolac.iis.sinica.edu.tw/flolac11/doku.php?id=en:lecture:logic&rev=1309986046&do=diff Lecturer: 蔡益坤 Yih-Kuen Tsay * Lecture 1: Elementary Logic (3 hours) * propositional logic: syntax and semantics, satisfiability, tautology, normal forms, proofs, natural deduction, soundness, completeness, compactness, consistency * first-order logic: syntax and semantics, validity, natural deduction, soundness, completeness, first-order theory text/html 2011-07-05T10:03:46+08:00 mht208 http://flolac.iis.sinica.edu.tw/flolac11/doku.php?id=en:lecture:satisfiability&rev=1309831426&do=diff Lecturers: 黃鐘揚 Chung-Yang (Ric) Huang and 江介宏 Jie-Hong Roland Jiang * Introduction to Boolean Satisfiability (SAT) solvers * SAT-based hardware verification * SAT and interpolation in logic synthesis * QBF evaluation and applications text/html 2011-07-05T03:42:23+08:00 mht208 http://flolac.iis.sinica.edu.tw/flolac11/doku.php?id=en:lecture:temporal&rev=1309808543&do=diff Lecturer: 王凡 Farn Wang * LTL * CTL, CTL* * Expressivenss * LTL satisfiability: tableau-based techniques * CTL model-checking * Simulation-checking * ATL and game graphs * ATL model-checking * Temporal Logics & Model Checking [[slides]] text/html 2011-06-29T11:55:50+08:00 yfc http://flolac.iis.sinica.edu.tw/flolac11/doku.php?id=en:lecture:smt&rev=1309319750&do=diff Lecturer: 陳郁方 Yu-Fang Chen * Introduction to Satisfiability Modulo Theories (SMT) * Software model checking using SMT and tool demonstration * Theory of linear arithmetic * Theory of equalities and uninterpreted function * Using SMT for Software Model Checking text/html 2011-06-28T04:46:56+08:00 yuf http://flolac.iis.sinica.edu.tw/flolac11/doku.php?id=en:lecture:string&rev=1309207616&do=diff Lecturer: 郁方 Fang Yu * Introduction to string analysis, string automata and its symbolic representation * Pre- and post-image computations on automata of common string operations * Widening and fixpoint acceleration, forward and backward reachability analyses of string-manipulating programs * From string analysis to size analysis, composite analysis and relational analysis * String abstractions for string verification * Automatic detection and removal of Web application vulnerabilit… text/html 2011-06-20T14:41:23+08:00 tsay http://flolac.iis.sinica.edu.tw/flolac11/doku.php?id=en:start&rev=1308552083&do=diff Researchers in Taiwan who are interested in the foundational aspects of computing science have founded a number of research teams and worked together in some joint projects. As in any discipline, a student will have to go through a series of courses to be prepared for further research in this field. Being affiliated to different institutes, however, the researchers often find it difficult to lecture all these courses alone. It is thus desirable to bring together those who share a common interest… text/html 2011-04-29T04:50:21+08:00 mht208 http://flolac.iis.sinica.edu.tw/flolac11/doku.php?id=zh-tw:lecture:temporal&rev=1304023821&do=diff Lecturer: 王凡 Farn Wang * LTL * CTL, CTL* * Expressivenss * LTL satisfiability: tableau-based techniques * CTL model-checking * Simulation-checking * ATL and game graphs * ATL model-checking * Temporal Logics & Model Checking [[slides]] text/html 2011-04-29T04:49:44+08:00 mht208 http://flolac.iis.sinica.edu.tw/flolac11/doku.php?id=zh-tw:lecture:string&rev=1304023784&do=diff Lecturer: 郁方 Fang Yu * Introduction to string analysis, string automata and its symbolic representation * Pre- and post-image computations on automata of common string operations * Widening and fixpoint acceleration, forward and backward reachability analyses of string-manipulating programs * From string analysis to size analysis, composite analysis and relational analysis * String abstractions for string verification * Automatic detection and removal of Web application vulnerabilit… text/html 2011-04-29T04:49:33+08:00 mht208 http://flolac.iis.sinica.edu.tw/flolac11/doku.php?id=zh-tw:lecture:automata&rev=1304023773&do=diff Lecturer: 蔡益坤 Yih-Kuen Tsay * Lecture 1: Automata-Based Model Checking (3 hours) * Büchi automata, generalized Büchi automata, model checking using automata, intersection and emptiness test, parallel compositions, on-the-fly state exploration, fairness, the SPIN model checker text/html 2011-04-29T04:49:15+08:00 mht208 http://flolac.iis.sinica.edu.tw/flolac11/doku.php?id=zh-tw:lecture:satisfiability&rev=1304023755&do=diff Lecturers: 黃鐘揚 Chung-Yang (Ric) Huang and 江介宏 Jie-Hong Roland Jiang * Introduction to Boolean Satisfiability (SAT) solvers * SAT-based hardware verification * SAT and interpolation in logic synthesis * QBF evaluation and applications text/html 2011-04-29T04:48:54+08:00 mht208 http://flolac.iis.sinica.edu.tw/flolac11/doku.php?id=zh-tw:lecture:smt&rev=1304023734&do=diff Lecturer: 陳郁方 Yu-Fang Chen * Introduction to Satisfiability Modulo Theories (SMT) * Software model checking using SMT and tool demonstration * Theory of linear arithmetic * Theory of equalities and uninterpreted function * Using SMT for Software Model Checking text/html 2011-04-29T04:45:27+08:00 mht208 http://flolac.iis.sinica.edu.tw/flolac11/doku.php?id=zh-tw:lecture:logic&rev=1304023527&do=diff Lecturer: 蔡益坤 Yih-Kuen Tsay * Lecture 1: Elementary Logic (3 hours) * propositional logic: syntax and semantics, satisfiability, tautology, normal forms, proofs, natural deduction, soundness, completeness, compactness, consistency * first-order logic: syntax and semantics, validity, natural deduction, soundness, completeness, first-order theory