Learning algorithms and formal verification

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

This tutorial is on applications of computational learning theory to verification of systems. Computational learning theory deals with algorithmic models for learning formally representable concepts using either positive and negative samples or by access to an oracle that can answer certain queries about the concept. The problem of learning formal languages has been particularly useful in verification applications. We will introduce Angluin's algorithm, a learning algorithm that learns regular languages efficiently using an oracle that can answer membership and equivalence queries. We will also survey results on learning regular languages in other learning models. We will give an account of how learning has been used to solve a variety of problems in verification, spanning compositional verification, parameterized model-checking, synthesis of interfaces, machines with unbounded queues, and program testing. In all these examples, a crucial property that is exploited is the simplicity of certain concepts that underlie real-world systems, the learning of which yields a a simple mechanism to prove the correctness of the system. We will also lay out general arguments on why learning algorithms can play a crucial role in the design of verification algorithms, and list some open research directions that work towards this goal.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation, - 8th International Conference, VMCAI 2007, Proceedings
Number of pages1
StatePublished - Nov 27 2007
Event8th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2007 - Nice, France
Duration: Jan 14 2007Jan 16 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4349 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other8th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2007
CountryFrance
CityNice
Period1/14/071/16/07

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Learning algorithms and formal verification'. Together they form a unique fingerprint.

Cite this