Arvutiteaduse instituut
  1. Kursused
  2. 2013/14 sügis
  3. Formaalmeetodid tarkvaratehnikas (MTAT.03.274)
EN
Logi sisse

Formaalmeetodid tarkvaratehnikas 2013/14 sügis

  • Home
  • Lectures
  • Homework
  • Links

Formal Methods in Software Engineering

This course is an introduction to Model-Based Analysis and Testing techniques. We will experiment with real tools as well as learn the underlying theory. Therefore, some of the lectures will be hands-on labs and rather informal, while others will be more conventional lectures, dry and without any sense of humor.

  • Lectures / Labs:
    • Wednesdays 12:15, Liivi 2-612.
    • Fridays 10:15, Liivi 2-612.
  • Instructor: Vesal Vojdani (vesal@ut.ee)
  • Mailing list: ati.fm@lists.ut.ee
  • Exam:
    • Home exam deadline: 14.01.2013
    • Oral exam: 15.01.2013 (register timeslot!)
    • Room: 512 (below the lecture room).

List of Topics

The following techniques and tools will be covered. The underlying theory, such as SAT/SMT solving, Büchi Automata and Abstract Interpretation, will be introduced in a demand-driven fashion. Since the theory is a lot of fun in and of itself, we have to space things out to keep you motivated to hear all this practical stuff:

  1. Verification of Sequential Programs (Dafny)
  2. Static Analysis for Verifying Contracts (CodeContracts)
  3. Symbolic Execution for Test Generation (Pex)
  4. Model-Based Test Generation (SpecExplorer)
  5. Explicit State Model Checking (SPIN)
  6. Symbolic Model Checking (nuSMV)
  7. Model Checking Software: State bounds (CBMC) & Abstraction (SLAM)
  8. Static Analysis of Concurrent Systems (Goblint)

More broadly, the essence of this course is best expressed by a famous quotation from the father of Social Psychology, Kurt Lewin: "There is nothing more practical than a good theory."

Acknowledgements

The preparation of this course was partially supported by the EU ARTEMIS Joint Undertaking under grant agreement n° 269335 (MBAT: Combined Model-based Analysis and Testing of Embedded Systems) and the German Research Foundation (DFG).

  • Arvutiteaduse instituut
  • Loodus- ja täppisteaduste valdkond
  • Tartu Ülikool
Tehniliste probleemide või küsimuste korral kirjuta:

Kursuse sisu ja korralduslike küsimustega pöörduge kursuse korraldajate poole.
Õppematerjalide varalised autoriõigused kuuluvad Tartu Ülikoolile. Õppematerjalide kasutamine on lubatud autoriõiguse seaduses ettenähtud teose vaba kasutamise eesmärkidel ja tingimustel. Õppematerjalide kasutamisel on kasutaja kohustatud viitama õppematerjalide autorile.
Õppematerjalide kasutamine muudel eesmärkidel on lubatud ainult Tartu Ülikooli eelneval kirjalikul nõusolekul.
Tartu Ülikooli arvutiteaduse instituudi kursuste läbiviimist toetavad järgmised programmid:
euroopa sotsiaalfondi logo it akadeemia logo