S E F M S c h o o l
2 0 0 9
SOFTWARE ENGINEERING AND FORMAL METHODS
16-22
November, 2009 College of
Technology, Vietnam National University, Hanoi, Vietnam |
|
COURSES
SEFM School Place: University of Technology and Engineering,Vietnam
National University - Room 212, Building E3, 144 Xuan Thuy, Cau Giay, Hanoi,
VietnamHotel for participants: No 4, Allay 2, Tran Quy Kien,
Dich Vong, Cau Giay, Hanoi, Vietnam
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||
|
Day |
||||
|
|
Opening
by Prof. Dang Van Hung and Prof. Nguyen Ngoc Binh |
|
|
|
|
Morning session: |
Logics for Computer Science |
|
|
|
|
|
Lecturer: Hiroakira Ono |
|
|
|
|
|
JAIST (Japan
Advanced Institute of Science and Technology), Japan |
|||
|
|
||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lecture Time |
|
|
|
|
|
Coffee Break |
|
|
|
|
|
Lecture Time |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lunch Break |
|
|
|
|
Early afternoon session: |
SAT/SMT
solvers, its algorithm, implementation, and applications |
|
|
|
|
|
Lecturer: Nao Hirokawa |
|
|
|
|
|
JAIST (Japan
Advanced Institute of Science and Technology), Japan |
|
||
|
|
||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lecture Time |
|
|
|
|
|
Coffee Break |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Late afternoon session: |
Java
program analysis as model checking |
|
|
|
|
|
Lecturer: Mizuhito Ogawa |
|
|
|
|
|
JAIST (Japan
Advanced Institute of Science and Technology), Japan |
|
||
|
|
||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lecture Time |
|
|
|
|
|
Coffee Break |
|
|
|
|
|
Lecture Time |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|||
|
Day |
|
|||
|
Morning session: |
Logics for Computer Science (continued) |
|
|
|
|
|
Lecturer: Hiroakira Ono |
|
|
|
|
|
JAIST (Japan
Advanced Institute of Science and Technology), Japan |
|
||
|
|
||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lecture Time |
|
|
|
|
|
Coffee Break |
|
|
|
|
|
Lecture Time |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lunch Break |
|
|
|
|
Early afternoon session: |
SAT/SMT
solvers, its algorithm, implementation, and applications (continued) |
|
|
|
|
|
Lecturer: Nao Hirokawa |
|
|
|
|
|
JAIST (Japan
Advanced Institute of Science and Technology), Japan |
|
||
|
|
||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lecture Time |
|
|
|
|
|
Coffee Break |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Late afternoon session: |
Java
program analysis as model checking (continued) |
|
|
|
|
|
Lecturer: Mizuhito Ogawa |
|
|
|
|
|
JAIST (Japan
Advanced Institute of Science and Technology), Japan |
|
||
|
|
||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lecture Time |
|
|
|
|
|
Coffee Break |
|
|
|
|
|
Lecture Time |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|||
|
Day |
|
|||
|
Morning session: |
Logics for Computer Science (continued) |
|
|
|
|
|
Lecturer: Hiroakira Ono |
|
|
|
|
|
JAIST (Japan
Advanced Institute of Science and Technology), Japan |
|
||
|
|
||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lecture Time |
|
|
|
|
|
Coffee Break |
|
|
|
|
|
Lecture Time |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lunch Break |
|
|
|
|
Early afternoon session: |
SAT/SMT
solvers, its algorithm, implementation, and applications (continued) |
|
|
|
|
|
Lecturer: Nao Hirokawa |
|
|
|
|
|
JAIST (Japan
Advanced Institute of Science and Technology), Japan |
|
||
|
|
||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lecture Time |
|
|
|
|
|
Coffee Break |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Late afternoon session: |
Java
program analysis as model checking (continued) |
|
|
|
|
|
Lecturer: Mizuhito Ogawa |
|
|
|
|
|
JAIST (Japan
Advanced Institute of Science and Technology), Japan |
|
||
|
|
||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lecture Time |
|
|
|
|
|
Coffee Break |
|
|
|
|
|
Lecture Time |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|||
|
Day |
|
|||
|
Morning Session: |
Formal methods for human-computer interaction |
|
|
|
|
|
Lecturer: Antonio Cerone |
|
|
|
|
|
IIST, United Nations University, Macau SAR China |
|
||
|
|
||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lecture Time |
|
|
|
|
|
Coffee Break |
|
|
|
|
|
Lecture Time |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lunch Break |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Afternoon Session: |
Formal methods for human-computer interaction (continued) |
|
|
|
|
|
Lecture Time |
|
|
|
|
|
Coffee Break |
|
|
|
|
|
Lecture Time |
|
|
|
|
|
|
|||
|
Day |
|
|||
|
Morning Session: |
Formal methods for human-computer interaction (contined) |
|
|
|
|
|
Lecturer: Antonio Cerone |
|
|
|
|
|
IIST, United Nations University, Macau SAR China |
|
||
|
|
||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lecture Time |
|
|
|
|
|
Coffee Break |
|
|
|
|
|
Lecture Time |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lunch Break |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Afternoon Session: |
Formal methods for human-computer interaction (continued) |
|
|
|
|
|
Lecture Time |
|
|
|
|
|
Coffee Break |
|
|
|
|
|
Lecture Time |
|
|
|
|
|
|
|||
|
Day |
|
|||
|
Morning Session: |
Logical Program Specification and Testing |
|
|
|
|
|
Lecturer: Bernd-Holger Schlingloff |
|
|
|
|
|
Germany |
|
||
|
|
||||
|
|
|
|
|
|
|
|
|
|
|
|
|
8:30 - 10:00 |
Lecture Time |
|
|
|
|
10:00 - 10:15 |
Coffee Break |
|
|
|
|
10:15 - 11:30 |
Lecture Time |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
11:30-13:00 |
Lunch Break |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Afternoon Session: |
Logical Program Specification and Testing (continued) |
|
|
|
|
13:00 - 14:30 |
Lecture Time |
|
|
|
|
14:30 - 14:45 |
Coffee Break |
|
|
|
|
14:45 - 16:00 |
Lecture Time |
|
|
|
|
|
|
|||
|
Day 7: 22 (Sun) Nov |
|
|||
|
Morning Session: |
Logical Program Specification and Testing (continued) |
|
|
|
|
|
Lecturer: Bernd-Holger Schlingloff |
|
|
|
|
|
Germany |
|
||
|
|
||||
|
|
|
|
|
|
|
|
|
|
|
|
|
8:30 - 10:00 |
Lecture Time |
|
|
|
|
10:00 - 10:15 |
Coffee Break |
|
|
|
|
10:15 - 11:30 |
Lecture Time |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
11:30-13:00 |
Lunch Break |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Afternoon Session: |
Logical Program Specification and Testing (continued) |
|
|
|
|
13:00 - 14:30 |
Lecture Time |
|
|
|
|
14:30 - 14:45 |
Coffee Break |
|
|
|
|
14:45 - 16:00 |
Lecture Time |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
School
Closing by Prof. Dang Van Hung |
|
|
|
|
|
|
|||
|
Tutorials (23-24 Nov.): You are welcome to attend the tutorials
free (see
the programme) |
|
|||
|
|
|
|||
|
COURSE ABSTRACTS |
|
|||
|
|
|
|||
|
|
||||
|
Basics of logic for computer
science will be discussed in the course. A particular emphasis will be
placed on syntax and semantics of temporal logics, which offer primary
theoretical tools of discussing the specification and analysis of programs.
Basic knowledge on propositional logic is presupposed. The course begins by
introducing some sequent calculi and then develops the proof theory for
them. Decision procedures based on cut elimination theorem and their
application to automated theorem proving will be discussed. Then, several important
modal logics and Kripke-type semantics for them will be introduced, and
completeness and finite model property will be shown. These arguments can
be naturally extended to temporal logics. The decidability and the
expressiveness of linear temporal logic PLTL will be shown first, and then
temporal logic of concurrency CTL and its applications will be discussed. Lecturer: Hiroakira Ono |
|
|||
|
|
||||
|
|
|
|||
|
2. SAT/SMT solvers,
its algorithm, implementation, and applications |
|
|||
|
Basics of SAT and SMT
solvers will be discussed in the course. A SAT solver decides
whether a propositional formula (in conjunctive normal form) is
satisfiable. While the satisfiablity problem is known to be NP-complete, state-of-art
SAT solvers can solve the problems efficiently. SAT modulo theory (SMT)
solvers allow us to use more expressive formulas like linear arithmetic
formulas. Recently many techniques for SMT solvers have been developed, and
currently very efficient SMT solvers are available. In this course first we
discuss how to use SAT/SMT solvers for solving practical problems. Here the
main issue is how to reduce complex problems into (compact) propositional
formulas. Next algorithms (for SAT and SMT) including DPLL and quantifier
elimination are explained. Finally, as an instance of successful
applications of SAT/SMT solvers, we pick up automatic termination provers
for term rewrite systems and functional programming languages. Lecturer: Nao Hirokawa |
|
|||
|
|
||||
|
|
|
|||
|
|
||||
|
The scheme of dataflow
analysis as model checking was proposed in early 90's. This opens the
possibility to implement effective analyses by existing model checkers. When applying the
scheme to practical programming languages, such as Java, there are several
problems: a practical programming language has large language construct
(which makes its model generation heavy), and which abstraction is chosen.
Furthermore, Java has dynamic method invocations, which makes difficult to
generate its call graph. In this course, we
first introduce basis of model checking, reviewing automata theory
(including Buchi automata), and its implementation techniques behind in the
front half. The latter half focuses
on single-threaded Java program analyses based on model checking, answering
to the problems posed above and showing their limitations. Basic knowledge on
basic automata theory is assumed. Lecturer: Mizuhito Ogawa |
|
|||
|
|
||||
|
|
|
|||
|
|
||||
|
Lecturer: Antonio Cerone |
|
|||
|
|
||||
|
|
|
|||
|
5. Logical Program
Specification and Testing |
|
|||
|
Lecturer: Bernd-Holger Schlingloff |
|
|||
|
|
||||
|
|
|
|||
|
|
||||
|
|
|
|||
|
Hiroakira Ono joined Japan Advanced Institute
of Science and Technology in 1993 as a professor, and from 2008 he has been
a distinguished professor of Research Center for Integrated Science, JAIST.
His research topic is nonclassical logic, in particular, substructural
logics. In 2007, His coauthored book on algebraic approach to substructural
logics was published as a volume in the series "Studies in Logic and
the Foundations of Mathematics". He was also a member of Executive
Committee of Association for Symbolic Logic from 2006 to 2008. |
|
|||
|
|
||||
|
|
|
|||
|
Since 2007, Nao
Hirokawa is an assistant professor at School of Information Science at
Japan Advanced Institute of Science and Technology. His research interest
is term rewriting, in particular its termination analysis. |
|
|||
|
|
||||
|
|
|
|||
|
Mizuhito Ogawa joined Japan Advanced
Institute of Science and Technology (JAIST) in 2003 and he has been a
professor from 2007. His research interest contains formal languages,
rewriting, combinatorics, theorem proving, and model checking. For model
checking, his research focuses on program analyses by model checking, such
as a stacking-based context-sensitive points-to analysis for Java as
on-the-fly weighted pushdwon model checking. |
|
|||
|
|
||||
|
|
|
|||
|
Antonio Cerone joined the International
Institute for Software Technology (IIST) of the United Nations University
(UNU) as a Research Fellow in February 2004. His research focuses on the
use of formal methods in verification of software and hardware, and in
modelling cognitive human behaviour. He is particularly interested in the
verification of interactive systems , security systems, safety-critical
systems, asynchronous hardware and concurrent and real-time systems. |
|
|||
|
|
||||
|
|
|
|||
|
|
||||
|
|
||||
|
|
|
|||
|
Created: July 2009 |