|
| Udgave: |
Efterår 2012 NAT |
| Point: |
7,5 |
| Blokstruktur: |
1. blok |
| Skemagruppe: |
C |
| Fagområde: |
dat |
| Varighed: |
9 uger |
| Omfang: |
4 hours of lecture per week. One hour of discussion of exercises per week. |
| Institutter: |
Datalogisk Institut |
| Studieordning: |
Datalogi |
| Uddannelsesdel: |
Bachelor niveau |
| Kontaktpersoner: |
Holger Bock Axelsen |
| Andre undervisere: |
Nils Andersen |
| Skema- oplysninger: |
 Vis skema for kurset
Samlet oversigt over tid og sted for alle kurser inden for Lektionsplan for Det Naturvidenskabelige Fakultet Efterår 2012 NAT |
| Undervisnings- form: |
Forelæsninger |
| Formål: |
In recent years, powerful tools have been developed for the verification of programs and hardware systems. These tools are furthermore making their way into industry, as it is recognized that static verification can give safety guarantees that are superior to that which can be determined by testing. The goal of this course is to give the student a firm foundation in such techniques, including basic logic and the more specialized logical formalisms that are used in modelling, specification, and verification of programs and hardware systems.
The course is applicable to any area of computer science where it is necessary to specify required properties or to prove that a system satisfies a specification. |
| Indhold: |
The course covers propositional and predicate logic in detail. It then turns to more specialized logics, such as temporal logic, that are used to reason about the correctness of computer systems. Many examples are shown, and an explanation is given of the increasingly widespread technology for modelling of computer systems, knowns as symbolic model checking. |
| Kompetence- beskrivelse: |
Constructing formal proofs in a variety of logics, familiarity with model checking tools, understanding of the relationship between what is true and what is provable.
|
| Målbeskrivelse: |
At course completion, the student should be able to:
Use propositional logic, predicate logic, and temporal logic to describe various real-world situations. Use the semantics and deduction techniques for propositional logic, predicate logic, and temporal logic to prove properties such as implication, satisfiability, and validity about formulas in the logics. Prove properties of the relationship (e.g., soundness or completeness) between the semantics of propositional logic, predicate logic, Hoare logic, and temporal logic and their various associated deduction techniques. Perform any of the above in the context of a logic that is a minor variant of propositional logic, predicate logic, or temporal logic. |
| Lærebøger: |
Is expected to be: Logic in Computer Science, 2nd Edition; by Michael Huth and Mark Ryan, Cambridge University Press, 2004, ISBN 0 521 54310X. |
| Tilmelding: |
Via KUnet fra May 15th to June 1st. |
| Faglige forudsætninger: |
Ingen |
| Formelle krav: |
Ingen |
| Eksamensform: |
Assignments will be made each week and be due in the following week. 5 assignments out of the 7 must be completed by the due date and approved to qualify to take the exam. The exam will be a 4-hour written final exam, and will be graded using the 7-step grading scale with an internal grading. All books and notes may be brought to the exam.
Reexam is a 4-hour written final exam, which is replaced by a 20 minute oral exam with 20 minutes for preparation if there are 10 or fewer students registered for the exam. Both with internal grading. |
| Eksamen: |
Skriftlig prøve den 7. november 2012.
Reeksamen: BEMÆRK reeksamensformen er ændret! Mundtlig prøve den 30. januar 2013. Såfremt der er 10 eller færre tilmeldte til reeksamen, vil den blive afholdt som en mundtlig prøve.
|
| Kursus hjemmeside: |
 |
| Undervisnings- sprog: |
Kun engelsk
|
| Sidst redigeret: |
4/1-2013 |