A new course in LP2

[Willard Rafnsson]

Dear students,

There is a new course starting in LP2 which some of you will be interested in. It's called "Automated Reasoning for Program Verification".

Briefly, the course is about proving that a program satisfies a property, formalized in a logic, using a solver for said logic (e.g. MiniSAT, Z3 and Vampire).

I highly recommend it to anyone curious about logic, logic programming, or proving that a program behaves as intended.

See details below.

Cheers,
Willard.

***

Dear Master Students,

In the upcoming study period 2, between October 28-December 13, 2013,
I will teach a new course "Automated Reasoning for Program Verification" at Chalmers:
http://www.cse.chalmers.se/~laurako/links/ARV.html
This course is designed for Master students.

I am writing you today to encourage you to consider the possibility taking this course.

The course is connected to the automated verification of computer programs.
It introduces different approaches for proving automatically that computer systems have no errors.
Depending on the complexity of computer programs, the used programming language and data structures,
proving that software systems have no errors requires proving properties in various fragments of first-order logics,
such as propositional logic, combination of theories (e.g. theory of arrays and integers),
and full first-order logic with equality.
In this course, we will address both the theoretical and practical aspects for using and implementing
automated methods proving correctness of computer programs in such logics.
We will also use the best existing tools in the area,
such as the MiniSAT solver, the Z3 prover, and the Vampire theorem prover.
For example, the Z3 prover is successfully used in the industrial verification of Windows device drivers,
and the Vampire theorem prover, co-developed by our group at Chalmers, is used by Intel and the avionic industry.

Passing the course will earn you 7,5 credits.
The course examination will include solving homework assignments and passing a final written exam.

To sign up for the course, please simply send me an email to laura....@chalmers.se.
Thank you!

If you have any questions or considerations, you are very welcome to contact me.

Looking forward to seeing some of you in the course,

Laura Kovacs

[Willard Rafnsson]

Hello students,

There is another new course starting in LP2 which some of you will be interested in. It's called "Decision Making Under Uncertainty", and is highly recommended for anyone interested in machine learning and artificial intelligence.

See details below.

Also, if you liked the Algorithms course, don't forget to check out the Advanced Algorithms course, also in LP2:

  http://www.cse.chalmers.se/~ptr/advalg.html

Cheers,
Willard.

***

Title: Decision Making Under Uncertainty

Decision theory forms the basis of modern artificial intelligence and economics. This course gives a firm foundation to decision theory from mainly a statistical, but also a philosophical perspective. The course has two aims:

1. To give a thorough understanding of statistical decision theory, automatic methods for designing experiments and relate the theory to human decision making

2. Apply the theory to practical problems in reinforcement learning and artificial intelligence, through the development of algorithms and experiments with intelligent agents.

The course concludes with an agent competition between student groups.

Extensive information about the course, including notes and slides and reading material can be found here:

http://www.cse.chalmers.se/~chrdimi/teaching/optimal_decisions/index.html

Best,
Christos