Cursos de razonamiento automático y demostración asistida por ordenador

En esta página se recopilan cursos de razonamiento automático y demostración asistida por ordenador que sirven de referencia al curso Razonamiento automático de la Universidad de Sevilla.

Está ordenada por países y universidades.

Alemania

Universidad de Friburgo

• Computer-supported modeling and reasoning. ~ Jan-Georg Smaus.

Universidad del Sarre

• Concrete Semantics with Isabelle/HOL (Summer semester 2015) ~ Jasmin Blanchette, Mathias Fleury y Daniel Wand.
• Introduction to computational logic (Summer Semester 2018) ~ Gert Smolka
• Introduction to computational logic (Summer Semester 2019) ~ Gert Smolka

Universidad técnica de Kaiserslautern

• Specification and verification with higher-order logic. ~ Arnd Poetzsch-Heffter.

Universidad técnica de Munich (TUM)

• Introduction to the Isabelle proof assistant. ~ C. Ballarin.
• Introduction to the Isabelle proof assistant. ~ C. Ballarin y G. Klein.
• Semantics of programming languages. ~ Tobias Nipkow.
• Theorem proving with Isabelle/HOL: An intensive course. ~ Tobias Nipkow.

Australia

NICTA

• Advanced topics in software verification. ~ Gerwin Klein.
• Theorem proving: Principles, techniques, applications. ~ Gerwin Klein.

Austria

Universidad de Innsbruck

• Automated theorem proving in Isabelle/HOL. ~ C. Ballarin y T. Weber.
• Automatic deduction. ~ C. Ballarin.
• Experiments in verification: Introduction to Isabelle/HOL. ~ Christian Sternagel
• Interactive theorem proving using Isabelle/HOL. ~ Christian Sternagel.
• Machine learning for theorem proving. ~ C. Kaliszyk

Brasil

Universidad Federal de Rio Grande del Norte

• Lógica computacional: Demonstração assistida e semi-automática de teoremas. ~ Joao Marcos.

Canadá

Universidad de Waterloo

• Computer-aided reasoning for software engineering. ~ Vijay Ganesh.
• Logic and computation. ~ Prabhakar Ragde.

Escocia

Universidad de Edimburgo

• Automated reasoning (2013-14). ~ J. Fleuriot y P. Jackson.
• Automated reasoning (2016-17). ~ J. Fleuriot y P. Jackson.

Estados Unidos

Universidad de Cornell

• Data structures and functional programming. ~ Michael Clarkson.

Carnegie Mellon

• Logic and formal verification. ~ J. Avigad.
• Logic and proof (Release 0.1). ~ J. Avigad, R.Y. Lewis, F. van Doorn

MIT

• Interactive computer theorem proving. ~ A. Chlipala.
• Formal reasoning about programs. ~ A. Chlipala.

Univ. de Berkeley

• Formal methods: specification, verification, and synthesis. ~ S.A. Seshia.

Univ. de Colorado

• Practical theorem proving with Isabelle/Isar. ~ Jeremy G. Siek.
• Theorem proving in Isabelle. ~ Jeremy G. Siek.

Univ. de Northeastern

• Logic and computation. ~ R. Pucella.

Univ. de Pensilvania

• Software foundations. ~ B.C. Pierce et als.
• Software foundations. Vol. 1: Logical foundations. ~ B.C. Pierce et als.

Universidad de Tejas en Austin

• Automated logical reasoning. ~ I. Dillig.
• SAT solving and theorem proving. ~ W.A. Hunt, Jr.

Universidad de Whashington

• Computer-aided reasoning for software. ~ E. Torlak

Francia

Universidad de Lille1

• Introduction à l’assistant de preuve Coq. ~ R. Affeldt

Universidad de Niza

• Coq Winter School 2017.
• Cours vidéo de Coq. ~ Y. Bertot.
• Preuves assistées par ordinateur à l’aide de Coq. ~ Y. Bertot.

Universidad de Rennes 1

• Analyse et conception formelles. ~ T. Genet.
• Software formal analysis and design. ~ T. Genet.

Japón

Universidad de Tsukuba

• Exercises in Information Sciences II (Theorem Proving). ~ F. Ghourabi

Reino Unido

Universidad de Cambridge

• Interactive formal verification. ~ Larry Paulson.
• Interactive formal verification. ~ Tjark Weber.

Suecia

Real Instituto de Tecnología (KTH)

• Advanced formal methods. ~ M. Dam.

Suiza

EPFL (Ecole polytechnique fédérale de Lausanne)

• Synthesis, analysis, and verification. ~ E. Kneuss, V. Kunčak.

ETH de Zúrich

• Computer-supported modeling and reasoning. ~ A.D. Brucker, D. Basin, J.G. Smaus y B. Wolff.