M.Tech 2nd sem CS Syllabus (pdf)

 M. Tech in Computer Science and Engineering II Semester

Formal Models in Computer Science

Subject Code : 12SCS21                                                                                      IA Marks : 50

No of Lecture Hrs/Week : 4                                                                                Exam hours : 3

Total No of Lecture Hours : 52                                                                            Exam Marks : 100

1. Propositional Logic

Declarative  sentences,  Natural  deduction,  Propositional  logic  as  a  formal  language,  Semantics  of propositional logic, Normal forms.

Image credit

2. Predicate Logic

The need for a richer language,  Predicate logic as a formal language, Proof theory of predicate logic, Semantics of predicate logic, Undecidability of predicate logic, Micromodels of software.

3. Verification by Model Checking

Motivation  for verification,  Linear-time  temporal  logic, Model checking,  Branching-time  logic, CTL*

and the expressive powers of LTL and CTL.

4. Program Verification

Need for specifying and verifying code, A framework for software verification, Proof calculus for partial correctness and total correctness, Programming by contract.

5. Introduction to Z: Basic concepts; Z notation in Propositional logic and Predicate logic.

Laboratory Work:

1. Design, develop and run a program in ALLOY (or in any equivalent  system)  to model a Software Package Dependency System. Make suitable assumptions regarding the system. The model should allow checking to see if prerequisites in the form of libraries or other packages are present for all components in the system

2. Design, develop and run a program in NuSMV (or in any equivalent system) to model and solve the

Mutual Exclusion problem.

3. Design, develop and run a program in NuSMV (or in any equivalent system) to model and simulate the

Alternate Bit Protocol.

4. Design, develop and run a program in NuSMV (or in any equivalent system) to model and solve the planning problem of Ferry Man.

5. Design, develop and run a program in NuSMV (or in any equivalent system) to model and solve the

Dining Philosophers Problem.

Text Books:

1. Michael Huth and Mark Ryan: Logic in Computer Science, 2nd Edition, Cambridge University Press,

2004.

2. Jim Woodcock , Jim Davies: Using Z Specification, Refinement and Proof, Prentice Hall, 1996. (Online Edition: http://www.usingz.com/text/online/)

The above is sample. Click on Download to get the complete 

syllabus

                       DOWNLOAD

Please comment.......