<- Archives UCL - Programme d'études ->



Programming methods [ LSINF2224 ]


5.0 crédits ECTS  30.0 h + 15.0 h   2q 

Teacher(s) Pecheur Charles ;
Language English
Place
of the course
Louvain-la-Neuve
Online resources

 > http://www.icampus.ucl.ac.be/claroline/course/index.php?cid=LINF2224

Prerequisites
  • basic notions in theory of programming, as covered in courses such as INGI1122 (Program conception methods), INGI1101 (Logic and discrete structures) and INGI1123 (Calculability)
Main themes
  • Program foundations and properties, semantics, validity and proof.
  • Deductive proof for programs: Hoare logic, weakest preconditions, verification conditions, invariants and variants.
  • Automating proofs: loops, procedures and recursion, data structures, reactive program.
  • State-based analysis: models-checking, temporal logic, abstraction.
Aims

Students completing successfully this course will be able to

  • define and formalize the principles of program analysis and verification introduced in bachelor courses.
  • describe and apply the techniques that allow those principles to be automated on a computer.
  • illustrate the potential and limits of such techniques using pratical examples.

Students will have developed skills and operational methodology. In particular, they have developed their ability to

  • formalize in mathematical form a given problem;
  • write a brief technical report covering the main elements of an analysis;
  • argue orally.
Evaluation methods
  • Assignments (50% of final grade)
  • oral examination based on a list of questions (available at the end of the semester) (50% of final grade)
Teaching methods

The course combines

  • lectures,
  • exercises (modeling and analysis of programs),
  • and assignments where students use automated verification software (ESC/Java, Java PathFinder) to prove properties of Java programs.

The aims, methodology and tools used in each assignment are described in a document provided to the students. The program code to be analyzed is commented and a brief user's guide is included. The program verification and model-checking tools to be used are clearly indicated. To ease their grip by students, exercise sessions are planned. In addition, a consultancy is provided by the supervisors of the course in case of trouble. At the end of each mission, students write a brief report used as a basis for evaluation.

Content
  1. Demonstration
  2. Introduction
  3. Foundations
  4. Sequential Programs
  5. Verification Conditions
  6. Procedures
  7. Recursion
  8. Data Structures
  9. Reactive Programs
  10. State-Based Models
  11. Model Checking
  12. Abstraction
Bibliography

Support material :

  • copies from lecture slides

Bibliography :

  • B. Liskov, J. Guttag. Program Development in Java: Abstraction, Specification and Object-Oriented Design. Addison-Wesley, 2001.
  • O.-J. Dahl. Verifiable Programming. Prentice Hall, 1992.
  • K. R. Apt, E.-R. Olderog. Verification of Sequential and Concurrent Programs. Springer Verlag, 1991.
  • J. Loeckx, K. Sieber. The Foundations of Program Verification (2nd Ed.) Wiley-Teubner, 1984.
  • D. Gries, The Science of Computer Programming. Springer-Verlag, 1981.

 

Other information

  

Cycle et année
d'étude
> Master [120] in Computer Science
> Master [120] in Computer Science and Engineering
Faculty or entity
in charge
> INFO


<<< Page précédente